Efficiently Representing Existential Dependency Sets for Expansion-based
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
4th Doctorial Workshop on Mathematical and Engineering Methods in Computer Science
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Given a quantified boolean formula (QBF) in prenex conjunctive normal
form, we consider the problem of identifying variable dependencies. In
related work, a formal definition of dependencies has been suggested
based on quantifier prefix reordering: two variables are independent
if swapping them in the prefix does not change satisfiability of the
formula. Instead of the general case, we focus on the sets of
depending existential variables for all universal variables which are
relevant particularly for expansion-based QBF solvers. We present an
approach for efficiently computing existential dependency sets by
means of a directed connection relation over variables and demonstrate
how this relation can be compactly represented as a tree using a
union-find data structure. Experimental results show the effectiveness
of our approach.
Forschungs-