Legespiele lösen mittels SAT- / SMT-Solver

Um ein Puzzle mit dem Computer lösen zu können, benötigen wir Programm, das eine Lösung (oder alle Lösungen) für dieses Puzzle erzeugt. Leider können wir oft kein fertiges Programm für diesen Zweck finden und müssen selbst programmieren. Ganz einfach ist das nicht, da für eine Lösung eines Puzzles häufig extrem viele Positionen untersucht werden müssen. Diese Zahl ist oft so groß, dass ein einfaches Durchprobieren aller Möglichkeiten zwar zum Ziel führen würde, aber viel zu lange dauert. Deshalb benötigt man weitere clevere Algorithmen wie Backtracking, um das vollständige Durchprobieren drastisch abzukürzen. Dadurch wird die Bearbeitungszeit akzeptabel, aber der Programmieraufwand steigt, da das abstrakte Backtracking an das vorliegende Puzzle angepasst werden muss.

Wünschenswert wäre es doch, statt der Programmierarbeit das Puzzle nur mit abstrakten Mitteln zu beschreiben. Kann es für solch eine abstrakte Beschreibung ein allgemeines Lösungsverfahren geben? Die Antwort ist 'ja' und damit kommen wir zu SAT- / SMT-Solvern.

SAT- / SMT-Solver

 SAT- / SMT-Solver sind sehr mächtige Werkzeuge, die sich für viele Probleme in der Informatik einsetzen lassen. Lösungen für Geduldspiele sind hier hier nur ein Nebenprodukt.

Die Aufgabe eines SAT- / SMT-Solvers besteht darin, für eine gegebene mathematische Formel festzustellen, ob sie eine Lösung besitzt und diese anzugeben. Bei einem SAT-Solver muss es sich um eine aussagenlogische Formel handeln wie (x ∨ ¬y) ∧ (¬x ∨ y ∨ z) ∧ ¬x, bei SMT-Solvern sind zusätzlich einige weitere Formeltypen wie arithmetische Gleichungen (wie u=3*v) oder Ungleichungen (wie u+v<10) möglich. Der genaue Umfang möglicher Formeln hängt vom jeweiligen SMT-Solver ab. Die Beschreibung der Problemstellung (hier also des Geduldspiels) wird recht einfach, und um den Lösungsweg, mit dem der SAT- / SMT-Solver seine Lösung findet, müssen wir uns keine Gedanken machen, dies passiert völlig automatisch. Intern werden wieder Backtracking und ähnliche Verfahren angewendet, aber darum müssen wir uns nicht mehr kümmern.

So viele Vorteile gibt es allerdings nicht ohne Nachteile: Das allgemeine Lösungsverfahren eines SAT- / SMT-Solvers arbeitet langsamer als ein problemangepasstes Backtracking, wir werden also keine rekordverdächtig großen Puzzles mit minimalem Programmieraufwand lösen können. Aber an der Weiterentwicklung von  SAT- / SMT-Solvern wird weltweit gearbeitet, so dass demnächst ihre Geschwindigkeit steigt.

Beschreibung von quadratischen 3x3-Legespielen für einen SMT-Solver

Wie lässt sich ein Legespiel mit derartigen Formeln beschreiben? Hier sollen zumindest verbale Beschreibungen für diese Formeln gegeben werden. Dazu betrachten wir die üblichen 3x3-Legespiele, bei denen neun quadratische Karten zu einem 3x3-Quadrat gelegt werden sollen, so dass immer passende Kanten aufeinandertreffen. 

Wir können das Spiel wie folgt beschreiben:

• Das Spiel besteht aus neun vorgegebenen Karten mit je vier Kanten. 
• Die Kanten der Karten haben je einen Namen (z.B. "brauner Hund, Kopf")
• Dazu gibt es einen zunächst leeren Rahmen mit sieben Positionen, der die Karten aufnehmen soll.
• Die Positionen sind durchnummeriert und die Kanten an jeder Position haben jeweils Variablen für Farbe und Körperteil. Legt man eine Karte an eine Position, übernehmen diese Variablen die Werte (d.h. Farbe und Körperteil) von den Kanten dieser Karte.

Nach der Beschreibung des Spiels erfolgt die Beschreibung einer Lösung:

• Jede Karte hat vier mögliche Orientierungen, darf also mehrfach um 90 Grad gedreht werden. 
• Jede Karte wird an eine Position im Rahmen gelegt. Daraus ergeben sich die Farben und Körperteile an den Kanten der Positionen im Rahmen. 
• Die Positionen der Karten sind alle verschieden. (Damit wird erreicht, dass keine zwei Karten übereinanderliegen und alle Positionen im Rahmen belegt werden)
• Gemeinsame Kanten benachbarter Positionen haben zueinander passende Namen, (z.B. "brauner Hund, Kopf" und "brauner Hund, Schwanz"). Es gibt 12 derartige Paare benachbarter Kanten, daraus entstehen jeweils 12 Bedingungen für gleiche Farben und unterschiedliche Körperteile.

Der große Vorteil besteht in der Kompaktheit der Beschreibung und der Einfachheit, die Beschreibung an andere Legespiele anzupassen. Mögliche Veränderungen wären:

• Dreieckige oder sechseckige Karten statt quadratischer Karten.
• Die Karten dürfen nicht gedreht werden.
• Die Karten tragen auf der Rückseite die gleichen Bilder und dürfen zusätzlich gewendet werden.
• Corner Matching statt Edge Matching.

Zusätzlich können wir SMT-Solver auch für ganz andere Typen von Geduldspielen einsetzen: Für Packprobleme (wie Pentominos) und sogar für Geduldspiele, die ganze Zugfolgen erfordern wie Zauberwürfel. 

Anleitung zum Verwenden eines SAT- / SMT-Solvers

Für mehrere SAT- / SMT-Solver gibt es eine Schnittstelle zur Programmiersprache Python. Dann kann man mit 1/2 bis 1 Seite Quelltext die Variablen und die Anforderungen an die Lösung für das Geduldspiel in Python beschreiben und anschließend den SAT- / SMT-Solver aufrufen, der dann die restliche Arbeit erledigt. Eine sehr schöne Anleitung gibt es von Dennis Yurichev [1]. Das Buch enthält auch sofort lauffähigen Quellcode für mehrere Geduldspiele, darunter Pentominos.

Mehr Infos:

[1] Dennis Yurichev: SAT/SMT by Example, 2024