真证数搜索的计算复杂性
On Computation Complexity of True Proof Number Search
University of Alberta（阿尔伯塔大学）
摘要：
指出了任意有向无环图中证明数搜索的真\emph{proof}数和真\emph{disproof}数的计算是NP困难的，这是证明数搜索的一个重要理论结果.该证明需要对SAT进行约简，这表明为任意DAG找到真证明/反证数至少与决定任意SAT实例是否可满足一样困难，因此是NP困难的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
