2026-07-22T22:13:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4905 2024-03-06T10:35:31Z ddc:004 open_access

Proof Complexity of Resolution-based QBF Calculi Beyersdorff, Olaf Chew, Leroy Janota, Mikolás proof complexity QBF lower bound techniques separations Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance Q-resolution and extensions. With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et al. [34] for the strong expansion-based calculus IR-calc. Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers (forallExp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two different classes were not known before. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Leroy Chew and Mikolás Janota 2015 Is Part Of LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2015.76 urn:nbn:de:0030-drops-49057 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.76 eng https://creativecommons.org/licenses/by/3.0/legalcode