Quantifier Shifting for Quantified Boolean Formulas Revisited

Simone Heisinger; Maximilian Heisinger; Adrian Rebola Pardo; Martina Seidl

doi:10.1007/978-3-031-63498-7_20

Quantifier Shifting for Quantified Boolean Formulas Revisited

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings
Editors	Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
Publisher	Springer
Pages	325-343
Number of pages	19
Volume	LNAI 14739
ISBN (Print)	978-3-031-63497-0
DOIs	https://doi.org/10.1007/978-3-031-63498-7_20
Publication status	Published - 2024

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14739 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

101013 Mathematical logic
102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102030 Semantic technologies
102031 Theoretical computer science
603109 Logic

JKU Focus areas

Digital Transformation

Access to Document

10.1007/978-3-031-63498-7_20

Cite this

Heisinger, S., Heisinger, M., Rebola Pardo, A., & Seidl, M. (2024). Quantifier Shifting for Quantified Boolean Formulas Revisited. In C. Benzmüller, M. J. H. Heule, & R. A. Schmidt (Eds.), Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings (Vol. LNAI 14739, pp. 325-343). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14739 LNAI). Springer. https://doi.org/10.1007/978-3-031-63498-7_20

Heisinger, Simone ; Heisinger, Maximilian ; Rebola Pardo, Adrian et al. / Quantifier Shifting for Quantified Boolean Formulas Revisited. Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. editor / Christoph Benzmüller ; Marijn J. H. Heule ; Renate A. Schmidt. Vol. LNAI 14739 Springer, 2024. pp. 325-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e0c6f8c52f7a469cbe8cc8c6c4d1f628,

title = "Quantifier Shifting for Quantified Boolean Formulas Revisited",

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.",

author = "Simone Heisinger and Maximilian Heisinger and \{Rebola Pardo\}, Adrian and Martina Seidl",

year = "2024",

doi = "10.1007/978-3-031-63498-7\_20",

language = "English",

isbn = "978-3-031-63497-0",

volume = "LNAI 14739",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "325--343",

editor = "Christoph Benzm{\"u}ller and Heule, \{Marijn J. H.\} and Schmidt, \{Renate A.\}",

booktitle = "Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings",

}

Heisinger, S , Heisinger, M , Rebola Pardo, A & Seidl, M 2024, Quantifier Shifting for Quantified Boolean Formulas Revisited. in C Benzmüller, MJH Heule & RA Schmidt (eds), Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. vol. LNAI 14739, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14739 LNAI, Springer, pp. 325-343. https://doi.org/10.1007/978-3-031-63498-7_20

Quantifier Shifting for Quantified Boolean Formulas Revisited. / Heisinger, Simone ; Heisinger, Maximilian ; Rebola Pardo, Adrian et al.
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. ed. / Christoph Benzmüller; Marijn J. H. Heule; Renate A. Schmidt. Vol. LNAI 14739 Springer, 2024. p. 325-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14739 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Quantifier Shifting for Quantified Boolean Formulas Revisited

AU - Heisinger, Simone

AU - Heisinger, Maximilian

AU - Rebola Pardo, Adrian

AU - Seidl, Martina

PY - 2024

Y1 - 2024

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85200231845

U2 - 10.1007/978-3-031-63498-7_20

DO - 10.1007/978-3-031-63498-7_20

M3 - Conference proceedings

SN - 978-3-031-63497-0

VL - LNAI 14739

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 325

EP - 343

BT - Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings

A2 - Benzmüller, Christoph

A2 - Heule, Marijn J. H.

A2 - Schmidt, Renate A.

PB - Springer

ER -

Heisinger S , Heisinger M , Rebola Pardo A , Seidl M. Quantifier Shifting for Quantified Boolean Formulas Revisited. In Benzmüller C, Heule MJH, Schmidt RA, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. Vol. LNAI 14739. Springer. 2024. p. 325-343. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-63498-7_20

Quantifier Shifting for Quantified Boolean Formulas Revisited

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this