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

DOI10.1016/J.TCS.2009.02.018MaRDI QIDQ1019749zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• The NP-hardness of finding a directed acyclic graph for regular resolution
• Pool resolution is NP-hard to recognize
• A complexity gap for tree resolution
• Publication:3343454
• Automating resolution is NP-hard

Cites work

• scientific article; zbMATH DE number 5899257 (Why is no real title available?)
• scientific article; zbMATH DE number 1361489 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Minimum propositional proof length is NP-hard to linearly approximate
• Near optimal seperation of tree-like and general resolution
• Reducibility among combinatorial problems
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Short proofs are narrow—resolution made simple
• The NP-hardness of finding a directed acyclic graph for regular resolution
• The intractability of resolution
• The relative efficiency of propositional proof systems

Cited in

(6)

• Pool resolution is NP-hard to recognize
• The NP-hardness of finding a directed acyclic graph for regular resolution
• Finding compact scheme forests in nested normal form is NP-hard
• scientific article; zbMATH DE number 7238987 (Why is no real title available?)
• A complexity gap for tree resolution
• scientific article; zbMATH DE number 1522926 (Why is no real title available?)

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

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