Improvements to the Evaluation of Quantified Boolean Formulae

Abstract

We present a theorem-prover for quantified Boolean formulae and eva luat e it on random quantified formulae and formulae that represent problems from a utomat ed planning. Even though the notion of quantified Boolean formula is theoretically important, automated reasoning with QBF has not been thoroughly investigated. Universal quantifiers are needed in representing many computational problems that cannot be easily translated to the propositional logic and solved by satisfiability algorithms. Therefore effi cient reasoning with QBF is important. The Davis-Putnam procedure can be extended to evaluate quantified Bool ea n formulae. A straightforward algorithm of this kind is not very efficient. We identify universal quantifiers as the main a rea where improvements to the basic algorithm can be made. We present a number of techniques for reducing the amount of search that is needed, and evaluate their e ffectiveness by running the algorithm on a co ll ection of formulae obtained from planning and gen erated randomly. For the structured problems we consider, the techniques lead to a dramatic speed-up.