Proof-Number Search

From Chessprogramming wiki
Jump to: navigation, 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.

ProofNTree.jpg
DisproofNTree.jpg
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] .

See also

Publications

1988 ...

1990 ...

1995 ...

2000 ...

2005 ...

2010 ...

2015 ...

Forum Posts

External Links

Proof

List of mathematical proofs from Wikipedia
Bijective proof from Wikipedia

Misc

feat.: Terri Lyne Carrington, Roy Hargrove, Munyungo Jackson, Lionel Loucke, Wah Wah Watson
feat.: Tal Wilkenfeld, Greg Phillinganes, Vinnie Colaiuta, Lionel Loueke

References

  1. Paul Klee - Tree Nursery, The Phillips Collection, Wikimedia Commons
  2. Victor Allis (1994). Searching for Solutions in Games and Artificial Intelligence. Ph.D. thesis, University of Limburg, pdf
  3. Victor Allis, Maarten van der Meulen, Jaap van den Herik (1994). Proof-Number Search. Artificial Intelligence, Vol. 66, No. 1
  4. Akihiro Kishimoto, Mark Winands, Martin Müller, Jahn-Takeshi Saito (2012). Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 3
  5. Jaap van den Herik (2012). All is Proof Numbers. ICGA Journal, Vol. 35, No. 3 (editorial)
  6. Akihiro Kishimoto, Mark Winands, Martin Müller, Jahn-Takeshi Saito (2012). Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 3
  7. Victor Allis (1994). Searching for Solutions in Games and Artificial Intelligence. Ph.D. thesis, University of Limburg
  8. Akihiro Kishimoto, Mark Winands, Martin Müller, Jahn-Takeshi Saito (2012). Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 3
  9. Martin Schijf (1993). Proof-number Search and Transpositions. M.Sc. thesis, Leiden University
  10. Dennis Breuker (1998). Memory versus Search in Games. Ph.D. thesis, Maastricht University, Chapter 4: The pn2-search algorithm
  11. Masahiro Seo (1995). The C* Algorithm for AND/OR Tree Search and Its Application to a Tsume-Shogi Program. M.Sc. thesis, University of Tokyo, ps
  12. Masahiro Seo, Hiroyuki Iida, Jos Uiterwijk (2001). The PN*-Search Algorithm: Applications to Tsume-Shogi. Artificial Intelligence, Vol. 129, Nos. 1-2
  13. Richard Korf (1993). Linear-Space Best-First Search. Artificial Intelligence, Vol. 62, No. 1, pdf
  14. Ayumu Nagai (2002). Df-pn Algorithm for Searching AND/OR Trees and Its Applications. Ph.D. thesis, University of Tokyo
  15. Mark Winands, Jos Uiterwijk, Jaap van den Herik (2002). PDS-PN: A new proofnumber search algorithm: Application to Lines of Action. CG 2002, pdf
  16. Akihiro Kishimoto, Yoshiyuki Kotani (1999). Parallel AND/OR tree search based on proof and disproof numbers. 5th Game Programming Workshop
  17. Tomoyuki Kaneko (2010). Parallel Depth First Proof Number Search. AAAI 2010
  18. Akihiro Kishimoto, Mark Winands, Martin Müller, Jahn-Takeshi Saito (2012). Game-Tree Search using Proof Numbers: The First Twenty Years. ICGA Journal, Vol. 35, No. 3
  19. 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
  20. Charles Elkan (1989). Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving. IJCAI 1989, pdf
  21. Akihiro Kishimoto, Martin Müller (2003). Df-pn in Go: An Application to the One-Eye Problem. Advances in Computer Games 10, pdf
  22. Jonathan Schaeffer, Neil Burch, Yngvi Björnsson, Akihiro Kishimoto, Martin Müller, Rob Lake, Paul Lu, Steve Sutphen (2007). Checkers is Solved. Science, Vol. 317, no. 5844
  23. Jonathan Schaeffer, Yngvi Björnsson, Neil Burch, Akihiro Kishimoto, Martin Müller, Rob Lake, Paul Lu, Steve Sutphen (2005). Solving Checkers. IJCAI 2005
  24. Dennis Breuker, Victor Allis, Jaap van den Herik (1994). 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
  25. Sjeng : Download / proof.c
  26. Re: A new(?) technique to recognize draws by Dan Andersson, CCC, June 01, 2002
  27. Tsumego at Sensei's Library
  28. Modal logic from Wikipedia
  29. Dovetailing (computer science) from Wikipedia

Up one level