Proof number search

from Wikipedia, the free encyclopedia

Proof-number search (short PN search) or proof number search is a Spielbaum- search algorithm provided by Victor Allis , originally to solve the game Connect Four and Qubic , was invented. Applications are mainly the endgame solution and sub-goals during the game. The method is particularly suitable for problems which require a large number of moves to be solved, to which the defending player only has a small number of meaningful replies (forced moves). While in the classic alpha-beta searchthe entire game tree is evaluated down to a previously defined depth, the PN search can also find proving or disproving subtrees at an early stage, which are deep but not branching out much. (More precisely: only comparatively few terminal positions have to be evaluated for their proof or refutation.)

algorithm

To apply the algorithm, a binary goal is defined (e.g. player on the move wins) and the game tree is transformed into an and-or tree . This is easily possible by considering maximizing nodes as OR nodes and minimizing nodes as AND nodes (cf. Minimax algorithm ).

Numbers for the evidence (proof numbers) and counter-evidence (disproof numbers) of nodes are entered in the node and updated during the search. They are defined as the lower bound of the nodes still to be expanded in order to achieve a proof or counter-proof. For an AND node, the evidence number is calculated as the sum of the evidence number of all child nodes. (To prove an AND node, all child nodes must be proven.) The refutation number is the minimum of the refutation numbers of all child nodes. (For a refutation, the refutation of a child node is sufficient.) Correspondingly, for an OR node, the result is the proof number as the minimum of the proof numbers of all children and the refutation number as the sum of the refutation numbers of all children. For end nodes that can be proven according to the rules of the game, the proof number is set to 0 and the refuting number to ∞. If the end node can be refuted, the proof number ∞ and the refutation number are 0. Inner nodes of the search tree that are not yet expanded are initialized to an estimated value, in the simplest case both numbers to 1.

End nodes are now expanded step by step, the proof or refutation of which most likely contribute to solving the root node. The heuristic that selects this so-called most proving node (MPN) is based on the evidence and refutation numbers carried along in each node of the tree: Starting from the root node, the child with the smallest evidence number is selected for each OR node, while with AND- Node descends to the child node with the smallest rebuttal number. The end node reached in this way is the MPN and is expanded in the next step.

The following points are processed in one iteration:

  1. Choosing an MPN.
  2. Expansion. A child node is created for every valid move.
  3. Evaluation. Evidence and rebuttal numbers are assigned to the new child nodes.
  4. Update. The evidence and rebuttal numbers of all previous nodes up to the root are recalculated.

The algorithm terminates when the proof number / refutation number of the root node has the value 0 and this is thus proven / refuted.

Extensions

A decisive disadvantage of the PN search is the memory consumption, which increases continuously as the search continues. The complexity of the solvable problems is therefore limited by the available working memory. However, there are variants that loosen this limitation and can evaluate significantly more positions, e.g. B. PN ^ 2, PDS-PN.

See also

literature

swell

  1. ^ Mark HM Winands, Jos WHM Uiterwijk, and H. Jaap van den Herik: PDS-PN: A New Proof-Number Search Algorithm . (PDF) In: Lecture Notes in Computer Science . 2003.