A satisfiability procedure for quantified Boolean formulae

We present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSAT(CNF) Of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a sequence of such replacements, the original formula can be simplified to true or false. It may also be necessary to transform the original formula to generate a subformula to replace. QSAT(CNF) eliminates collections of variables from an unquantified clause form formula until all variables have been eliminated. QSAT and QSAT(CNF) can be applied to hardware verification and symbolic model checking. Results of an implementation of QSAT(CNF) are described, as well as some complexity results for QSAT and QSAT(CNF). QSAT runs in linear time on a class of quantified Boolean formulae related to symbolic model checking. We present the class of "long and thin" unquantified formulae and give evidence that this class is common in applications. We also give theoretical and empirical evidence that QSAT(CNF) is often faster than Davis and Putnam-type satisfiability checkers and ordered binary decision diagrams (OBDDs) on this class of formulae. We give an example where QSAT(CNF) is exponentially faster than BDDs. (C) 2003 Elsevier B.V. All rights reserved.