Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR18-102 | 15th May 2018 11:42

Short Proofs in QBF Expansion


Authors: Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
Publication: 22nd May 2018 20:47
Downloads: 890


For quantified Boolean formulas (QBF) there are two main different approaches to solving: QCDCL and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than CDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of expansion solving techniques over QCDCL solving.

Our first result shows that tree-like expansion systems allow short proofs of QBFs that are a source of hardness for QCDCL, i.e. tree-like Exp+Res is strictly stronger than tree-like Q-Resolution.

In our second result we efficiently transform dag-like Q-Resolution proofs of QBFs with bounded quantifier complexity into Exp+Res proofs. This is theoretical confirmation of experimental findings by Lonsing and Egly, who observed that expansion QBF solvers often outperform QCDCL solvers on instances with few quantifier alternations.

ISSN 1433-8092 | Imprint