Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
U. Egly, H. Tompits, S. Woltran:
"On Quantifier Shifting for Quantified Boolean Formulas";
Vortrag: Fifth Internternational Symposium on the Theory and Applications of Satisfiability Testing (SAT-02),
Cincinnati, Ohio, USA;
06.05.2002
- 09.05.2002; in: "Proceedings Quantified Boolean Formulas Workshop",
T. Walsh, E. Giunchiglia (Hrg.);
(2002),
S. 48
- 61.
Kurzfassung englisch:
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.
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.