# Proof-Number Search

Home * Search * Proof-Number Search

Paul Klee - Tree Nursery [1]

Proof-Number Search, (Pn-Search, PnS, PNS)
a best-first and-or tree search algorithm designed by Victor Allis for finding the game-theoretical value in game trees [2] . PNS is based on ideas derived from conspiracy number search. While in cn search the purpose is to continue searching until it is unlikely that the minimax value of the root will change, PNS aims at proving the true value of the root [3]. In the fall 2012 issue of the ICGA Journal, about 20 years after its invention, Akihiro Kishimoto, Mark Winands, Martin Müller and Jahn-Takeshi Saito wrote a résumé about PNS and its variants and enhancements, considered a tribute to Victor Allis by editor Jaap van den Herik [4] [5] .

# Algorithm

## Conspiracy Numbers

PNS specializes conspiracy numbers to and-or tree search with binary outcome, with significant reduced memory requirements compared to CnS [6] . MAX-nodes are represented as OR-nodes, MIN-nodes as AND-nodes. A solved tree with value true is called proved, while a solved tree with value false is called disproved. Evaluation of leaves yields in the values of false, true or unknown, the latter can be expanded to become a frontier node. For backpropagation, after expansion, AND-nodes become false if at least one child is false, else unknown if at least one child is unknown, otherwise true. At OR-nodes, false and true are interchanged analogously.

## Proof and Disproof Numbers

The algorithm requires the whole tree in memory to select the next evaluated but yet unknown node to be expanded using two criteria: the potential range of subtree values and the number of nodes which must conspire to prove or disprove that range of potential values. These two criteria enable PNS to treat game trees with a non-uniform branching factor and deep and narrow lines efficiently.

PNS continuously tries to solve the tree by focusing on the potentially shortest solution, i.e., consisting of the least number of nodes. At each step of the search, a node which is part of the potentially shortest solution available is selected and expanded or developed. After expansion, its conspiracy numbers, the proof- and disproof number, are established anew, to update the proof- and disproof numbers of its ancestors. This process of selection, expansion and ancestor update is repeated until either the tree is solved or has run out of time- or memory resources.

## Tree Sample

Following sample, taken from Allis' Ph.D. thesis [7] , illustrates how proof and disproof numbers are assigned and updated to solve the tree.

All frontier nodes (E, F, I, L, M, N and P) have proof number or conspiracy of 1. A terminal node with value true (node K) has proof number 0, with value false (node O), proof number ∞. Internal AND-nodes (B, D, G, H and J) have proof numbers equal to the sum of the proof numbers of their children, internal OR-nodes (A and C) have proof numbers equal to the minimum of the proof numbers of their children. Disproof numbers behave analogously to proof numbers, interchanging the roles of AND-nodes and OR-nodes, and the cardinalities 0 and ∞. Each pair consisting of a smallest proof set and a smallest disproof set has a non-empty intersection.

 And-or tree with proof numbers and disproof numbers

# Pseudo Code

The PNS C-like pseudo code is based on the code given in Game-Tree Search using Proof Numbers: The First Twenty Years by Kishimoto et al. [8] . The domain dependent procedure evaluate assigns one of the values proven, disproven and unknown to node.value.

```void PNS ( Node root ) {
evaluate( root );
setProofAndDisproofNumbers( root );
Node current = root;
while ( root.proof != 0 && root.disproof != 0 && resourcesAvailable() ) {
Node mostProving = selectMostProvingNode( current );
expandNode( mostProving );
current = updateAncestors( mostProving, root );
}
}
```

## Set Numbers

```void setProofAndDisproofNumbers( Node n ) {
if ( n.expanded ) { /* interior node */
if ( n.type == AND ) {
n.proof = 0;  n.disproof = ∞;
for (each child c of n) {
n.proof += c.proof;
n.disproof = min(n.disproof, c.disproof);
}
} else { /* OR node */
n.proof = ∞;  n.disproof = 0;
for (each child c of n) {
n.disproof += c.disproof;
n.proof = min(n.proof, c.proof);
}
}
} else { /* terminal node or none terminal leaf */
switch( n.value ) {
case disproven: n.proof = ∞; n.disproof = 0; break;
case proven:    n.proof = 0; n.disproof = ∞; break;
case unknown:   n.proof = 1; n.disproof = 1; break;
}
}
}
```

## Select

```Node selectMostProvingNode( Node n ) {
while ( n.expanded ) {
int value = ∞;
Node best;
if ( n.type == AND ) {
for (each child c of n) {
if ( value > c.disproof ) {
best = c;
value = c.disproof;
}
}
} else { /* OR node */
for (each child c of n) {
if ( value > c.proof ) {
best = c;
value = c.proof;
}
}
}
n = best;
}
return n;
}
```

## Expand

```void expandNode( Node n ) {
generateChildren( n );
for (each child c of n) {
evaluate( c );
setProofAndDisproofNumbers( c );
if ( n.type == AND ) {
if ( c.disproof == 0 ) break;
} else {  /* OR node */
if ( c.proof == 0 ) break;
}
}
n.expanded = true;
}
```

## Update Ancestors

```Node updateAncestors( Node n, Node root ) {
while( n != root ) {
int oldProof = n.proof;
int oldDisproof = n.disproof;
setProofAndDisproofNumbers( n );
if ( n.proof == oldProof && n.disproof == oldDisproof )
return n;
n = n.parent;
}
setProofAndDisproofNumbers( root );
return root;
}
```

# Enhancements

Proof-number search as illustrated above is suited for pure trees, but has issues with games consisting of directed acyclic graphs (transpositions) and even more, directed cyclic graphs (repetitions), already addressed by Martin Schijf in 1993 [9] .

## Pn²

The Pn² search algorithm safes resources by using a second PNS instead of calling evaluate, which child-nodes can be discarded afterwards [10] .

## Depth First

C* and PN*, introduced by Masahiro Seo [11] and Seo et al [12] , transforms a best-first PNS into an iterative deepening depth-first approach df-pn. Moreover, PN* also incorporates ideas from Korf's Linear-Space Best-First Search (RBFS) [13], and is enhanced by methods such as recursive iterative deepening, dynamic evaluation, efficient successor ordering, and pruning by dependency relations.

## PDS

Ayumu Nagai proposed a depth-first variation of PNS dubbed PDS for Proof-number and Disproof-number Search [14] .

## PDS-PN

PDS-PN is a two-level search, which performs a depth-first Proof-number and Disproof-number Search (PDS) at the first level, followed by second level best-first PNS [15] .

## Parallel PNS

Parallel search implementations of PNS were introduced by Akihiro Kishimoto and Yoshiyuki Kotani in 1999 [16] , and by Tomoyuki Kaneko in 2010 [17] .

# Applications

In conjunction with retrograde analysis and alpha-beta, PNS approaches were used to solve various games completely or partial, and to support game playing programs in finding game theoretic solutions. As pointed out by Kishimoto et al. [18] , Victor Allis first used the notion of proof and disproof numbers while analyzing and solving Connect Four, still called conspiracy numbers [19] . Charles Elkan applied proof numbers to theorem proving [20] . In Go, PNS could be applied in Life and death situations [21] , and PNS played an important role in solving Checkers by Jonathan Schaeffer et al. in 2007 [22] [23] .

In Shogi as well in Chess, PNS solves deep tsume-shogi or mate problems. Prover was a PNS implementation for chess, using chess-specific routines of Duck. Provers only goal was searching for mate [24] . Sjeng by Gian-Carlo Pascutto uses Proof-number search in it's suicide and loser's mode [25] .