On Computation Complexity of True Proof Number Search

TL;DR

This paper proves that computing true proof and disproof numbers in proof number search for arbitrary DAGs is NP-hard, establishing a significant theoretical complexity barrier for this search method.

Contribution

It provides the first NP-hardness proof for calculating true proof and disproof numbers in arbitrary directed acyclic graphs, via a reduction from SAT.

Findings

Proof of NP-hardness for proof number computation in DAGs

Reduction from SAT problem demonstrates computational difficulty

Establishes theoretical limits for proof number search methods

Abstract

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.