Activity: Talk or presentation › Contributed talk › unknown
Description
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 optimal among syntactic
methods for dependency computation.