Wie lässt sich ein Geduldspiel wie Mephisto mit dem Computer analysieren? Wir wollen wieder einen SMT-Solver verwenden, um möglichst wenig Programmieraufwand in das spezielle Geduldspiel zu investieren und statt dessen dem Solver möglichst die ganze Arbeit zu überlassen, die vielen Möglichkeiten für Lage, Orientierung und Reihenfolge der Streifen durchzuprobieren.
Für den SMT-Solver können wir das Spiel wie folgt beschreiben:
- Das Spiel besteht aus 10 Streifen (nummeriert von 0 bis 9) der Länge 5, jeder entspricht einer Liste der Länge 5 mit Elementen Quadrat, Kreis und Stern. Diese tragen jeweils ein Vorzeichen (+ oder -) entsprechend der Orientierung auf dem Streifen. Entsprechend seiner Lage kann jeder Streifen 4 Orientierungen annehmen (gedreht um 180 Grad bzw. gewendet)
- Dazu gibt es einen zunächst leeren Rahmen Größe 2x5x5, der die Streifen aufnehmen soll. Er hat 10 Positionen für die Streifen (waagerecht in der unteren Schicht, senkrecht in der oberen)
- Die Positionen der Streifen im Rahmen werden nummeriert von 0 bis 9, dazu die verwendete Orientierung (nummeriert von 0 bis 3).
Nach der Beschreibung des Spiels erfolgt die Beschreibung einer Lösung:
- Jeder Streifen hat eine Position und eine Orientierung Rahmen.
- Die Nummern der verwendeten Streifen sind alle verschieden. Damit wird gleichzeitig erreicht, dass alle Streifen verwendet werden (und nicht z.B. einer doppelt und ein anderer gar nicht).
- Übereinaderliegende Elementarquadrate tragen die gleichen Symbole in der gleichen Orientierung.
Das ist schon ausreichend, um den SMT-Solver (hier: Z3Py, das ist der SMT-Solver Z3 mit einem Interface zu Python) zu benutzen.
Jetzt können wir gespannt sein, wie viele Lösungen ermittelt werden und in wieweit diese wirklich verschieden sind.
SMT-Solver-Info: Z3 liefert 64 verschiedene Lösungen, die aber alle Varianten derselben Lösung sind: Wir können ein gelöstes Spiel auf 16 Arten in den Rahmen packen: Möglich ist eine Rotation um 90 Grad (4 Möglichkeiten), das Wenden jedes Steins an seiner Position (2 Möglichkeiten) sowie das Vertauschen der oberen und der unteren Schicht (2 Möglichkeiten). Außerdem sind zwei der 10 Steine spiegelsymmetrisch, diese können diese können zusätzlich einzeln gewendet werden (2*2 Möglichkeiten). Dies sind die 64 gefundenen Lösungen.
Hier die zwei symmetrischen Steine:
Keine Kommentare:
Kommentar veröffentlichen