A Duality-Aware Calculus for Quantified Boolean Formulas

Katalin Fazekas; Martina Seidl; Armin Biere

doi:10.1109/SYNASC.2016.038

A Duality-Aware Calculus for Quantified Boolean Formulas

Katalin Fazekas
, Martina Seidl
, Armin Biere

Institut für Formale Modelle und Verifikation

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

Abstract

Learning and backjumping are essential features in search-based decision procedures for Quantiﬁed Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allows to simultaneously reason on prenex conjunctive and disjunctive normal form. It captures both satisfying and falsifying search states in a symmetric way. This symmetry simpliﬁes the framework and offers potential for further variants.

Originalsprache	Englisch
Titel	Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)
Herausgeber*innen	James Davenport, Dana Petcu, Tudor Jebelean, Viorel Negru, Stephen M. Watt, Tetsuo Ida, Daniela Zaharie
Verlag	IEEE Computer Society
Seiten	181-186
Seitenumfang	6
ISBN (elektronisch)	9781509057078
DOIs	https://doi.org/10.1109/SYNASC.2016.038
Publikationsstatus	Veröffentlicht - 23 Jän. 2017

Wissenschaftszweige

102 Informatik
102001 Artificial Intelligence
102011 Formale Sprachen
102022 Softwareentwicklung
102031 Theoretische Informatik
603109 Logik
202006 Computer Hardware

JKU-Schwerpunkte

Computation in Informatics and Mathematics

Zugriff auf Dokument

10.1109/SYNASC.2016.038

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

Fazekas, K., Seidl, M., & Biere, A. (2017). A Duality-Aware Calculus for Quantified Boolean Formulas. in J. Davenport, D. Petcu, T. Jebelean, V. Negru, S. M. Watt, T. Ida, & D. Zaharie (Hrsg.), Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16) (S. 181-186). Artikel 7829610 IEEE Computer Society. https://doi.org/10.1109/SYNASC.2016.038

@inproceedings{6ea747b9a1d442ef8a427ddd275609d1,

title = "A Duality-Aware Calculus for Quantified Boolean Formulas",

abstract = "Learning and backjumping are essential features in search-based decision procedures for Quantiﬁed Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allows to simultaneously reason on prenex conjunctive and disjunctive normal form. It captures both satisfying and falsifying search states in a symmetric way. This symmetry simpliﬁes the framework and offers potential for further variants.",

author = "Katalin Fazekas and Martina Seidl and Armin Biere",

year = "2017",

month = jan,

day = "23",

doi = "10.1109/SYNASC.2016.038",

language = "English",

pages = "181--186",

editor = "James Davenport and Dana Petcu and Tudor Jebelean and Viorel Negru and Watt, \{Stephen M.\} and Tetsuo Ida and Daniela Zaharie",

booktitle = "Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)",

publisher = "IEEE Computer Society",

}

A Duality-Aware Calculus for Quantified Boolean Formulas. / Fazekas, Katalin; Seidl, Martina; Biere, Armin.
Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16). Hrsg. / James Davenport; Dana Petcu; Tudor Jebelean; Viorel Negru; Stephen M. Watt; Tetsuo Ida; Daniela Zaharie. IEEE Computer Society, 2017. S. 181-186 7829610.

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

TY - GEN

T1 - A Duality-Aware Calculus for Quantified Boolean Formulas

AU - Fazekas, Katalin

AU - Seidl, Martina

AU - Biere, Armin

PY - 2017/1/23

Y1 - 2017/1/23

N2 - Learning and backjumping are essential features in search-based decision procedures for Quantiﬁed Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allows to simultaneously reason on prenex conjunctive and disjunctive normal form. It captures both satisfying and falsifying search states in a symmetric way. This symmetry simpliﬁes the framework and offers potential for further variants.

AB - Learning and backjumping are essential features in search-based decision procedures for Quantiﬁed Boolean Formulas (QBF). To obtain a better understanding of such procedures, we present a formal framework, which allows to simultaneously reason on prenex conjunctive and disjunctive normal form. It captures both satisfying and falsifying search states in a symmetric way. This symmetry simpliﬁes the framework and offers potential for further variants.

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

U2 - 10.1109/SYNASC.2016.038

DO - 10.1109/SYNASC.2016.038

M3 - Conference proceedings

SP - 181

EP - 186

BT - Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)

A2 - Davenport, James

A2 - Petcu, Dana

A2 - Jebelean, Tudor

A2 - Negru, Viorel

A2 - Watt, Stephen M.

A2 - Ida, Tetsuo

A2 - Zaharie, Daniela

PB - IEEE Computer Society

ER -