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

Institute of Formal Models and Verification

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

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.

Original language	English
Title of host publication	Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)
Editors	James Davenport, Dana Petcu, Tudor Jebelean, Viorel Negru, Stephen M. Watt, Tetsuo Ida, Daniela Zaharie
Publisher	IEEE Computer Society
Pages	181-186
Number of pages	6
ISBN (Electronic)	9781509057078
DOIs	https://doi.org/10.1109/SYNASC.2016.038
Publication status	Published - 23 Jan 2017

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1109/SYNASC.2016.038

Cite this

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 (Eds.), Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16) (pp. 181-186). Article 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). ed. / James Davenport; Dana Petcu; Tudor Jebelean; Viorel Negru; Stephen M. Watt; Tetsuo Ida; Daniela Zaharie. IEEE Computer Society, 2017. p. 181-186 7829610.

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

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 -

A Duality-Aware Calculus for Quantified Boolean Formulas

Abstract

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this