Nintai mit SMT-Solver lösen

Die Beschreibung dieses Anlegespiels gibt es bei Nintai, 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 36 vorgegebenen Steinen mit je drei Kanten.
• Die Kanten der Steine haben je einen Namen bestehend aus einer Ziffer. Die Farbe der Kante ist unwichtig, da alle 36 Steine in einer Lösung farblich gleich ausgerichtet sein müssen. Damit müssen die Namen der Kanten nur in der gleichen Reihenfolge (z.B. blau-grün-gelb) notiert werden. 
• Dazu gibt es einen zunächst leeren Rahmen mit 36 Positionen, der die Steine aufnehmen soll.
• Die Positionen sind durchnummeriert und die Kanten an jeder Position haben jeweils eine Variable für die Ziffer. Legt man einen Stein an eine Position, wird diese Variable von den Kanten dieses Steins übernommen.

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

• Die Steine haben alle die gleiche farbliche Orientierung, dürfen also nicht gedreht werden.
• Jeder Stein hat eine Position im Rahmen. Daraus ergeben sich die Ziffern an den Kanten der Positionen im Rahmen. 
• Die Positionen der Steine sind alle verschieden. Damit wird erreicht, dass keine zwei Steine übereinander liegen und alle Positionen im Rahmen belegt werden.
• Gemeinsame Kanten benachbarter Positionen haben die gleiche Ziffer. Es gibt 45 derartige Paare benachbarter Kanten, daraus entstehen 45 Bedingungen für gleiche Ziffern.

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 immer neue Lösungen im Abstand von wenigen Sekunden. Wegen der für uns undurchschaubaren Arbeitsweise des SMT-Solvers ist nicht klar, wie lange der Lösungsprozess laufen wird und wie viele Lösungen gefunden werden. Man kann vor dem eigentlichen Lösungsprozess einige Steine fest platzieren (z.B. drei Steine in den Ecken) und sich dann alle Lösungen berechnen lassen. Dies bedeutet nur einige wenige zusätzliche Bedingungen für den SMT-Solver. Dafür gibt es jeweils nur wenige Lösungen, die alle gefunden werden. Aus den so ermittelten Anzahlen lässt sich ganz vorsichtig schätzen, dass es für Nintai insgesamt Hunderttausende oder gar Millionen von Lösungen geben könnte.

Da es so viele Lösungen gibt, kann man nach besonders schönen Lösungen Ausschau halten. Nur sollten sich die zusätzlichen Anforderungen leicht als zusätzliche Bedingungen für den SMT-Solver formulieren lassen. Hier eine Lösung, die am Rand ausschließlich die Ziffer 1 trägt.  

Der SMT-Solver findet sechs Lösungen. Doch diese Lösungen sind nicht wirklich verschieden, sie gehen alle durch Drehungen und Spielgelungen auseinander hervor. Diese Drehungen und Spiegelungen sind allerdings nur deshalb möglich, weil die Nummern auf den Steinen entsprechend angelegt sind. Jeden Stein gibt es (bei unveränderter farblicher Orientierung) auch gedreht und gespiegelt.

Hersteller: Nintai Products
Erscheinungsjahr: 1985

Google: Nintai Puzzle
Shopping: Nicht lieferbar.