Als ich auf ein Pentomino-Spiel stieß, bei dem es notwendig war, 13 Zahlen in ein Quadrat von 8 mal 8 zu setzen. Nach einer bestimmten Zeit, in der ich erfolglos versuchte, dieses Problem zu lösen, entschied ich, dass es notwendig war, ein Programm zu schreiben, das dies für mich tun würde. Dazu musste ein Lösungsalgorithmus gewählt werden. Das erste, was mir in den Sinn kommt, ist der übliche Algorithmus von Zweigen und Rändern, wenn die Figuren nacheinander nebeneinander gestapelt werden (der Algorithmus mit tanzenden Links ist hier nicht geeignet, da die Figuren unterschiedlich sind). Verschiedene Heuristiken werden normalerweise verwendet, um diesen Algorithmus zu beschleunigen. Beispielsweise wird eine Verzweigung mit der geringsten Anzahl von Optionen bevorzugt. Sie können andere Heuristiken in diesen Algorithmus einbauen und implementieren, aber hier dachte ich, dass viele verschiedene Tricks zur Beschleunigung der Lösung solcher Probleme bereits in SAT-Lösern implementiert wurden. Daher ist es notwendig, die Aufgabe in die entsprechende mathematische Sprache zu übersetzen und eine Art SAT-Löser zu verwenden. Wie dies implementiert wurde und was die resultierenden Ergebnisse sind, kann unter dem Schnitt gelesen werden.
Am Anfang möchte ich Sie daran erinnern, was das Spiel Pentamino ist. Dies ist ein quadratisches 8x8-Feld, das mit 13 Figuren gekachelt werden muss - 12 Kringel, die aus 5 Quadraten und einer 2x2-Figur bestehen:
Hier ist zu sagen, was das Boolesche Erfüllbarkeitsproblem oder das SAT-Problem ist. Im Allgemeinen kann es als das Finden solcher Werte von Booleschen Variablen formuliert werden, in denen der gegebene Ausdruck wahr wird. Im Allgemeinen ist dies eine vollständige NP-Aufgabe, es gibt jedoch viele Tricks, die helfen, sie effektiv zu lösen. Zu diesem Zweck wurden viele spezielle Anwendungen entwickelt, die als SAT-Löser bezeichnet werden. Ich werde einen SAT-Solver namens Minisat verwenden. Um dieses Problem zu lösen, muss der Eingabeausdruck in konjunktiver Normalform umgeschrieben werden, dh in Form eines Produkts logischer Variablensummen. Jede Klammer in konjunktiver Normalform wird hier als Klausel bezeichnet, die das logische „oder“ einiger Literale ist, dh boolesche Variablen oder deren Verweigerung. Zum Beispiel:
(x1 V nicht x3) (x2 V x4) (x2 V x3 V nicht X4)
Ich musste die Kachelaufgabe in die SAT-Aufgabe übersetzen. Nehmen Sie eine Pentamino-Figur und bringen Sie sie auf alle möglichen Arten ins Spiel, einschließlich Verschiebungen, Drehungen und Reflexionen. Für jede solche Position der Figur ordnen wir eine boolesche Variable zu und wir gehen davon aus, dass, wenn in unserer endgültigen Lösung diese Figur an dieser bestimmten Position vorhanden ist, die Variable wahr und wenn nicht falsch ist. Wir machen das für alle Figuren.
Lassen Sie uns nun eine Formel erstellen, die unser Problem beschreibt, dh wir werden unseren Variablen tatsächlich Einschränkungen auferlegen. Das erste, was Sie tun müssen, ist sicherzustellen, dass alle Zellen unseres Spielfelds mit mindestens einer Figur bedeckt sind. Zu diesem Zweck finden wir für jede Zelle von 64 alle Abbildungen und Positionen dieser Abbildungen, die diese Zelle abdecken, und setzen aus den Variablen, die diesen Positionen der Abbildungen zugeordnet sind, eine Klausel. Das zweite, was zu tun ist, ist, den Schnittpunkt von Formen zu beseitigen. Dies kann in einem doppelten Zyklus erfolgen, indem einfach alle möglichen Positionen aller Figuren aussortiert werden und bestimmt wird, ob das Paar gemeinsame Zellen hat. Wenn dies der Fall ist, überschneiden sie sich und Sie müssen eine Klausel der Form hinzufügen (nicht x_i V nicht x_j), wobei x_i die der ersten Position zugewiesene Variable und x_j die zweite Position ist. Diese Klausel gilt, wenn x_i und x_j nicht gleichzeitig gleich eins sind, dh Schnittpunkte ausschließen. Und schließlich ist zu berücksichtigen, dass jede Figur nur einmal auf dem Spielfeld vorhanden sein kann. Dazu gehen wir auch alle Positionen jeder Figur in einem Doppelzyklus durch und machen für jedes Positionspaar derselben Figur eine Klausel ähnlich der vorherigen, die aus zwei Negativen besteht. Das heißt, wenn zwei identische Figuren erscheinen (aber an unterschiedlichen Positionen), wird eine dieser Klauseln falsch sein und dementsprechend eine solche Lösung ausschließen.
Es war alles eine Theorie, und jetzt wollen wir weiter üben. Jede Figur hat eine Zahl von 1 bis d, um sie von anderen zu unterscheiden und bequem zu drucken. Erstellen Sie dann eine Matrix des Spielfelds und codieren Sie die entsprechenden Zellen des Spielfelds als belegt / nicht belegt von der Figur:
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 1 1 . . . . .
1 1 . . . . . .
. 1 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 3 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
4 . . . . . . .
4 . . . . . . .
4 4 . . . . . .
. 4 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
5 5 . . . . . .
5 5 . . . . . .
5 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
6 6 6 . . . . .
. 6 . . . . . .
. 6 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
7 . 7 . . . . .
7 7 7 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
8 . . . . . . .
8 . . . . . . .
8 8 8 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . 9 . . . . .
. 9 9 . . . . .
9 9 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. a . . . . . .
aaa . . . . .
. a . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
b . . . . . . .
bb . . . . . .
b . . . . . . .
b . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. cc . . . . .
. c . . . . . .
cc . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
dd . . . . . .
dd . . . . . .
Jetzt ist es für jedes Stück notwendig, alle möglichen Positionen auf dem Spielfeld durch Verschiebungen, Drehungen und Reflexionen zu finden. Beginnen wir mit Drehungen und Reflexionen. Insgesamt gibt es 8 mögliche Transformationen von Windungen und Reflexionen, einschließlich einer trivialen Transformation, bei der die Figur intakt bleibt. Für diese Transformationen erstelle ich 8 entsprechende Matrizen, wie unten gezeigt. Nach der Drehung oder Reflexion kann die Figur über das Spielfeld hinausgehen, sodass Sie sie wieder auf das Spielfeld zurückbringen müssen. Es sollte auch berücksichtigt werden, dass sich einige Zahlen nach der Transformation in sich selbst verwandeln können, und solche Fälle sollten ausgeschlossen werden. Ich füge der Orientierungsklasse einzigartige Optionen hinzu. Das Ergebnis ist der folgende Code:
int dimension_ = 2; const unsigned int MATRIX_SIZE = dimension_ * dimension_; int * matrix = new int[ MATRIX_SIZE ]; for( unsigned int i = 0; i < MATRIX_SIZE; i++ ) { matrix[ i ] = 0; } for( unsigned int i = 0; i < dimension_; i++ ) { int * matrix1 = new int[ MATRIX_SIZE ]; std::copy( matrix, matrix + MATRIX_SIZE, matrix1 ); matrix1[ i ] = 1; for( unsigned int j = dimension_; j < 2 * dimension_; j++ ) { if( !matrix1[ j - dimension_ ] ) { int * matrix2 = new int[ MATRIX_SIZE ]; std::copy( matrix1, matrix1 + MATRIX_SIZE, matrix2 ); matrix2[ j ] = 1; unsigned int NUMBER = 1 << dimension_; for( unsigned int l = 0; l < NUMBER; l++ ) { int * matrix3 = new int[ MATRIX_SIZE ]; std::copy( matrix2, matrix2 + MATRIX_SIZE, matrix3 ); if( l & 1 ) { for( unsigned int l1 = 0; l1 < dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } if( l & 2 ) { for( unsigned int l1 = dimension_; l1 < 2 * dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } Orientation * orientation = new Orientation( figure ); for( std::vector<Point *>::const_iterator h = figure->points().begin(); h != figure->points().end(); ++h ) { const Point * p = *h; int x = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { x = x + p->coord( i1 ) * matrix3[ i1 ]; } int y = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { y = y + p->coord( i1 ) * matrix3[ dimension_ + i1 ]; } Point p1( x, y ); orientation->createPoint( p1.coord( 0 ), p1.coord( 1 ) ); } orientation->moveToOrigin(); if( isUnique( orientations, orientation ) ) { orientations.push_back( orientation ); } else { delete orientation; } delete [] matrix3; } delete [] matrix2; } } delete [] matrix1; }
Dieser Code wird auf jede der Figuren angewendet, und dann werden die empfangenen eindeutigen Ausrichtungen entlang der x- und y-Achse verschoben, wodurch alle möglichen Positionen jeder Figur erzeugt werden. Als Ergebnis haben wir für jede der Figuren die folgende Anzahl unterschiedlicher Positionen:
---------- Figure 1
Count = 288
---------- Figure 2
Count = 64
---------- Figure 3
Count = 280
---------- Figure 4
Count = 280
---------- Figure 5
Count = 336
---------- Figure 6
Count = 144
---------- Figure 7
Count = 168
---------- Figure 8
Count = 144
---------- Figure 9
Count = 144
---------- Figure a
Count = 36
---------- Figure b
Count = 280
---------- Figure c
Count = 144
---------- Figure d
Count = 49
Dann weisen wir jeder möglichen Position eine boolesche Variable zu und erstellen eine Formel, wie oben beschrieben. Danach rufen wir minisat direkt aus der Anwendung auf, die eine Lösung zurückgibt - eine Menge unserer Variablen mit den zugewiesenen Werten true oder false. Da wir wissen, welchen Positionen diese Variablen zugewiesen wurden, drucken wir die Lösung:
bbbb 3 3 3 3
ddbc 8 8 8 3
dd 1 ccc 8 2
5 5 1 1 1 c 8 2
5 5 5 1 4 4 4 2
7 7 a 4 4 9 6 2
7 aaa 9 9 6 2
7 7 a 9 9 6 6 6
Was weiter
Darauf einzugehen wäre natürlich nicht so interessant. Daher stellte sich für mich zunächst die Frage, wie viele verschiedene Lösungen existieren, die sich nicht in trivialen Wendungen und Reflexionen des Spielfelds unterscheiden. Zu diesem Zweck gibt es im SAT-Solver einen Modus, mit dem Sie Klauseln hinzufügen können, ohne vorhandene Informationen zu verlieren. Dies beschleunigt den Prozess erheblich, als ob die Lösung von Grund auf neu gesucht worden wäre. Die folgende Lösung kann durch Hinzufügen einer Klausel gefunden werden, die die Negation aller in der vorherigen Lösung vorhandenen Variablen enthält. Nachdem ich dieses Verfahren hinzugefügt und die neue Lösung mit den vorherigen verglichen hatte, wobei ich die Wendungen und Reflexionen des Spielfelds berücksichtigte, erhielt ich 1364 verschiedene Optionen.
Eine weitere interessante Erweiterung, die ich implementiert habe, war das Studium verschiedener anderer Formen des Spielfelds und der Figuren. Und schließlich war das Studium dreidimensionaler Spielfelder sehr interessant. Dies ist jedoch ein Thema für einen anderen Artikel.
Update
Nach dem Hinzufügen einer zusätzlichen Bedingung: Für jede Figur einer Klausel - sollte es mindestens eine Position dieser Figur im Spielfeld geben, ist die Berechnung viel schneller geworden. Außerdem wurde ein Fehler behoben, wodurch die Anzahl aller möglichen eindeutigen Optionen 16146 beträgt.