¶ Checkers ist gelöst (Checkers is Solved)
Checkers (im Deutschen als die anglo-amerikanische Variante von Dame bekannt) ist ein strategisches Brettspiel für zwei Spieler. Im Jahr 2007 wurde durch das Programm Chinook der Beweis erbracht, dass das Spiel bei perfektem Spiel von beiden Seiten unweigerlich in einem Unentschieden (Draw) endet. [1]
Das Lösen von Checkers gilt als einer der bedeutendsten Meilensteine in der Geschichte der Künstlichen Intelligenz und der Spieltheorie, da der Suchraum mit Positionen um Größenordnungen komplexer ist als bei zuvor gelösten Spielen wie Vier gewinnt oder Mühle. [2]
Das Ergebnis: Checkers ist schwach gelöst (weakly solved). Das bedeutet, das spieltheoretische Ergebnis der Startposition ist bekannt (Unentschieden) und es existiert eine Strategie, um dieses Ergebnis gegen jeden beliebigen Gegner zu erreichen. [1:1]
¶ Historischer Kontext
Die Geschichte der Computer-Dame reicht zurück bis in die 1950er Jahre zu Arthur Samuel, dessen Programm bereits 1962 einen (selbsternannten) Meister schlug. Der entscheidende Durchbruch gelang jedoch erst dem Projekt Chinook an der University of Alberta unter der Leitung von Jonathan Schaeffer. [2:1]
Das Ziel war zunächst, den menschlichen Weltmeister Marion Tinsley zu schlagen. Tinsley galt als unbesiegbar und hatte in über 40 Jahren nur drei Partien verloren. In den Matches 1992 und 1994 lieferte sich Chinook enge Duelle mit Tinsley. Nach Tinsleys Rücktritt und Tod verlagerte sich das Ziel des Projekts. Anstatt nur "besser als Menschen" zu spielen, sollte das Spiel mathematisch perfektioniert und gelöst werden. [1:2]
¶ Regeln und Aufbau
Checkers wird auf einem Brett gespielt (identisch zum Schachbrett).
Abb. 1: Exemplarischer Verlauf einer Standard-Eröffnung mit Zwangszug (Quelle: Eigene Darstellung).
Die wichtigsten Regeln, die die Komplexität beeinflussen [2:2]:
- Steine: 12 Steine pro Spieler (Weiß und Schwarz).
- Zug: Einfache Steine ziehen ein Feld diagonal vorwärts.
- Könige: Erreichen Steine die gegnerische Grundlinie, werden sie zu Königen und können ein Feld vorwärts oder rückwärts ziehen.
- Schlagzwang: Wenn ein Schlagzug möglich ist, muss er ausgeführt werden. Diese Regel reduziert den Verzweigungsfaktor (Branching Factor) des Spielbaums erheblich und ist essenziell für die Lösbarkeit.
¶ Komplexität
Um ein Spiel vollständig zu lösen, muss der riesige Zustandsraum bewältigt werden. Schaeffer et al. definierten hierfür verschiedene Härtegrade.
Die folgende Tabelle ordnet Checkers in diesen Kontext ein und verdeutlicht den massiven Anstieg der Komplexität im Vergleich zu anderen, bereits gelösten Spielen [2:3]:
- Suchraum-Größe (Space Complexity): Die Anzahl der möglichen legalen Positionen beträgt bei Checkers ca. (500 Trillionen).
- Entscheidungs-Komplexität (Decision Complexity): Diese wird als "hoch" eingestuft, da es schwierig ist, korrekte Züge allein durch Heuristiken zu bestimmen.
| Spiel | Suchraum (Positionen) | Status | Gelöst durch |
|---|---|---|---|
| Vier gewinnt | \approx 10^ | Stark gelöst | Allis (1988) |
| Mühle | \approx 10^ | Stark gelöst | Gasser (1993) |
| Checkers | Schwach gelöst | Schaeffer et al. (2007) | |
| Schach | \approx 10^ | Ungelöst | - |
¶ Einordnung des Ergebnisses
Der Unterschied zwischen den Lösungsgraden ist entscheidend:
- Stark gelöst (Strongly solved): Für jede theoretisch mögliche Stellung auf dem Brett ist das Ergebnis und der perfekte Zug bekannt (wie bei Mühle).
- Schwach gelöst (Weakly solved): Das Ergebnis ist nur für die Startposition bekannt (hier: Remis), und das Programm besitzt eine Strategie, dieses Ergebnis gegen jeden Gegner zu erzwingen. Es kennt jedoch nicht zwingend die Antwort auf jede irrelevante Nebenvariante, die im perfekten Spiel nie vorkommen würde. [2:4]
Checkers ist das mit Abstand komplexeste Spiel, das bisher gelöst wurde – der Suchraum ist etwa eine Million Mal größer als der von Vier gewinnt. Während dieser Meilenstein erreicht ist, bleibt Schach in weiter Ferne: Mit geschätzten Positionen ist der Suchraum von Schach nochmals um Quadratwurzel-Dimensionen größer, weshalb es ohne neue technologische Paradigmen auf sehr lange Zeit ungelöst bleiben wird. [1:3]
¶ Lösungsansatz: Der hybride Beweis
Da der Zustandsraum von Positionen zu gigantisch ist, um ihn "brute force" vollständig zu durchsuchen (was für ein "starkes Lösen" nötig wäre), nutzte das Team einen hybriden Ansatz. Dieser besteht aus drei Komponenten, die wie eine Sanduhr ineinandergreifen. Die breite Basis (Endspiel-Datenbanken), die schmale Taille (Vorwärtssuche) und der breite Trichter oben (Eröffnungsanalyse). [1:4]
¶ 1. Endspiel-Datenbanken (Backward Search)
Das Fundament des Beweises bildet das perfekte Wissen über alle Stellungen mit wenigen Steinen. Hierfür wurde keine Heuristik verwendet, sondern die Retrograde Analyse. Man beginnt bei den terminalen Spielzuständen (Sieg/Niederlage) und rechnet von dort aus rückwärts.
¶ Funktionsweise
Der Algorithmus startet mit trivialen Stellungen (z.B. 1 Stein gegen 0 Steine = Sieg). Basierend auf diesen Ergebnissen werden alle Stellungen mit 2 Steinen gelöst, dann 3, und so weiter, bis die Grenze der Rechenkapazität erreicht ist.
- Umfang: Für Checkers wurden alle Positionen mit Steinen auf dem Brett vollständig gelöst.
- Datenmenge: Diese Datenbank umfasst (39 Billionen) Positionen. [1:5]
- Komprimierung: Um diese gewaltige Datenmenge nutzbar zu machen, wurde ein spezieller Kompressionsalgorithmus entwickelt, der durchschnittlich 154 Positionen in einem einzigen Byte speichern kann. [1:6]
Perfekte Information durch Lookup: Die Datenbank fungiert als Orakel. Sobald die Vorwärtssuche eine Stellung mit 10 oder weniger Steinen erreicht, wird die Suche sofort abgebrochen. Ein einfacher Datenbank-Zugriff liefert augenblicklich das mathematisch bewiesene Ergebnis (Sieg, Remis oder Niederlage), was die benötigte Suchtiefe drastisch reduziert. [2:5]
¶ 2. Vorwärtssuche (Forward Search)
Für die Startphase und das Mittelspiel (alles mit mehr als 10 Steinen) musste eine komplexe Sucharchitektur entwickelt werden. Diese teilte sich in zwei Rollen auf. Es gibt den "Manager", der den Überblick behält, und die "Solver", die die Arbeit erledigen. [1:7]
Abb. 2: Schematische Visualisierung der Interaktion (Quelle: Eigene Darstellung, basierend auf Schaeffer et al. [1:8]). Hinweis: Die Animation ist symbolisch und dient nur der Veranschaulichung; die echten Rechenzeiten pro Knoten liegen zwischen 15s und 100s.
¶ A. Der Proof-Tree Manager (Das Gehirn)
Der Manager koordiniert den gesamten Beweisprozess und verwaltet die "Master-Kopie" des Beweisbaums. Er fungiert als zentrale Schaltstelle für das Netzwerk von durchschnittlich 50 parallel arbeitenden Computern. [1:9]
Seine Aufgaben sind weitaus komplexer als nur Arbeit zu verteilen:
-
Priorisierung durch Proof Number Search (PNS):
Der Manager nutzt den PNS-Algorithmus, um eine priorisierte Liste von Knoten zu erstellen, die untersucht werden müssen. Er sucht dabei stets nach dem "Weg des geringsten Widerstands" im Suchbaum, um eine Position zu beweisen oder zu widerlegen. [1:10] -
Iterative Suche über den Fehler ():
Dies ist eine der innovativsten Techniken des Projekts. Statt wie üblich die Suchtiefe iterativ zu erhöhen (Iterative Deepening), iterierte der Manager über den heuristischen Fehler.- Der Manager setzt einen Schwellenwert (Epsilon).
- Er nimmt vorläufig an, dass alle heuristischen Bewertungen "Gewinne" und alle "Verluste" sind.
- Unter dieser Annahme wird versucht, den Beweis zu führen. Gelingt dies, wird erhöht und der Prozess wiederholt, bis der echte Beweis erbracht ist. Dies fokussiert die Rechenleistung zuerst auf die "klaren" Fälle und verfeinert den Beweis schrittweise. [1:11]
-
Lösung des GHI-Problems:
Ein kritisches Problem in Spielbäumen ist die Graph-History Interaction (GHI). Da dieselbe Brettstellung über verschiedene Zugfolgen erreicht werden kann (Transpositionen), ist es schwierig, Remis durch Zugwiederholung korrekt zu erkennen. Standard-Algorithmen können hier fälschlicherweise ein Remis annehmen. Der Manager implementierte einen neuen Algorithmus, um Zyklen und Wiederholungen im Beweisbaum korrekt als Remis oder Nicht-Remis zu klassifizieren. [1:12] -
Datenhaltung:
Der Manager speichert nur den oberen Teil des Beweisbaums permanent auf der Festplatte (ca. Positionen). Sobald eine Anfrage das Ende dieses gespeicherten Baums erreicht, wird dynamisch ein Solver beauftragt, die Linie weiter bis in die Endspiel-Datenbanken zu verfolgen. Dies sparte massiv Speicherplatz (Terabytes), erforderte aber das erneute Berechnen von Zwischenschritten. [1:13]
¶ B. Die Solver (Die Arbeiter)
Der Manager sendet einzelne Positionen an ein Netzwerk von Dutzenden Computern (im Jahr 2007 waren es ca. 50 parallel). Die Solver folgen dabei einem strikten Protokoll. Zuerst wird Chinook für eine schnelle Einschätzung genutzt (ca. 15s). Findet dieser keinen Beweis, wird der rechenintensivere Depth-first PNS Solver gestartet (ca. 100s). [1:14]
Die Solver melden ihre Ergebnisse in drei Kategorien zurück:
- Proven (Bewiesen): Das exakte Ergebnis (Sieg, Remis, Niederlage).
- Partially Proven: Eine Schranke (z.B. "mindestens Remis"). Dies ist oft ausreichend für den Beweisbaum.
- Heuristic: Eine bloße Schätzung, falls das Zeitlimit ohne Beweis abgelaufen ist. Der Manager nutzt diese Schätzung, um die Priorität des Knotens für spätere Untersuchungen neu zu berechnen. [1:15]
| Algorithmus | Funktionsweise | Stärke |
|---|---|---|
| Alpha-Beta | Der klassische Schachcomputer-Ansatz. Sucht tief (17-23 Halbzüge) und nutzt eine heuristische Bewertungsfunktion. (Laufzeit: ~15s) | Gut im Abschätzen von Positionen, die noch nicht bewiesen sind. Findet taktische Fallen. |
| Depth-first PNS | Depth-first Proof-number search. Ein Algorithmus, der versucht, den Beweisbaum so klein wie möglich zu halten. (Laufzeit: ~100s) | Extrem effizient darin, forcierte Gewinn- oder Verlustwege zu beweisen, ohne unnötige Varianten zu prüfen. |
¶ 3. Eröffnungs-Analyse (Top-Down)
Das bloße "Lösen der Startaufstellung" reichte nicht aus. Da im professionellen Checkers die ersten drei Halbzüge (Plys) oft zufällig vorgegeben sind ("3-Move Ballot"), um bekannte Remis-Varianten zu vermeiden und das Spiel spannender zu gestalten, musste der Beweis robust gegenüber verschiedenen Eröffnungen sein. Es gibt theoretisch rund 300 solcher Eröffnungssequenzen.
Das folgende Diagramm zeigt den Beweisbaum der ersten 3 Halbzüge für 19 relevante Eröffnungen.
Abb. 3: Der Beweisbaum für die ersten 3 Halbzüge (Quelle: Schaeffer et al. [1:16], Fig. 3).
- Reduktion auf 19 Linien: Von den ca. 300 Eröffnungen sind viele durch Zugumstellung (Transpositionen) identisch oder konnten durch eine heuristische Suche (Alpha-Beta) vorab als irrelevant ausgeschlossen werden. Übrig blieben die 19 kritischen Linien in der Grafik.
- Das Ergebnis: Die Standard-Startaufstellung ist ein Remis. Gleichzeitig wurde gezeigt, dass auch die anderen untersuchten Eröffnungen im Remis enden, solange keine Seite einen Fehler macht.
¶ Warum enthält die Grafik eine Verlust-Linie (=L)?
Eine wichtige Beobachtung im Diagramm ist Linie 13 (Zugfolge 12-16, 24-19, 09-13), die in einem Verlust endet. Dies ist für das Verständnis des "3-Move Ballots" entscheidend:
- Im Beweis (Optimale Strategie): Der Computer muss diese Linie analysieren, um zu beweisen, dass der Zug
09-13ein Fehler ist. Da Schwarz in derselben Stellung (nach24-19) alternative Züge wie09-14(Linie 14) hat, die das Remis halten, wird ein perfekter Spieler (beim perfekten Spiel vom start aus) die Verlust-Linie 13 niemals wählen. Die übergeordnete Eröffnung gilt somit als "gelöst" (Remis), solange mindestens ein Pfad existiert, der nicht verliert. - Im Turnier (Ballot): Würde das Losverfahren diese Zugfolge (inklusive des Fehlers
09-13) erzwingen, müsste der Spieler tatsächlich eine objektiv verlorene Stellung verteidigen. In der Praxis werden solche unfairen Eröffnungen aus dem Lostopf entfernt. Schaeffers Beweis liefert hierfür nun die mathematische Gewissheit: Da Linie 13 nachweislich ein Verlust ist, kann sie im modernen Turnierschach endgültig als unspielbare Eröffnung aus dem Pool gestrichen werden.
Fazit des Algorithmus: Das System ist keine reine "Brute Force" Maschine. Es ist eine elegante Kombination aus Wissen (Endspiel-Datenbanken) und Intelligenz (gezielte Suche im Beweisbaum), die es ermöglichte, einen Suchraum zu bewältigen, der eine Million Mal komplexer ist als alles, was zuvor gelöst wurde.
¶ Synthese: Die Struktur des Suchraums
Zusammenfassend ergibt sich durch die Interaktion der drei Komponenten (Datenbanken, Manager, Solver) eine charakteristische Struktur des gelösten Raums, die in der folgenden Grafik visualisiert wird.
Abb. 4: Visualisierung des Suchraums. Unten (schraffiert) die Endspiel-Datenbanken, darüber der relevante Suchraum der Vorwärtssuche (Quelle: Schaeffer et al. [1:17], Fig. 2).
Die Grafik verdeutlicht die Effizienz des Beweises anhand wichtiger Fachbegriffe [1:18]:
- Endgame Databases (Schraffierter Bereich unten): Alle Positionen mit 1 bis 10 Steinen sind vollständig gelöst. Sobald die Suche diesen Bereich erreicht, ist das Ergebnis sofort bekannt.
- Seeded Line (Zick-Zack-Linie): Die durchgezogene Linie repräsentiert die "beste" Spielvariante, die basierend auf menschlicher Literatur manuell als Startpfad vorgegeben wurde ("Hand-Seeding"). Dies fokussiert die Suche von Beginn an auf relevante Bereiche und verhindert, dass Rechenzeit für offensichtlich unterlegene Varianten verschwendet wird.
- Relevant Search Space (Inneres Oval): Der Beweis musste nicht den gesamten theoretischen Raum (äußere Kurve) durchsuchen. Durch "Pruning" (Abschneiden irrelevanter Zweige) beschränkte sich die Arbeit auf den inneren Bereich (gepunktet).
- Stored Boundary (Gepunktete Linie): Dies ist die Schnittstelle im Beweisbaum.
- Oberhalb der Linie agiert der Manager: Er speichert die Struktur des Beweisbaums permanent auf der Festplatte.
- Unterhalb der Linie agieren die Solver: Sie berechnen temporäre Ergebnisse um die Lücken zu den Datenbanken zu schließen, deren Details aber nicht dauerhaft gespeichert werden müssen, um Speicherplatz zu sparen.
¶ Algorithmus und Visualisierung
Um die enorme Tiefe des Spiels zu bewältigen, müssen die Solver effizient entscheiden, wann sie rechnen und wann sie "wissen". Das folgende Diagramm zeigt die hybride Logik eines Solvers. Er kombiniert die Datenbank-Abfrage für Steine mit der Alpha-Beta-Suche für komplexe Stellungen. [1:19]
Entscheidungsbaum
Pseudocode
def SolvePosition(pos, alpha, beta, depth):
# 1. Datenbank-Lookup (Endspiel)
if NumberOfPieces(pos) ≤ 10:
return EndgameDatabase.lookup(pos)
# 2. Transposition Table (Cache)
if TranspositionTable.contains(pos):
return TranspositionTable.get(pos)
# 3. Vorwärtssuche (Alpha-Beta)
best_value = float('-inf')
for move in GenerateMoves(pos):
# Rekursiver Aufruf
val = -SolvePosition(MakeMove(pos, move),
-beta, -alpha, depth-1)
best_value = max(best_value, val)
alpha = max(alpha, val)
# Pruning (Schnitt)
if alpha ≥ beta:
break
TranspositionTable.store(pos, best_value)
return best_value
¶ Resultate
Die Berechnung lief fast kontinuierlich von 1989 bis 2007. Zum Höhepunkt der Berechnungen waren über 200 Prozessoren parallel im Einsatz. Das Projekt gilt als eine der längsten durchgehenden Berechnungen der Geschichte. [1:20]
¶ Der Beweis in Zahlen
- Das Hauptergebnis: Die Startposition ist ein Remis (Draw). Wenn beide Spieler fehlerfrei spielen, kann niemand gewinnen.
- Datenmenge: Der permanent gespeicherte Beweisbaum ist überraschend klein und umfasst nur ca. Knoten. Dies ist jedoch nur die "Spitze des Eisbergs". Um diese Knoten zu verifizieren, mussten insgesamt etwa Positionen berechnet werden. [1:21]
- Speichereffizienz: Die Endspiel-Datenbanken (39 Billionen Stellungen) wurden extrem effizient komprimiert. Durchschnittlich konnten 154 Positionen in einem einzigen Byte gespeichert werden, was den Gesamtspeicherbedarf auf handhabbare 237 Gigabyte reduzierte. [1:22]
- Längste Gewinnführung: Die längste analysierte perfekte Spielvariante umfasste 154 Halbzüge (Ply), bevor eine Datenbank-Position erreicht wurde. [1:23]
¶ Korrektheit und Fehleranalyse
Ein zentrales Problem bei Berechnungen über 18 Jahre ist die Zuverlässigkeit. Wie kann man sicher sein, dass kein Hardwarefehler (Bit-Flip) oder Software-Bug das Ergebnis verfälscht hat?
Das Team argumentiert statistisch:
Selbst wenn ein Fehler tief im Baum auftreten würde (z.B. bei Tiefe 40), ist die Wahrscheinlichkeit, dass dieser Fehler das Ergebnis an der Wurzel (Startposition) ändert, "verschwindend gering" (), da viele alternative Pfade zum gleichen Ergebnis führen und Fehler sich oft gegenseitig aufheben oder in irrelevanten Zweigen passieren. [1:24]
¶ Wissenschaftliche Bedeutung
Checkers ist das komplexeste Spiel, das bisher gelöst wurde. Der Erfolg demonstriert weniger "menschliche Intelligenz" im Computer, sondern die Macht von massiver Suche kombiniert mit Wissen (Datenbanken).
- Paradigmenwechsel: Anstatt menschliches Wissen mühsam in Regeln zu kodieren (wie bei klassischen Expertensystemen), generierte Chinook sein Wissen durch das vollständige Lösen von Teilproblemen (Endspiele) selbst. [1:25]
- Grenzen: Während Checkers (Dame) gelöst ist, bleibt Schach aufgrund seines weitaus größeren Zustandsraums () auf absehbare Zeit ungelöst. Die Methoden von Chinook (insbesondere Endspiel-Datenbanken) sind jedoch heute Standard in fast allen starken Spiel-Engines. [1:26]
¶ Referenzen
SCHAEFFER, Jonathan, et al. Checkers is solved. science, 2007, 317. Jg., Nr. 5844, S. 1518-1522. ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎
SCHAEFFER, Jonathan; LAKE, Robert. Solving the game of checkers. Games of no chance, 1996, 29. Jg., S. 119-133. ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎