2026-07-23T16:56:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6875 2024-03-06T10:39:05Z ddc:004 open_access

Understanding Cutting Planes for QBFs Beyersdorff, Olaf Chew, Leroy Mahajan, Meena Shukla, Anil proof complexity QBF cutting planes resolution simulations We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res. Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Olaf Beyersdorff and Leroy Chew and Meena Mahajan and Anil Shukla 2016 Is Part Of LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2016.40 urn:nbn:de:0030-drops-68758 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40 eng https://creativecommons.org/licenses/by/3.0/legalcode