A Compact Representation for Syntactic Dependencies in QBFs

12 years 3 days ago
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...
Florian Lonsing, Armin Biere
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SAT
Authors Florian Lonsing, Armin Biere
Comments (0)