Variable Dependencies and Q-Resolution

Abstract We propose Q ( D )-resolution, a proof system for Quantified Boolean Formulas. Q ( D )-resolution is a generalization of Q-resolution parameterized by a dependency scheme D. This system is motivated by the generalization of the QDPLL algorithm using dependency schemes implemented in the solver DepQBF. We prove soundness of Q ( D )-resolution for a dependency scheme D that is strictly more general than the standard dependency scheme; the latter is currently used by DepQBF. This result is obtained by proving correctness of an algorithm that transforms Q ( D )-resolution refutations into Q-resolution refutations and could be of independent practical interest. We also give an alternative characterization of resolution- path dependencies in terms of directed walks in a formula’s implication graph which admits an algorithmically more advantageous treatment.

Authors

• Friedrich Slivovsky
• Stefan Szeider

Keywords

No keywords are indexed for this paper.