Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR17-037 | 25th February 2017 10:51

#### Understanding Cutting Planes for QBFs

TR17-037
Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Publication: 27th February 2017 16:45
Downloads: 223
Keywords:

Abstract:

We define a cutting planes system CP+\$\forall\$red 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+\$\forall\$red 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 \$\forall\$Exp+Res. A similar picture holds for a semantic version semCP+\$\forall\$red.

Technically, our results establish the effectiveness of two lower bound techniques for CP+\$\forall\$red: via strategy extraction and via monotone feasible interpolation.

ISSN 1433-8092 | Imprint