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

DOI10.1016/J.TCS.2009.02.018zbMATH Open1166.68038OpenAlexW2032927579MaRDI QIDQ1019749FDOQ1019749

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

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
• scientific article; zbMATH DE number 3878376
• Automating resolution is NP-hard

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)

Cites Work

• Title not available (Why is that?)
• The relative efficiency of propositional proof systems
• Short proofs are narrow—resolution made simple
• The intractability of resolution
• 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
• Title not available (Why is that?)
• Reducibility among combinatorial problems
• Near optimal seperation of tree-like and general resolution
• Title not available (Why is that?)
• The NP-hardness of finding a directed acyclic graph for regular resolution

Cited In (6)

• A complexity gap for tree resolution
• Title not available (Why is that?)
• Title not available (Why is that?)
• Finding compact scheme forests in nested normal form is NP-hard
• Pool resolution is NP-hard to recognize
• The NP-hardness of finding a directed acyclic graph for regular resolution

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)