Samuel R. Buss.
"Pool resolution is NP-hard to recognize."
Archive for Mathematical Logic 48, 8 (2009) 793-798.
Download preprint version: PDF.
Download publisher's version: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s00153-009-0152-4.
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.