6.10.24

Magische Quadrate mit SMT-Solver erstellen

Hier geht es um die Erstellung Magischer Quadrate zur weiteren Verwendung in anderen Geduldspielen, z.B. beim Boss-Puzzle. 

In einem Magischen Quadrat der Größe nxn sind die Zahlen von 1 bis n² so eingetragen. dass die folgenden Summen alle gleich sind: Die Summen jeder Zeile, ebenso die Summen jeder Spalte und die Summen der beiden Diagonalen. Bei den Schiebespielen in der oberen Reihe muss man sich in den Leerfeldern die Zahlen 9 bzw. 16 vorstellen.


Für den SMT-Solver Z3 können wir diese Aufgabe wie folgt beschreiben:

  • Das Spiel besteht aus n² ganzzahligen Variablen.
  • Jede dieser Variablen soll einen Wert zwischen 1 und n²  (einschließlich) annehmen. 
  • Die magische Summe berechnen wir als s = n² * (n²+1) / (2n) =  n * (n²+1) / 2

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

  • Die Werte der Variablen sind alle verschieden. (Damit kommen alle Zahlen 1...n² vor und auch keine doppelt). 
  • Die Summen jeder Zeile, jeder Spalte und die Summen der beiden Diagonalen sind gleich der magischen Summe s. 
Das ist schon ausreichend, um den SMT-Solver (hier: Z3Py, das ist der SMT-Solver Z3 mit einem Interface zu Python) zu benutzen.

Für die Boss-Puzzle kommt noch die Bedingung der geraden Permutation hinzu: Dazu muss man einfach noch die Zahl der Fehlstellungen ermitteln und entscheiden, ob diese gerade oder ungerade ist.

Beim der Variante Sixty-5 kommt zusätzlich die Bedingung hinzu, dass die Variable zum Feld oben rechts den Wert 5 haben muss.

Das alles ist in wenigen Zeilen programmiert und gibt das Gefühl, die magischen Quadrate selbst gefunden zu haben.

Insgesamt gibt es die folgende Anzahl von Lösungen [1]:

  • Es gibt 8 Magische Quadrate der Größe 3x3
  • Es gibt 7040 Magische Quadrate der Größe 4x4
  • Für die Größe 5x5 reicht unsere Zeit nicht, alle Lösungen mit dem SMT-Solver zu finden. Mit anderen Methoden geht es schneller: In [1] berichtet Michael Holzapfel, dass es 2.202.441.792 verschiedene Magische Quadrate gibt. 

Alle diese Zahlen müssen aus Symmetriegründen (Rotation und Spiegelung) noch durch 8 geteilt werden, wenn man nur wesentlich verschiedene Lösungen zählen möchte.

Mehr Infos:

Keine Kommentare:

Kommentar veröffentlichen