Using Autarky to Evaluate Quantified Boolean Formulae
Jens Rühmkorf · elib (German Aerospace Center) · 2010
Abstract — In this paper, we discuss algorithmical implica-tions for the extension of autarky from propositional logic to evaluate quantified boolean formulae (QBF). First, the Davis-Putnam procedure for the satisfiability problem (SAT) is described. Then we explain efficient known data structures for SAT and extensions to QBF which we used in our solver. Finally, we introduce the concept of autarky and describe how detecting 2-autarky structures in a given QBF formula helps pruning the search tree. To the best of our knowledge we are the first to describe such techniques for QBF. Keywords—Autarky; Davis-Putnam; SAT; QBF I.