Une fois que je suis tombé sur un jeu de pentomino où il fallait mettre 13 chiffres dans un carré de 8 par 8. Après un certain temps pendant lequel j'ai essayé en vain de résoudre ce problème, j'ai décidé qu'il était nécessaire d'écrire un programme qui ferait cela pour moi. Pour ce faire, il a fallu choisir un algorithme de solution. La première chose qui vient à l'esprit est l'algorithme habituel des branches et des bordures, lorsque les figures sont empilées les unes à côté des autres (l'algorithme avec les liens dansants ne convient pas ici, car les figures sont différentes). Diverses heuristiques sont généralement utilisées pour accélérer cet algorithme, par exemple, la ramification avec le moins d'options est préférée. Vous pouvez trouver et implémenter d'autres heuristiques dans cet algorithme, mais ici, je pensais que de nombreuses astuces différentes pour accélérer la solution de ces problèmes ont déjà été implémentées dans les solveurs SAT. Par conséquent, il est nécessaire de traduire la tâche dans le langage mathématique approprié et d'utiliser une sorte de solveur SAT. À propos de la façon dont cela a été mis en œuvre et quels résultats peuvent être lus sous la coupe.
Au début, je veux vous rappeler ce qu'est le jeu pentamino. Il s'agit d'un champ carré 8x8, qui doit être carrelé avec 13 chiffres - 12 gribouillis, qui se composent de 5 carrés et d'un chiffre 2x2:
Ici, il convient de dire quel est le problème de satisfiabilité booléenne ou le problème SAT. En termes généraux, elle peut être formulée comme la recherche de telles valeurs de variables booléennes dans lesquelles l'expression donnée devient vraie. D'une manière générale, il s'agit d'une tâche complète de NP, cependant, il existe de nombreuses astuces qui aident à la résoudre efficacement. Pour ce faire, de nombreuses applications spéciales appelées solveurs SAT ont été développées. J'utiliserai un solveur SAT nommé minisat. Pour résoudre ce problème, il est nécessaire de réécrire l'expression d'entrée sous forme normale conjonctive, c'est-à-dire sous la forme d'un produit de sommes logiques de variables. Chaque parenthèse sous forme normale conjonctive est appelée ici une clause, qui est le «ou» logique de certains littéraux, c'est-à-dire les variables booléennes ou leurs dénis. Par exemple:
(x1 V pas x3) (x2 V x4) (x2 V x3 V pas X4)
J'avais besoin de traduire la tâche de tuilage en tâche SAT. Prenez une figure pentamino et mettez-la sur le terrain de jeu de toutes les manières possibles, y compris les changements, les virages et les réflexions. Pour chacune de ces positions de la figure, nous associons une variable booléenne et nous supposerons que si dans notre solution finale cette figure est présente dans cette position particulière, alors la variable sera vraie et sinon, alors fausse. Nous le faisons pour tous les chiffres.
Établissons maintenant une formule décrivant notre problème, c'est-à-dire que nous imposerons des restrictions sur nos variables. La première chose à faire est de s'assurer que toutes les cellules de notre terrain de jeu seront recouvertes d'au moins un chiffre. Pour ce faire, pour chaque cellule de 64, nous retrouvons tous les chiffres et positions de ces chiffres qui couvrent cette cellule et composons une clause à partir des variables qui sont affectées à ces positions des chiffres. La deuxième chose à faire est d'éliminer l'intersection des formes. Cela peut être fait en un double cycle, en triant simplement toutes les positions possibles de toutes les figures et en déterminant si la paire a des cellules communes. S'il y en a, alors ils se coupent et vous devez ajouter une clause du formulaire (pas x_i V pas x_j), où x_i est la variable affectée à la première position, et x_j est la deuxième position. Cette clause est vraie lorsque x_i et x_j ne sont pas égaux à un en même temps, c'est-à-dire, exclut les intersections. Et enfin, la troisième chose à considérer est que chaque figurine ne peut être présente sur le terrain qu'une seule fois. Pour ce faire, nous parcourons également toutes les positions de chaque figure dans un double cycle et pour chaque paire de positions de la même figure nous faisons une clause similaire à la précédente et constituée de deux négatifs. Autrement dit, lorsque deux chiffres identiques apparaissent (mais dans des positions différentes), l'une de ces clauses donnera faux et, par conséquent, exclura une telle solution.
Tout cela n'était qu'une théorie, et maintenant passons à la pratique. Chaque chiffre a un numéro de 1 à d pour le distinguer des autres et l'imprimer facilement. Ensuite, créez une matrice du terrain de jeu et encodez les cellules correspondantes du terrain de jeu comme occupées / non occupées par la figure:
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 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 . . . . . .
Maintenant, pour chaque pièce, il est nécessaire de trouver toutes les positions possibles sur le terrain de jeu au moyen de décalages, de virages et de réflexions. Commençons par les virages et les reflets. Au total, il y a 8 transformations possibles de spires et de réflexions, dont une transformation triviale qui laisse la figure intacte. Pour ces transformations, je crée 8 matrices correspondantes, comme indiqué ci-dessous. Après rotation ou réflexion, la figurine peut dépasser le terrain de jeu, vous devez donc la remettre sur le terrain de jeu. Il convient également de tenir compte du fait que certains chiffres peuvent se transformer en eux-mêmes après la transformation, et de tels cas doivent être exclus. J'ajoute des options uniques à la classe d'orientation. Le résultat est le code suivant:
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; }
Ce code est appliqué à chacune des figures, puis les Orientations uniques reçues sont décalées le long des axes x et y créant toutes les positions possibles de chaque figure. En conséquence, nous avons le nombre suivant de positions différentes pour chacun des chiffres:
---------- 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
Ensuite, nous attribuons une variable booléenne à chaque position possible et créons une formule, comme décrit ci-dessus. Après cela, nous appelons minisat directement depuis l'application, qui retourne une solution - un ensemble de nos variables avec les valeurs assignées true ou false. En sachant à quelles positions ces variables ont été affectées, nous imprimons la solution:
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
Et ensuite
Naturellement, il ne serait pas si intéressant de s'y attarder. Par conséquent, la première question qui s'est posée pour moi était «combien de solutions différentes existent qui ne diffèrent pas dans les virages triviaux et les réflexions du terrain de jeu?». Pour ce faire, il existe un mode dans le solveur SAT qui vous permet d'ajouter des clauses sans perdre d'informations existantes, ce qui accélère considérablement le processus par rapport à la recherche de la solution à partir de zéro. La solution suivante peut être trouvée en ajoutant une clause qui contient la négation de toutes les variables présentes dans la solution précédente. Après avoir ajouté cette procédure et comparé la nouvelle solution avec les précédentes, en tenant compte des virages et des réflexions du terrain de jeu, j'ai eu 1364 options différentes.
Une autre extension intéressante que j'ai mise en œuvre a été l'étude de diverses autres formes de terrain de jeu et de figures. Et enfin, l'étude des terrains de jeu en trois dimensions était très intéressante. Mais c'est un sujet pour un autre article.
Mettre à jour
Après avoir ajouté une condition supplémentaire: pour chaque chiffre d'une clause - il devrait y avoir au moins une position de ce chiffre sur le terrain de jeu, le calcul est devenu beaucoup plus rapide. De plus, une erreur a été corrigée, à la suite de laquelle le nombre de toutes les options uniques possibles est 16146.