[Back]

F. Slivovsky, St. Szeider:
"Dependency Schemes and Q-resolution";
Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Vienna, Austria; 2014-07-14 - 2014-07-17; in: "SAT 2014", LNCS / Springer, 8561 (2014), ISBN: 978-3-319-09283-6; 269 - 284.

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.

Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems