Article:
Samuel R. Buss and Jan Hoffmann.
"The NP-hardness of finding a directed acyclic graph for regular resolution"
Theoretical Computer Science 396 (2008) 271-276.
doi:10.1016/j.tcs.2008.01.039
Download: PDF.
Abstract: Let R be a resolution refutation, given as a sequence of clauses without explicit description of the underlying dag. Then, it is NP-complete to decide whether R is a regular resolution refutation.
Back to Sam Buss's publications page.