An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation

摘要

The high computational complexity of advanced reasoning tasks such as reasoning about knowledge and planning calls for efficient and reliable algorithms for reasoning problems harder than NP. In this paper we propose Evaluate, an algorithm for evaluating quantified Boolean formulae (QBFs). Algorithms for evaluation of QBFs are suitable for experimental analysis of problems that belong to a wide range of complexity classes, a property not easily found in other formalisms. Evaluate is a generalization of the Davis-Putnam procedure for SAT and is guaranteed to work in polynomial space.