##
**Contributions to the theory of practical quantified Boolean formula solving.**
*(English)*
Zbl 1390.68585

Milano, Michela (ed.), Principles and practice of constraint programming. 18th international conference, CP 2012, QuĂ©bec City, QC, Canada, October 8–12, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33557-0/pbk). Lecture Notes in Computer Science 7514, 647-663 (2012).

Summary: Recent solvers for quantified Boolean formulas (QBFs) use a clause learning method based on a procedure proposed by E. Giunchiglia et al. [J. Artif. Intell. Res. (JAIR) 26, 371–416 (2006; Zbl 1183.68475)], which avoids creating tautological clauses. The underlying proof system is Q-resolution. This paper shows an exponential worst case for the clause-learning procedure. This finding confirms empirical observations that some formulas take mysteriously long times to solve, compared to other apparently similar formulas.

Q-resolution is known to be refutation complete for QBF, but not all logically implied clauses can be derived with it. A stronger proof system called QU-resolution is introduced, and shown to be complete in this stronger sense. A new procedure called QPUP for clause learning without tautologies is also described.

A generalization of pure literals is introduced, called effectively depth-monotonic literals. In general, the variable-elimination resolution operation, as used by Quantor, sQueezeBF, and Bloqqer is unsound if the existential variable being eliminated is not at innermost scope. It is shown that variable-elimination resolution is sound for effectively depth-monotonic literals even when they are not at innermost scope.

For the entire collection see [Zbl 1251.68026].

Q-resolution is known to be refutation complete for QBF, but not all logically implied clauses can be derived with it. A stronger proof system called QU-resolution is introduced, and shown to be complete in this stronger sense. A new procedure called QPUP for clause learning without tautologies is also described.

A generalization of pure literals is introduced, called effectively depth-monotonic literals. In general, the variable-elimination resolution operation, as used by Quantor, sQueezeBF, and Bloqqer is unsound if the existential variable being eliminated is not at innermost scope. It is shown that variable-elimination resolution is sound for effectively depth-monotonic literals even when they are not at innermost scope.

For the entire collection see [Zbl 1251.68026].

### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |