Go to page
 

Bibliographic Metadata

Title
A Duality-Aware Calculus for Quantified Boolean Formulas
AuthorFazekas, Katalin ; Seidl, Martina ; Biere, Armin
Published in
SYNASC 2016 / Davenport, James; Negru, Viorel; Ida, Tetsuo; Petcu, Dana; Jebelean, Tudor; Watt, Stephen; Zaharie, Daniela, 2016, page 181-186
Published2016
LanguageEnglish
Series18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Document typeArticle in a collected edition
Keywords (DE)Quantifizierte Boolsche Formel
Keywords (EN)Quantified Boolean Formulas
Project-/ReportnumberW1255-N23
Project-/ReportnumberS11408-N23
ISBN978-1-5090-5707-8
URNurn:nbn:at:at-ubl:3-75 Persistent Identifier (URN)
DOI10.1109/SYNASC.2016.038 
Restriction-Information
 The work is publicly available
Files
A Duality-Aware Calculus for Quantified Boolean Formulas [0.23 mb]
Links
Reference
Classification
Abstract (German)

Wir präsentieren ein formales Rahmenwerk, das es ermöglicht das Verhalten von QBF-Beweisen zu beschreiben.

Abstract (English)

Learning and backjumping are essential features in search-based decision procedures for Quantified 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 simplifies the framework and offers potential for further variants.

Stats
The PDF-Document has been downloaded 50 times.