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

Let R be a resolution refutation, given as a sequence of clauses without explicit description of the underlying dag. Then, it is NPcomplete to decide whether R is a regular resolution refutation.

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Samuel R. Buss, Jan Hoffmann 0002
• Keywords: Explicit Description, Regular Resolution Refutation, Resolution Refutation, TCS 2008, Theoretical Computer Science