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.