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.
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.