An Algorithm to Evaluate Quantified Boolean Formulae

Thehigh computational complexityof advancedreasoningtasks suchas belief revision andplanningcalls for efficient andreliable algorithms for reasoningproblems harder than NP. In this paper weproposeEvaluate, an algorithmfor evaluating Quantified Boolean Formulae, a languagethat extendspropositional logic in a waysuch that manyadvanced forms of propositional reasoning, e. g. , reasoningabout knowledge, can be easily formulatedas evaluation of a QBF. Algorithmsfor evaluation of QBFs are suitable for the experimental analysis on a wide range of complexity classes, a propertynot easily foundin other formalisms. Evaluateis basedon a generalization of the Davis-Putnamprocedure for SAT, and is guaranteed to workin polynomialspace. Beforepresenting Evaluate, wediscuss all the abstract properties of QBFs that wesingled out to makethe algorithmmoreefficient. We also briefly mentionthe mainresults of the experimentalanalysis, whichis reportedelsewhere.

Authors

• Marco Cadoli Andrea Giovanardi

Keywords

No keywords are indexed for this paper.