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. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Slivovsky, F., & Szeider, S. (2014). Variable dependencies and Q-resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8561 LNCS, pp. 269–284). Springer Verlag. https://doi.org/10.1007/978-3-319-09284-3_21
Mendeley helps you to discover research relevant for your work.