Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers
Given a quantied boolean formula (QBF) in prenex con- junctive normal form, we consider the problem of identifying variable dependencies. In related work, a formal denition of dependencies has been suggested based on quantier prex reordering: two variables are independent if swapping them in the prex does not change satisa- bility 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 eciently 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-nd data structure. Experimental results show the eectiveness of our approach.