Die Beschreibung dieses Anlegespiels gibt es bei Schreckschrauben, hier soll nur die Lösung mit einem SMT-Solver beschrieben werden. Der Einfachheit halber werden wie bei anderen Anlegespielen die Muttern als (sechseckige) Karten bezeichnet.
Für den SMT-Solver können wir das Spiel wie folgt beschreiben:
- Das Spiel besteht aus sieben vorgegebenen Karten mit je sechs Kanten.
- Die Kanten der Karten haben je einen Namen bestehend aus einer Ziffer.
- 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 eine Ziffer. Legt man eine Karte an eine Position, übernehmen diese Variablen die Werte (d.h. Ziffern) von den Kanten dieser Karte.
Nach der Beschreibung des Spiels erfolgt die Beschreibung einer Lösung:
- Jede Karte hat eine der sechs möglichen Orientierungen (jeweils um Vielfache von 60 Grad gedreht).
- Jede Karte hat eine Position im Rahmen. Daraus ergeben sich die Ziffern 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 die gleiche Ziffer. Es gibt 12 derartige Paare benachbarter Kanten, daraus entstehen 12 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 6 verschiedene Lösungen. Diese sind aber identisch, sie unterscheiden sich nur durch eine Rotation des Rahmens um Vielfache von 60 Grad. Es gibt also nur eine einzige Lösung.
Hersteller: Heye
Google: "Das magische Dreieck" Heye
Shopping: Lieferbar, Preis ca. 10 €
Keine Kommentare:
Kommentar veröffentlichen