A Non-prenex, Non-clausal QBF Solver with Game-State Learning

摘要

We describe a DPLL-based solver for the problem of quan tified 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 tipf ixpoint and tipdiam families of model checking problems.