Finding a tree structure in a resolution proof is NP-complete

DOI10.1016/j.tcs.2009.02.018zbMath1166.68038OpenAlexW2032927579MaRDI QIDQ1019749

Jan Hoffmann

Publication date: 28 May 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.02.018

zbMATH Keywords

NP-completenessresolutiontree-like resolution

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)

Related Items (1)

Pool resolution is NP-hard to recognize

Cites Work

• Near optimal seperation of tree-like and general resolution
• The NP-hardness of finding a directed acyclic graph for regular resolution
• The intractability of resolution
• Minimum propositional proof length is NP-hard to linearly approximate
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Reducibility Among Combinatorial Problems
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• The relative efficiency of propositional proof systems
• Short proofs are narrow—resolution made simple
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Finding a tree structure in a resolution proof is NP-complete