Finding a tree structure in a resolution proof is NP-complete
type: Item
instance of: scholarly article
title: Finding a tree structure in a resolution proof is NP-complete
zbMATH Open document ID: 1166.68038
author: Jan Hoffmann
published in: Theoretical Computer Science
publication date: 2009-05-28T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 68Q17
zbMATH DE Number: 5559010
zbMATH Keywords: resolution
zbMATH Keywords: tree-like resolution
zbMATH Keywords: NP-completeness
MaRDI profile type: Publication
full work available at URL: j.tcs.2009.02.018
OpenAlex ID: W2032927579
cites work: Minimum propositional proof length is NP-hard to linearly approximate
cites work: Q3002781
cites work: Resolution Is Not Automatizable Unless W[P] Is Tractable
cites work: Near optimal seperation of tree-like and general resolution
cites work: Short proofs are narrow—resolution made simple
cites work: The NP-hardness of finding a directed acyclic graph for regular resolution
cites work: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
cites work: The relative efficiency of propositional proof systems
cites work: The intractability of resolution
cites work: Q4699307
cites work: Reducibility Among Combinatorial Problems
cites work: Q5593816
DOI: 10.1016/J.TCS.2009.02.018
description: scientific article; zbMATH DE number 5559010