Pool resolution is NP-hard to recognize

DOI10.1007/S00153-009-0152-4MaRDI QIDQ1042441zbMATH OpenOpenAlexFDO

Authors Samuel R. Buss

Publication date 14 December 2009

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial 4.0 International

Full work available at URL https://doi.org/10.1007/s00153-009-0152-4

zbMATH Keywords

NP-completenessproof searchresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

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.

Recommendations

• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• An improved separation of regular resolution from pool resolution and clause learning
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Automating resolution is NP-hard
• Small Stone in pool
• Improved separations of regular resolution from clause learning proof systems
• Extended resolution simulates binary decision diagrams
• Determinization of Resolution by an Algorithm Operating on Complete Assignments
• 2 -Way vs.d -Way Branching for CSP

Cites work

• Finding a tree structure in a resolution proof is NP-complete
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 1361489 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Minimum propositional proof length is NP-hard to linearly approximate
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• The NP-hardness of finding a directed acyclic graph for regular resolution

Cited in

(5)

• Finding a tree structure in a resolution proof is NP-complete
• Automating resolution is NP-hard
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Small Stone in pool
• The NP-hardness of finding a directed acyclic graph for regular resolution

This page was built for publication: Pool resolution is NP-hard to recognize

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1042441)