Pool resolution is NP-hard to recognize
type: Item
instance of: scholarly article
title: Pool resolution is NP-hard to recognize
zbMATH Open document ID: 1185.03084
author: Samuel R. Buss
published in: Archive for Mathematical Logic
publication date: 2009-12-14T00:00:00Z
review text: 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.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 68Q17
zbMATH DE Number: 5646253
zbMATH Keywords: resolution
zbMATH Keywords: proof search
zbMATH Keywords: NP-completeness
MaRDI profile type: Publication
full work available at URL: s00153-009-0152-4
OpenAlex ID: W2008459032
cites work: Minimum propositional proof length is NP-hard to linearly approximate
cites work: Resolution Is Not Automatizable Unless W[P] Is Tractable
cites work: Q5715680
cites work: The NP-hardness of finding a directed acyclic graph for regular resolution
cites work: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
cites work: Finding a tree structure in a resolution proof is NP-complete
cites work: Q4699307
cites work: Q4539605
cites work: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
DOI: 10.1007/S00153-009-0152-4
Recommended article: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
Recommended article: An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
Recommended article: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Recommended article: Automating Resolution is NP-Hard
Recommended article: Small Stone in Pool
Recommended article: Improved Separations of Regular Resolution from Clause Learning Proof Systems
Recommended article: Extended resolution simulates binary decision diagrams
Recommended article: Determinization of Resolution by an Algorithm Operating on Complete Assignments
Recommended article: 2 -Way vs.d -Way Branching for CSP
description: scientific article; zbMATH DE number 5646253