×

Variable dependencies and Q-resolution. (English) Zbl 1423.68426

Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 269-284 (2014).
Summary: 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.
For the entire collection see [Zbl 1293.68033].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI