Simone Heisinger, Maximilian Heisinger, Adrian Rebola Pardo, Martina Seidl,
"Quantifier Shifting for Quantified Boolean Formulas Revisited"
, in Christoph Benzmüller, Marijn J.H. Heule, Renate A. Schmidt: Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Serie Lecture Notes in Computer Science, Vol. LNAI 14739, Springer, Seite(n) 325-343, 2024, ISBN: 978-3-031-63497-0
Original Titel:
Quantifier Shifting for Quantified Boolean Formulas Revisited
Sprache des Titels:
Englisch
Original Buchtitel:
Automated Reasoning, 12th International Joint Conference, IJCAR 2024
Original Kurzfassung:
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.
Forschungs-