Academic
Publications
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers

Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers,10.1016/j.entcs.2009.08.029,Electronic Notes in Theoretical Compu

Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers   (Citations: 1)
BibTex | RIS | RefWorks Download
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.
Journal: Electronic Notes in Theoretical Computer Science - ENTCS , vol. 251, pp. 83-95, 2009
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: