2026-08-17T17:24:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8517 2024-03-06T10:42:16Z ddc:004 open_access

Genuine Lower Bounds for QBF Expansion Beyersdorff, Olaf Blinkhorn, Joshua QBF proof complexity lower-bound techniques resolution We propose the first general technique for proving genuine lower bounds in expansion-based QBF proof systems. We present the technique in a framework centred on natural properties of winning strategies in the 'evaluation game' interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce a result with manifest practical import: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Joshua Blinkhorn 2018 Is Part Of LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2018.12 urn:nbn:de:0030-drops-85174 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.12 eng https://creativecommons.org/licenses/by/3.0/legalcode