Reasoning with Quantified Boolean Formulas

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas(QBFs) is an important research issue in Artificial Intelligence and Computer Science. Indeed, QBF solvers have already been proposed for many reasoning tasks in knowledge representation and reasoning, in automated planning and in formal methods for computer aided design. Even more, since QBF reasoning is the prototypical PSPACE problem, the reduction of many other decision problems in PSPACE are readily available. For these reasons, in the last few years several decision procedures for QBFs have been proposed and implemented, mostly based either on search or on variable elimination, or on a combination of the two. In this chapter, after a brief recap of the basic terminology and notation about QBFs, we briefly review various applications of QBF reasoning that have been recently proposed, and then we focus on the description of the main approaches which are at the basis of currently available solvers for prenex QBFs in conjunctive normal form (CNF). Other approaches and extensions to non prenex, non CNF QBFs are briefly reviewed at the end of the chapter. © 2009 John Franco and John Martin and IOS Press.