Bounded universal expansion for preprocessing QBF. (English) Zbl 1214.68331
Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 244-257 (2007).
Summary: We present a new approach for preprocessing Quantified Boolean Formulas (QBF) in conjunctive normal form (CNF) by expanding a selection of universally quantified variables with bounded expansion costs. We describe a suitable selection strategy which exploits locality of universals and combines cost estimates with goal orientation by taking into account unit literals which might be obtained.
Furthermore, we investigate how Q-resolution can be integrated into this method. In particular, resolution is applied specifically to reduce the amount of copying necessary for universal expansion.
Experimental results demonstrate that our preprocessing can successfully improve the performance of state-of-the-art QBF solvers on well-known problems from the QBFLIB collection.
For the entire collection see [Zbl 1120.68007].
Furthermore, we investigate how Q-resolution can be integrated into this method. In particular, resolution is applied specifically to reduce the amount of copying necessary for universal expansion.
Experimental results demonstrate that our preprocessing can successfully improve the performance of state-of-the-art QBF solvers on well-known problems from the QBFLIB collection.
For the entire collection see [Zbl 1120.68007].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
