Pool resolution is NP-hard to recognize

DOI10.1007/s00153-009-0152-4zbMath1185.03084OpenAlexW2008459032MaRDI QIDQ1042441

Samuel R. Buss

Publication date: 14 December 2009

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

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

zbMATH Keywords

NP-completenessresolutionproof search

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The NP-hardness of finding a directed acyclic graph for regular resolution
• Finding a tree structure in a resolution proof is NP-complete
• Minimum propositional proof length is NP-hard to linearly approximate
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning

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