Pool resolution is NP-hard to recognize
- Author(s): Buss, Samuel R.
- et al.
Published Web Locationhttps://doi.org/10.1007/s00153-009-0152-4
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.