Proof-Number Search, (Pn-Search, PnS, PNS)
a best-firstand-or tree search algorithm designed by Victor Allis for finding the game-theoretical value in game trees ^{[1]} . 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 ^{[2]} .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^{[3]}^{[4]} .

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 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;}

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 deepeningdepth-first approach df-pn. Moreover, PN* also incorporates ideas from Korf'sLinear-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]} .

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]} .

Victor Allis (1988). A Knowledge-Based Approach of Connect Four: The Game is Over, White to Move Wins. M.Sc. thesis, Report No. IR-163, Faculty of Mathematics and Computer Science, Vrije Universteit, Amsterdam

Charles Elkan (1989). Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving. IJCAI 1989, pdf

Ayumu Nagai, Hiroshi Imai (1999). Proof for the Equivalence Between Some Best-First Algorithms and Depth-First Algorithms for AND/OR Trees. Proceedings of the Korea-Japan Joint Workshop on Algorithms and Computation

^Victor Allis (1988). A Knowledge-Based Approach of Connect Four: The Game is Over, White to Move Wins. M.Sc. thesis, Report No. IR-163, Faculty of Mathematics and Computer Science, Vrije Universteit, Amsterdam

^Charles Elkan (1989). Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving. IJCAI 1989, pdf

Home * Search * Proof-Number SearchProof-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

^{[1]}. 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 atprovingthe true value of the root^{[2]}.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^{[3]}^{[4]}.^{[5]}## Table of Contents

## 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 valuetrueis called proved, while a solved tree with valuefalseis called disproved. Evaluation of leaves yields in the values offalse,trueorunknown, the latter can be expanded to become a frontier node. For backpropagation, after expansion, AND-nodes becomefalseif at least one child isfalse, elseunknownif at least one child isunknown, otherwisetrue. At OR-nodes,falseandtrueare 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 toproveordisprovethat 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 valuefalse(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.## Pseudo Code

The PNS C-like pseudo code is based on the code given inGame-Tree Search using Proof Numbers: The First Twenty Yearsby Kishimoto et al.^{[8]}. The domain dependent procedure evaluate assigns one of the valuesproven,disprovenandunknownto node.value.## Set Numbers

## Select

## Expand

## Update Ancestors

## 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²

ThePn²search algorithm safes resources by using a second PNS instead of callingevaluate, which child-nodes can be discarded afterwards^{[10]}.## Depth First

C* andPN*, introduced by Masahiro Seo^{[11]}and Seo et al^{[12]}, transforms a best-first PNS into an iterative deepening depth-first approachdf-pn. Moreover, PN* also incorporates ideas from Korf'sLinear-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 dubbedPDSfor Proof-number and Disproof-number Search^{[14]}.## PDS-PN

PDS-PNis 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]}.## See also

## Publications

## 1988 ...

1988).A Knowledge-Based Approach of Connect Four: The Game is Over, White to Move Wins. M.Sc. thesis, Report No. IR-163, Faculty of Mathematics and Computer Science, Vrije Universteit, Amsterdam1989).Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving. IJCAI 1989, pdf## 1990 ...

1991).Proof-Number Search.Technical Reports in Computer Science, CS 91-01. Department of Computer Science, University of Limburg. ISSN 0922-8721.1992).Qubic Solved Again. Heuristic Programming in Artificial Intelligence 3: The Third Computer Olympiad1993).Proof-number Search and Transpositions. M.Sc. thesis, Leiden University1994).Searching for Solutions in Games and Artificial Intelligence. Ph.D. thesis, University of Limburg, pdf1994).How to Mate: Applying Proof-Number Search. Advances in Computer Chess 7, reprint as Mate in 38: Applying Proof-Number Search from Ed Schroder's Programmer's Stuff site1994).Proof-Number Search. Artificial Intelligence, Vol. 66, No. 11994).Proof-Number Search and Transpositions. ICCA Journal, Vol. 17, No. 2## 1995 ...

1995).The C* Algorithm for AND/OR Tree Search and Its Application to a Tsume-Shogi Program. M.Sc. thesis, University of Tokyo, ps1998).Memory versus Search in Games. Ph.D. thesis, Maastricht University, Chapter 3: The proof-number search algorithm, Chapter 4: The pn2-search algorithm1998).A new AND/OR Tree Search Algorithm Using Proof Number and Disproof Number. Complex Games Lab Workshop, Tsukuba1999).A New Depth-First-Search Algorithm for AND/OR Trees. M.Sc. thesis, University of Tokyo1999).Proof for the Equivalence Between Some Best-First Algorithms and Depth-First Algorithms for AND/OR Trees. Proceedings of the Korea-Japan Joint Workshop on Algorithms and Computation1999).Parallel AND/OR tree search based on proof and disproof numbers. 5th Game Programming Workshop1999).Application of df-pn+ to Othello endgames. 5th Game Programming Workshop » Othello## 2000 ...

2000).Abstract Proof Search. CG 2000, pdf2001).The PN*-Search Algorithm: Applications to Tsume-Shogi.Artificial Intelligence, Vol. 129, Nos. 1-22001).The Performance of PN*, PDS, and PN Search on 6x6 Othello and Tsume-Shogi. Advances in Computer Games 92001).The PN2-Search Algorithm. Advances in Computer Games 92001).PN, PN2 and PN* in Lines of Action. 6th Computer Olympiad Workshop, pdf » Lines of Action2001).AND/OR-tree Search Algorithms in Shogi Mating Search. ICGA Journal, Vol. 24, No. 42001).Proof-Set Search. Technical Report TR 01-09, University of Alberta CiteSeerX^{[26]}2002).Proof-Set Search. CG 20022002).PDS-PN: A New Proof-Number Search Algorithm: Application to Lines of Action. CG 2002 » Lines of Action2002).Df-pn Algorithm for Searching AND/OR Trees and Its Applications. Ph.D. thesis, University of Tokyo2002).Proof for the Equivalence Between Some Best-First Algorithms and Depth-First Algorithms for AND/OR Trees. IEICE transactions on information and systems2003).Df-pn in Go: An Application to the One-Eye Problem. Advances in Computer Games 10, pdf » Go^{[27]}2004).An Effective Two-Level Proof-Number Search Algorithm. Theoretical Computer Science. Vol. 313, No.3, pp. 511-525. ps2004).Informed Search in Complex Games. Ph.D. thesis, Universiteit Maastricht, Received the 2004 ChessBase Best-Publication Award, pdf, Chapter 4 - Proof-Number Search Algorithm, Chapter 5 - An Effective Two-Level Proof-Number Search Algorithm## 2005 ...

2005).Correct and Efficient Search Algorithms in the Presence of Repetitions. Ph.D. thesis, University of Alberta, Received the 2005 ChessBase Best-Publication Award, pdf2005).A Solution to the GHI Problem for Depth-First Proof-Number Search. 7th Joint Conference on Information Sciences (JCIS2003), pp. 489 - 492, pdf » Graph History Interaction2005).Solving Checkers. IJCAI 2005, pdf2006).Intelligent Search Techniques Proof-Number Search. MICC/IKAT Universiteit Maastricht2006).Monte-Carlo Proof-Number Search for Computer Go. CG 20062006).Improving Depth-first PN-Search: 1 + ε Trick. CG 2006, pdf2007).Lambda Depth-First Proof-Number Search and Its Application to Go. IJCAI 2007, pdf2008).A New Proof-Number Calculation Technique for Proof-Number Search. CG 20082008).About the Completeness of Depth-First Proof-Number Search. CG 20082008).Weak Proof-Number Search. CG 20082009).AND-OR Tree Search Algorithms for Domains with Uniform Branching Factors. Ph.D. thesis, University of Tokyo2009).Randomized Parallel Proof-Number Search. Advances in Computer Games 12, pdf2009).Enhancements of Proof Number Search in Connect6. IEEE Control and Decision Conference## 2010 ...

2010).Relevance-Zone-Oriented Proof Search for Connect6. Ph.D. thesis2010).Evaluation-Function Based Proof-Number Search. CG 2010, pdf2010).Job-Level Proof-Number Search for Connect6. CG 20102010).Relevance-Zone-Oriented Proof Search for Connect6. IEEE Transactions on Computational Intelligence and AI in Games, Vol. 2, No. 3 » Connect62010).Parallel Depth First Proof Number Search. AAAI 20102011).Solving Breakthrough with Race Patterns and Job-Level Proof Number Search. Advances in Computer Games 13 » Breakthrough (Game)2012).Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 32012).Minimal Proof Search for Modal Logic K Model Checking. CoRR, July 2012^{[28]}2012).Multiple-Outcome Proof Number Search. ECAI 20122013).Parallel Dovetailing and its Application to Depth-First Proof-Number Search. ICGA Journal, Vol. 36, No. 1^{[29]}2013).Solving Games and All That. Ph.D. thesis, 2.4 Proof Number Search2013).Job-Level Proof Number Search. IEEE Transactions on Computational Intelligence and AI in Games, Vol. 5, No. 12013).Scalable Parallel DFPN Search. CG 2013, pdf2014).Solved Openings in Losing Chess. ICGA Journal, Vol. 37, No. 2 » Losing Chess## 2015 ...

2015).Reducing the Seesaw Effect with Deep Proof Number Search. Advances in Computer Games 142017).Deep df-pn and its Efficient Implementations. Advances in Computer Games 15## Forum Posts

## External Links

feat.Terri Lyne Carrington, Roy Hargrove, Munyungo Jackson, Lionel Loucke, Wah Wah Watson

## References

1994).Searching for Solutions in Games and Artificial Intelligence. Ph.D. thesis, University of Limburg, pdf1994).Proof-Number Search. Artificial Intelligence, Vol. 66, No. 12012).Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 32012).All is Proof Numbers. ICGA Journal, Vol. 35, No. 3 (editorial)2012).Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 31994).Searching for Solutions in Games and Artificial Intelligence. Ph.D. thesis, University of Limburg2012).Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 31993).Proof-number Search and Transpositions. M.Sc. thesis, Leiden University1998).Memory versus Search in Games. Ph.D. thesis, Maastricht University, Chapter 4: The pn2-search algorithm1995).The C* Algorithm for AND/OR Tree Search and Its Application to a Tsume-Shogi Program. M.Sc. thesis, University of Tokyo, ps2001).The PN*-Search Algorithm: Applications to Tsume-Shogi.Artificial Intelligence, Vol. 129, Nos. 1-21993).Linear-Space Best-First Search.Artificial Intelligence, Vol. 62, No. 1, pdf2002).Df-pn Algorithm for Searching AND/OR Trees and Its Applications. Ph.D. thesis, University of Tokyo2002).PDS-PN: A new proofnumber search algorithm: Application to Lines of Action. CG 2002, pdf1999).Parallel AND/OR tree search based on proof and disproof numbers. 5th Game Programming Workshop2010).Parallel Depth First Proof Number Search. AAAI 20102012).Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 31988).A Knowledge-Based Approach of Connect Four: The Game is Over, White to Move Wins. M.Sc. thesis, Report No. IR-163, Faculty of Mathematics and Computer Science, Vrije Universteit, Amsterdam1989).Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving. IJCAI 1989, pdf2003).Df-pn in Go: An Application to the One-Eye Problem. Advances in Computer Games 10, pdf2007).Checkers is Solved. Science, Vol. 317, no. 58442005).Solving Checkers. IJCAI 20051994).How to Mate: Applying Proof-Number Search. Advances in Computer Chess 7, reprint as Mate in 38: Applying Proof-Number Search from Ed Schroder's Programmer's Stuff site## What links here?

Up one level