Armin Biere,
"Tutorial on Model Checking, Modelling and Verification in Computer Science"
: Proc. 3rd Intl. Conf. on Algebraic Biology (AB'08), Lecture Notes in Computer Science (LNCS),, Vol. 5147, Springer, 2008
Original Titel:
Tutorial on Model Checking, Modelling and Verification in Computer Science
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 3rd Intl. Conf. on Algebraic Biology (AB'08), Lecture Notes in Computer Science (LNCS),
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.