A non-prenex, non-clausal QBF solver with game-state learning. (English) Zbl 1306.68161

Strichman, Ofer (ed.) et al., Theory and applications of satisfiability testing – SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14185-0/pbk). Lecture Notes in Computer Science 6175, 128-142 (2010).
Summary: We describe a DPLL-based solver for the problem of quantified boolean formulas (QBF) in non-prenex, non-CNF form. We make two contributions. First, we reformulate clause/cube learning, extending it to non-prenex instances. We call the resulting technique game-state learning. Second, we introduce a propagation technique using ghost literals that exploits the structure of a non-CNF instance in a manner that is symmetric between the universal and existential variables. Experimental results on the QBFLIB benchmarks indicate our approach outperforms other state-of-the-art solvers on certain benchmark families, including the tipfixpoint and tipdiam families of model checking problems.
For the entire collection see [Zbl 1196.68013].


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68T05 Learning and adaptive systems in artificial intelligence
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)


Nenofex; Quaffle
Full Text: DOI Link