2026-07-23T04:16:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20583 2024-08-23T05:50:28Z ddc:004 open_access

Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree Beyersdorff, Olaf Hoffmann, Tim Kasche, Kaspar Spachmann, Luc Nicolas proof complexity QBF polynomial calculus circuits lower bounds We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-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 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Tim Hoffmann and Kaspar Kasche and Luc Nicolas Spachmann 2024 Is Part Of LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2024.27 urn:nbn:de:0030-drops-205834 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.27 eng https://creativecommons.org/licenses/by/4.0/legalcode