<div class="csl-bib-body">
<div class="csl-entry">Heisinger, S., Heisinger, M., Rebola-Pardo, A., & Seidl, M. (2024). Quantifier Shifting for Quantified Boolean Formulas Revisited. In <i>Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I</i> (pp. 325–343). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_20</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/209726
-
dc.description.abstract
Modern solvers for quantified Boolean formulas (QBFs) process formulas in prenex form, which divides each QBF into two parts: the quantifier prefix and the propositional matrix. While this representation does not cover the full language of QBF, every non-prenex formula can be transformed to an equivalent formula in prenex form. This transformation offers several degrees of freedom and blurs structural information that might be useful for the solvers. In a case study conducted 20 years back, it has been shown that the applied transformation strategy heavily impacts solving time. We revisit this work and investigate how sensitive recent QBF solvers perform w.r.t. various prenexing strategies.
en
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Normal Form Transformation
en
dc.subject
Prenexing
en
dc.subject
Quantified Boolean Formulas
en
dc.title
Quantifier Shifting for Quantified Boolean Formulas Revisited
