Solving QBF with combined conjunctive and disjunctive normal form

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