A non-prenex, non-clausal QBF solver with game-state learning

Abstract

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. © 2010 Springer-Verlag.