Pool resolution is NP-hard to recognize (Q1042441): Difference between revisions

Pool resolution, introduced by \textit{A. Van Gelder} [``Pool resolution and its relation to regular resolution and DPLL with clause learning'', Lect. Notes Comput. Sci. 3835, 580--594 (2005; Zbl 1143.68582)], is a restriction of the resolution propositional refutation system where the proof dag contains a depth-first traversal tree in which every variable is resolved at most once. It is intended to model DPLL-based satisfiability testing algorithms using clause learning and backtracking. Pool resolution can ``effectively p-simulate'' full resolution, due to \textit{F. Bacchus}, \textit{P. Hertel}, \textit{T. Pitassi} and \textit{A. Van Gelder} [``Clause learning can effectively p-simulate general propositional resolution'', in: Proc.\ of 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), AAAI Press, 283--290 (2008)], but it is unknown whether it can directly p-simulate full resolution. In this paper, the author proves that recognizing valid pool resolution proofs is NP-hard. The argument is based on a reduction from SAT: given a CNF formula, a valid resolution refutation (of another formula) is constructed in polynomial time such that the original formula is satisfiable if and only if the proof admits a regular depth-first traversal tree.