A Duality-Aware Calculus for Quantified Boolean Formulas
Katalin Fazekas, Martina Seidl, Armin Biere · 2016
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 statesin a symmetric way. This symmetry simplifies the framework and offers potential for further variants.