Die Proof Number Search (PNS) ist ein Best-First-Suchalgorithmus, der speziell entwickelt wurde, um in Spielbäumen den spieltheoretischen Wert (Gewinn, Verlust oder Remis) zu beweisen. Er wurde 1994 von L. Victor Allis vorgestellt.
Im Gegensatz zur Alpha-Beta-Suche, die darauf ausgelegt ist, den besten Zug innerhalb einer begrenzten Zeit zu finden, zielt PNS darauf ab, das Ergebnis eines Spiels durch das Finden eines vollständigen Beweisbaums zu erzwingen. Der Algorithmus sucht stets den "Weg des geringsten Widerstands", um eine Stellung zu beweisen oder zu widerlegen.
PNS arbeitet auf einem AND/OR-Baum.
- OR-Knoten: Wir sind am Zug. Es reicht aus, einen einzigen Gewinnzug zu finden, um die Position zu gewinnen (zu "beweisen").
- AND-Knoten: Der Gegner ist am Zug. Wir müssen beweisen, dass wir gegen alle seine Antwortmöglichkeiten gewinnen.
Jeder Knoten n im Baum erhält zwei Werte, die rekursiv berechnet werden:
- Proof Number (pn): Die minimale Anzahl an Blattknoten, die noch expandiert (bewiesen) werden müssen, um zu zeigen, dass Knoten n ein Gewinn ist.
- Disproof Number (dn): Die minimale Anzahl an Blattknoten, die expandiert werden müssen, um zu zeigen, dass Knoten n kein Gewinn (also Verlust oder Remis) ist.
Die Werte werden von den Blättern (Leaves) nach oben zur Wurzel (Root) propagiert.
1. Blattknoten (Terminal Node):
- Ist die Stellung gewonnen: pn=0,dn=∞
- Ist die Stellung verloren: pn=∞,dn=0
- Ist die Stellung unbekannt: pn=1,dn=1 (Standard-Initialisierung)
2. OR-Knoten (eigener Zug):
Um zu gewinnen, reicht ein Kind. Um zu verlieren, müssen alle Kinder verlieren.
pn(n)=c∈children(n)minpn(c)
dn(n)=c∈children(n)∑dn(c)
3. AND-Knoten (gegnerischer Zug):
Um zu gewinnen, müssen wir gegen alle Antworten bestehen. Um zu verlieren, reicht eine Widerlegung des Gegners.
pn(n)=c∈children(n)∑pn(c)
dn(n)=c∈children(n)mindn(c)
Der Algorithmus läuft in einer Schleife, bis die Wurzel gelöst ist (pn=0 oder dn=0) oder die Ressourcen erschöpft sind.
- Selection (Auswahl): Beginnend an der Wurzel wird der Baum durchlaufen. An jedem Knoten wird das Kind gewählt, das zur aktuellen Proof- oder Disproof-Number beigetragen hat (das "most proving child"). Dies wird wiederholt, bis ein Blattknoten erreicht ist.
- Expansion (Erweiterung): Der ausgewählte Blattknoten wird expandiert (seine Kinder werden generiert).
- Evaluation (Bewertung): Die neuen Kinder werden initialisiert (pn=1,dn=1 oder terminale Werte).
- Backpropagation (Aktualisierung): Die neuen Werte werden den Pfad zurück bis zur Wurzel gereicht. Dabei ändern sich die pn und dn Werte der Vorfahren.
Ein Nachteil der klassischen PNS ist der hohe Speicherbedarf, da der gesamte Baum im Speicher gehalten werden muss. Für das Lösen komplexer Spiele (wie Checkers im Projekt Chinook) wurde daher die Variante Df-pn (Depth-first Proof-number search) entwickelt.
Df-pn kombiniert die Idee der Proof Numbers mit der iterativen Tiefensuche. Es nutzt Transposition Tables, um Speicherplatz zu sparen, und berechnet Proof-Numbers dynamisch neu, statt den ganzen Baum zu speichern. Dies war entscheidend für das Lösen von Checkers.