A Solver for QBFs in Nonprenex Form

9 years 1 months ago
A Solver for QBFs in Nonprenex Form
Various problems in AI can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula's structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and implement a solver, qpro, which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the nonnormal form case and compare qpro with the leading normal-form provers on problems from the area of AI.
Uwe Egly, Martina Seidl, Stefan Woltran
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where ECAI
Authors Uwe Egly, Martina Seidl, Stefan Woltran
Comments (0)