Welt der Geduldspiele: Crazy Jacob mit SMT-Solver lösen

8.5.24

Crazy Jacob mit SMT-Solver lösen

Die Beschreibung dieses Anlegespiels gibt es bei Crazy Jacob, hier soll nur die Lösung mit einem SMT-Solver beschrieben werden.

Für den SMT-Solver können wir das Spiel wie folgt beschreiben:

Das Spiel besteht aus neun vorgegebenen Karten mit je drei Kanten.
Die Kanten der Karten haben je einen Namen bestehend aus Farbe und Körperteil (z.B. "gelb, Kopf").
Dazu gibt es einen zunächst leeren Rahmen mit neun 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, werden diese Variablen von den Kanten dieser Karte übernommen.

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

Jede Karte hat eine der drei möglichen Orientierungen (nicht gedreht, um 120 Grad gedreht, um 240 Grad gedreht).
Jede Karte hat eine Position im Rahmen. 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 übereinander liegen und alle Positionen im Rahmen belegt werden.
Gemeinsame Kanten benachbarter Positionen haben gleiche Farbe, aber verschiedene Körperteile (z.B. "braun, Kopf" und "braun, Schwanz"). Es gibt neun derartige Paare benachbarter Kanten, daraus entstehen jeweils neun Bedingungen für gleiche Farben und neun für unterschiedliche Körperteile.

Das ist schon ausreichend, um den SMT-Solver (hier: Z3Py, das ist der SMT-Solver Z3 mit einem Interface zu Python) zu benutzen.

SMT-Solver-Info: Z3 liefert 12 verschiedene Lösungen. Davon sind jedoch nur zwei wirklich verschieden: Wegen der Symmetrie des Rahmens muss man die Gesamtanzahl durch drei teilen. Außerdem gibt es Karten mit jeweils zwei gleichen Kanten, z.B. im Bild ganz oben. Liegt diese an einer Ecke, so kann man sie in einer Richtung um 120 Grad drehen und erhält wieder eine Lösung. Jede Lösung enthält eine solche Karte an einer Ecke, damit verbleiben nur zwei wesentlich verschiedene Lösungen.