Katalin Fazekas, Martina Seidl, Armin Biere,
"A Duality-Aware Calculus for Quantified Boolean Formulas"
: Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), IEEE Computer Society, Seite(n) 181-186, 2017
A Duality-Aware Calculus for Quantified Boolean Formulas
Sprache des Titels:
Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)
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.