Proof-number search (short: PN search) is a game tree search algorithm invented by

Victor Allis Louis Victor Allis (born 19 May 1965) is a Dutch computer scientist working in the artificial intelligence (AI) field. In his graduate work, he revealed AI solutions for Connect Four, Qubic, and Gomoku. His dissertation introduced two new game s ...

, with applications mostly in endgame solvers, but also for sub-goals during games. Using a binary goal (e.g. first player wins the game), game trees of two-person

perfect-information game In economics, perfect information (sometimes referred to as "no hidden information") is a feature of perfect competition. With perfect information in a market, all consumers and producers have complete and instantaneous knowledge of all market pr ...

s can be mapped to an

and–or tree An and–or tree is a graphical representation of the reduction of Computational problem, problems (or goals) to Logical conjunction, conjunctions and disjunctions of subproblems (or subgoals). Example The and-or tree: represents the Candidate s ...

. Maximizing nodes become OR-nodes, minimizing nodes are mapped to AND-nodes. For all nodes proof and disproof numbers are stored, and updated during the search. To each node of the partially expanded game tree the proof number and disproof number are associated. A proof number represents the minimum number of leaf nodes which have to be proved in order to prove the node. Analogously, a disproof number represents the minimum number of leaves which have to be disproved in order to disprove the node. Because the goal of the tree is to prove a forced win, winning nodes are regarded as proved. Therefore, they have proof number 0 and disproof number ∞. Lost or drawn nodes are regarded as disproved. They have proof number ∞ and disproof number 0. Unknown leaf nodes have a proof and disproof number of unity. The proof number of an internal AND node is equal to the sum of its children's proof numbers, since to prove an AND node all the children have to be proved. The disproof number of an AND node is equal to the minimum of its children's disproof numbers. The disproof number of an internal OR node is equal to the sum of its children's disproof numbers, since to disprove an OR node all the children have to be disproved. Its proof number is equal to the minimum of its children's proof numbers. The procedure of selecting the most-proving node to expand is the following. We start at the root. Then, at each OR node the child with the lowest proof number is selected as successor, and at each AND node the child with the lowest disproof number is selected as successor. Finally, when a leaf node is reached, it is expanded and its children are evaluated. The proof and disproof numbers represent lower bounds on the number of nodes to be evaluated to prove (or disprove) certain nodes. By always selecting the most proving (disproving) node to expand, an efficient search is generated. Some variants of proof number search like dfPN, PN², PDS-PN{{cite journal , author=Mark H.M. Winands, Jos W.H.M. Uiterwijk, and H. Jaap van den Herik , title=PDS-PN: A New Proof-Number Search Algorithm , journal=Lecture Notes in Computer Science , year=2003 , url=https://dke.maastrichtuniversity.nl/m.winands/documents/PDSPNCG2002.pdf have been developed to address the quite big memory requirements of the algorithm.

References

Further reading