Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR24-038 | 27th February 2024 15:47

Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree

RSS-Feed




TR24-038
Authors: Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann
Publication: 29th February 2024 08:39
Downloads: 195
Keywords: 


Abstract:

We initiate an in-depth proof-complexity analysis of polynomial calculus (Q-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of Q-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for Q-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999).
We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in Q-PC. This leads to incomparability results for Q-PC systems over different fields.



ISSN 1433-8092 | Imprint