Talks and Poster Presentations (with Proceedings-Entry):
U. Egly, H. Tompits, S. Woltran:
"On Quantifier Shifting for Quantified Boolean Formulas";
Talk: Fifth Internternational Symposium on the Theory and Applications of Satisfiability Testing (SAT-02),
Cincinnati, Ohio, USA;
05-06-2002
- 05-09-2002; in: "Proceedings Quantified Boolean Formulas Workshop",
T. Walsh, E. Giunchiglia (ed.);
(2002),
48
- 61.
English abstract:
Since most currently available solvers for quantified Boolean formulas (QBFs) process only input formulas in prenex normal form, suitable translations are required for handling arbitrary formulas. In this paper, we propose a normal form translation incorporating a certain anti-prenexing step in order to obtain QBFs possessing quantifier prefixes such that the number of alternating quantifiers is never greater than the number of alternations obtained by using nondeterministic normal form translations based on usual quantifier shifting rules. Furthermore, our algorithm is deterministic. We show that anti-prenexing is beneficial in some cases for QBF-solvers which are able to process arbitrary QBFs, like BDD-based solvers. We illustrate this point by discussing some experimental results in this direction.
Created from the Publication Database of the Vienna University of Technology.