Würfelschlagen lösen mit SAT/SMT-Solver

Auf wie viele Arten lässt sich eine Würfelschlange zu einem Würfel zusammenfalten? 

Um diese Frage zu beantworten, kommt man nicht um eine vollständige Analyse des Geduldspiels herum. Alle möglichen Biegungen der Würfelschlange müssen durchprobiert werden, ob sie zu einem perfekt zusammengefalteten 3x3x3-Würfel führen. Auch wenn das prinzipiell noch per Hand möglich ist (siehe [1] am Beispiel der häufigsten Würfelschlange cubra blue), wollen wir hier die Arbeit dem Computer überlassen. Die meisten solchen Programme arbeiten mittels Backtracking, welches noch problemangepasst programmiert werden muss.

Wenn wir statt dessen wieder einen SMT-Solver verwenden, müssen wir nur noch das Problem beschreiben und überlassen dem Solver die ganze Arbeit, die vielen Möglichkeiten in einer geeigneten Reihenfolge durchzuprobieren.

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

• Das Spiel besteht aus 27 Elementarwürfeln, diese sind entsprechend der Reihenfolge auf dem Faden der Würfelschlange von 0 bis 26 durchnummeriert.
• Dazu gibt es einen zunächst leeren Würfel der Größe 3x3x3, der die Elementarwürfel aufnehmen soll.
• Die Positionen im 3x3x3-Würfel werden beschrieben durch Koordinaten x, y und z, jeweils im Bereich von 0 bis 2.

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

• Jeder Elementarwürfel hat eine Position im großen 3x3x3-Würfel. 
• Die Positionen der Elementarwürfel sind alle verschieden. Damit wird gleichzeitig erreicht, dass alle Positionen im 3x3x3-Würfel belegt werden.
• Entlang der Schnur benachbarte Würfel in der Würfelschlange haben räumlich benachbarte Positionen im 3x3x3-Würfel, d.h. die Positionen der zwei benachbarten Würfel stimmen in zwei Koordinaten (x und y, x und z oder y und z) überein, die dritte Koordinate unterscheidet sich um genau 1.
• Für alle Elementarwürfel außer den Endwürfeln gilt: Verläuft die Schnur gerade durch den Würfel, dann stimmen die Positionen der zwei benachbarten Würfel in zwei der drei Koordinaten überein. Verläuft die Schnur um die Ecke, dann stimmen die Positionen der zwei benachbarten Würfel in nur einer Koordinate überein, die anderen zwei Koordinaten unterscheiden sich um jeweils genau 1.

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

Wegen der Symmetrie des Würfels ermittelt der Solver mehrere Lösungen, von denen einige durch Drehungen oder Spiegelungen auseinander hervorgehen. Dies lässt sich etwas einschränken, indem wir zusätzlich Forderungen an die Startposition der Würfelschlange stellen. Die Schlange startet mit einem dunklen Würfel und kann deshalb nur in einer Ecke oder einer Seitenmitte beginnen. Durch eine Drehung des Würfels können wir erreichen, dass eine Ecke als Startpunkt die Koordinaten (0,0,0) hat und die Seitenmitte als Startpunkt (1,1,0). Auch dann sind noch mehrere äquivalente Lösungen möglich, deren Ausschluss etwas mehr Aufwand erfordert.

Betrachten wir als Beispiel die rote Würfelschlange aus der Snake Cube Level Box, deren Lösungen hier noch nicht angegeben wurden. 

Hier die Kodierung der Würfelschlange:

0 0 1 1 1 1 0 1 1 0 1 1 1 1 1 0 1 1 0 1 1 1 1 1 1 0 0

Die 25 inneren Würfel der Würfelschlange werden folgendermaßen kodiert: 0 für gerade durchbohrte Würfel, 1 für Eckwürfel. Für die beiden Endwürfel am Anfang und Ende werden der Vollständigkeit halber vorn und hinten wird eine 0 angefügt. Die Art der Endwürfel spielt aber bei der Lösung keine Rolle.

SMT-Solver-Info: Z3 liefert 8 verschiedene Lösungen, die sämtlich in der Seitenmitte auf der Unterseite starten. Diese sind aber identisch, sie unterscheiden sich nur durch Rotation und Spiegelung. Nach der ersten Ecke (in der Mitte der oberen Schicht) kann es in jeder der vier Richtungen weitergehen, dies entspricht einer Rotation des 3x3x3-Würfels. An der zweiten Biegung (im Bild in der Mitte der Kante rechts oben) geht es nach hinten, es kann in gespiegelter Richtung auch nach vorn gehen. Dies entspricht acht Varianten für dieselbe Lösung. Also gibt also nur eine einzige Lösung:

Mehr Infos:

[1] www.mathematische-basteleien.de