The NP-hardness of finding a directed acyclic graph for regular resolution

DOI10.1016/j.tcs.2008.01.039zbMath1145.03034OpenAlexW2084517146MaRDI QIDQ924157

Jan Hoffmann, Samuel R. Buss

Publication date: 28 May 2008

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

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

zbMATH Keywords

NP-completenessdirected acyclic graphresolutionregular resolution

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items

Finding a tree structure in a resolution proof is NP-complete ⋮ Pool resolution is NP-hard to recognize

Cites Work

• On the complexity of regular resolution and the Davis-Putnam procedure
• On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
• Minimum propositional proof length is NP-hard to linearly approximate
• Regular Resolution Versus Unrestricted Resolution
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• An exponential separation between regular and general resolution
• The relative efficiency of propositional proof systems
• Regular resolution lower bounds for the weak pigeonhole principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item