On Quantifier Shifting for Quantified Boolean Formulas
Uwe Egly, Hans Tompits, Stefan Woltran · 2004
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. 1