Symmetriepuzzle lösen mit SAT/SMT-Solver

Manche Symmetriepuzzles sind wirklich schwierig zu lösen. Und ganz besonders schwer wird es, wenn man alle Lösungen finden möchte. Es gibt keine übersichtliche Art, alle Möglichkeiten systematisch durchzuprobieren. Auch wenn man den Computer einsetzen möchte und an Backtracking denkt, wird es nicht wirklich einfach, das Backtracking zu organisieren.

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.

Der Einfachheit halber wollen wir das Vorgehen für solche Symmetriepuzzles beschreiben, deren Steine aus Polyominos bestehen, welche auf einem quadratischen Gitter liegen sollen.

Vor dem Start entscheiden wir uns für eine maximale Größe des Rahmens, in dem wir nach einer symmetrischen Figur suchen. Eine praktikable Größe ist 7x7, manchmal reicht auch schon 5x5. Und der SMT-Solver schafft auch noch 12x12, vielleicht sogar noch größer. Wählen wir also einen Rahmen der Größe nxn. 

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

• Das Spiel besteht aus n² Feldern, angeordnet in einer nxn-Matrix M.
• Dazu gibt es k Steine, nummeriert von 1 bis k.
• Die zu platzierenden Steine werden ebenfalls mit kleineren Matrizen beschrieben, die abgedeckten Felder haben den Wert 1, der Rest 0. 
• Jeder Stein hat eine Orientierung, wenn er in das große Feld gelegt wird. Dabei kann der Ausgangsstein rotiert werden (um Vielfache von 90 Grad) oder (waagerecht) gespiegelt.

Nach der Beschreibung des Spiels erfolgt die Beschreibung einer Lösung. Ein Feld der Matrix M hat als Wert die die Nummer des Steins, der das Feld überdeckt, nicht überdeckte Felder haben den Wert 0.

• Jedes Feld der Matrix M hat als Wert eine ganze Zahl im Bereich [0,k]. Die Zahl 0 wird für Leerfelder stehen, andrer Zahlen für die Nummer des dort liegenden Steins.
• Jeder Stein erhält eine Orientierung.
• Jeder Stein erhält eine Position im Inneren der großen nxn-Matrix platziert. Dabei haben diejenigen Felder der Matrix, die er abdeckt, die Nummer des Steins. Alle anderen Felder haben nicht diese Nummer.
• Jedes Feld kann nur eine Nummer haben. Damit wird erreicht, dass keine zwei Steine sich überlappen.
• Eine der möglichen Symmetrien der Matrix erfüllt die folgende Bedingung: Für alle Felder der großen Matrix gilt: Wenn ein Feld besetzt ist (d.h. ≠0), dann auch das dazu symmetrisch gelegene Feld.  

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

Obwohl es bei ebenen Symmetriepuzzles nur Spiegelsymmetrie und Rotationssymmetrie relevant sind, müssen mehrere Fälle bei der genauen Lage von Symmetrieachse bzw. Rotationszentrum beachtet werden. Dies wird im Post Symmetrie im quadratischen Gitter genauer beschrieben.