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.

• Type: Conference
• Year: 2010
• Where: SAT
• Authors: William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke
• Keywords: Certain Benchmark Families, Hardware, Model Checking Problems, Quantified Boolean Formulas, SAT 2010