@inproceedings{93359485997848dc8db40fdc3114cd8b,

title = "Comparing Different Prenexing Strategies for Quantified Boolean Formulas",

abstract = "The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a prepositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not.",

author = "Uwe Egly and Martina Seidl and Hans Tompits and Stefan Woltran and M. Zolda",

note = "Copyright 2008 Elsevier B.V., All rights reserved.; 6th Int Conf, SAT 2003 ; Conference date: 05-05-2003 Through 08-05-2003",

year = "2004",

doi = "10.1007/978-3-540-24605-3_17",

language = "English",

isbn = "978-3-540-20851-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "214--228",

editor = "Enrico Giunchiglia and Armando Tacchella",

booktitle = "Theory and Applications of Satisfiability Testing",

}