A Compact Representation for Syntactic Dependencies in QBFs

Different quantifier types in Quantified Boolean Formulae (QBF) introduce variable dependencies which have to be taken into consideration when deciding satisfiability of a QBF. In this work, we focus on dependencies based on syntactically connected variables. We generalize our previous ideas for efficiently representing dependency sets of universal variables to existential ones. We obtain a dependency graph which is applicable to arbitrary QBF solvers. The core part of our work is the formulation and correctness proof of a static and compact, tree-shaped connection relation over equivalence classes of existential variables. In practice, this relation is constructed once from a given QBF and allows to share connection information among all variables. We report on practical aspects and demonstrate the effectiveness of our approach in experiments on structured formulae from QBF competitions. Further, we show by example that the common approach of quantifier scope analysis is not opt...

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Florian Lonsing, Armin Biere
• Keywords: Arbitrary Qbf Solvers, Different Quantifier Types, Hardware, Quantified Boolean Formulae, SAT 2009