Preprint:

    Samuel R. Buss.
    "Pool resolution is NP-hard to recognize."
    To appear in Archive for Mathematical Logic.

    Download preprint version: PDF.       

Abstract:  A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.

Back to Sam Buss's publications page.