On Computation Complexity of True Proof Number Search
This is an important theoretical result for researchers and practitioners working with proof number search, establishing a fundamental computational limit for arbitrary DAGs.
This paper demonstrates that computing true proof and disproof numbers for proof number search in arbitrary directed acyclic graphs is NP-hard. This was proven by reducing the problem to SAT, indicating its computational complexity.
We point out that the computation of true \emph{proof} and \emph{disproof} numbers for proof number search in arbitrary directed acyclic graphs is NP-hard, an important theoretical result for proof number search. The proof requires a reduction from SAT, which demonstrates that finding true proof/disproof number for arbitrary DAG is at least as hard as deciding if arbitrary SAT instance is satisfiable, thus NP-hard.