Understanding cutting planes for QBFs
Understanding cutting planes for QBFs
复制标题
DOI：
10.1016/j.ic.2018.08.002
复制
发表时间：
2018-10-01
影响因子：
1
通讯作者：
Shukla, Anil
中科院分区：
文献类型：
--
作者：
Beyersdorff, Olaf;Chew, Leroy;Shukla, Anil
We study the cutting planes system CP + for all red for quantified Boolean formulas (QBF), obtained by augmenting propositional Cutting Planes with a universal reduction rule, 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 + for all 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 for all Exp + Res. A similar picture holds for a semantic version semCP + for all red. Technically, our results establish the effectiveness of two lower bound techniques for CP + for all red: via strategy extraction and via monotone feasible interpolation. (C) 2018 Elsevier Inc. All rights reserved.
