Solving QBF by Combining Conjunctive and Disjunctive Normal Forms

Proceedings of the AAAI Conference on Artificial Intelligence, 21

Volume

Technical Papers

Constraint Satisfaction and Satisfiability

Similar to most state-of-the-art Boolean Satisfiability (SAT) solvers, all contemporary Quantified Boolean Formula (QBF) solvers require inputs to be in the Conjunctive Normal Form (CNF). Most of them also store the QBF in CNF internally for reasoning. In order to use these solvers, arbitrary Boolean formulas have to be transformed into equi-satisfiable formulas in Conjunctive Normal Form by introducing additional variables. In this paper, we point out an inherent limitation of this approach, namely the asymmetric treatment of satisfactions and conflicts. This deficiency leads to artificial increase of search space for QBF solving. To overcome the limitation, we propose to transform a Boolean formula into a combination of an equi-satisfiable CNF formula and an equi-tautological DNF formula for QBF solving. QBF solvers based on this approach treat satisfactions and conflicts symmetrically, thus avoiding the exploration of unnecessary search space. A QBF solver called IQTest is implemented based on this idea. Experimental results show that it significantly outperforms existing QBF solvers.