Heisinger, S., Heisinger, M., Rebola-Pardo, A., & Seidl, M. (2024). Quantifier Shifting for Quantified Boolean Formulas Revisited. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 325–343). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_20
12th International Joint Conference on Automated Reasoning (IJCAR 2024)
en
Event date:
3-Jul-2024 - 6-Jul-2024
-
Event place:
Nancy, France
-
Number of Pages:
19
-
Publisher:
Springer International Publishing
-
Peer reviewed:
Yes
-
Keywords:
Normal Form Transformation; Prenexing; Quantified Boolean Formulas
en
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
Project title:
Heisenbugs: Auffindung und Erklärung: VRG11-005 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
CC BY 4.0
