A solver for QBFs in negation normal form |
| |
Authors: | Uwe Egly Martina Seidl Stefan Woltran |
| |
Affiliation: | (1) Knowledge-based Systems Group E184/3, Institute of Information Systems, Vienna University of Technology, Favoritenstrasse 9-11, A-1040 Vienna, Austria;(2) Business Informatics Group E188/3, Institute of Software Technology and Interactive Systems, Vienna University of Technology, Favoritenstrasse 9-11, 1040 Vienna, Austria;(3) Database and Artificial Intelligence Group E184/2, Institute of Information Systems, Vienna University of Technology, Favoritenstrasse 9-11, A-1040 Vienna, Austria |
| |
Abstract: | Various problems in artificial intelligence 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 describe a solver, $\ensuremath{\sf qpro}Various problems in artificial intelligence 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 describe a solver, , which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare
with the leading normal form provers on several problems from the area of artificial intelligence. We prove properties of
the algorithms generalized to non-clausal form by using a novel approach based on a sequent-style formulation of the calculus.
This paper is based on an extended abstract presented at ECAI 2006 (see 16]). This work was supported by the Austrian Science Fund (FWF) under grant P18019, the Austrian Academic Exchange Service
(?AD) under grant Amadée 2/2006, and by the Austrian Federal Ministry of Transport, Innovation and Technology BMVIT and the
Austrian Research Promotion Agency FFG under grant FIT-IT-810806. |
| |
Keywords: | Solver QBFs Negation normal form |
本文献已被 SpringerLink 等数据库收录! |
|