Resolviendo el problema de mosaico usando el solucionador SAT usando el ejemplo de pentamino

Una vez que encontré un juego de pentomino donde era necesario poner 13 figuras en un cuadrado de 8 por 8. Después de un cierto período de tiempo durante el cual intenté resolver este problema sin éxito, decidí que era necesario escribir un programa que hiciera esto por mí. Para hacer esto, fue necesario elegir un algoritmo de solución. Lo primero que viene a la mente es el algoritmo habitual de ramas y bordes, cuando las figuras se apilan una tras otra adyacentes entre sí (el algoritmo con enlaces de baile no es adecuado aquí, ya que las figuras son diferentes). Por lo general, se utilizan diversas heurísticas para acelerar este algoritmo, por ejemplo, se prefiere la ramificación con el menor número de opciones. Puede crear e implementar otras heurísticas en este algoritmo, pero aquí pensé que muchos trucos diferentes para acelerar la solución de tales problemas ya se han implementado en solucionadores SAT. Por lo tanto, es necesario traducir la tarea al lenguaje matemático apropiado y utilizar algún tipo de solucionador SAT. Acerca de cómo se implementó esto y qué resultados pueden leerse debajo del corte.

Al principio quiero recordarte qué es el juego pentamino. Este es un campo cuadrado de 8x8, que debe estar en mosaico con 13 figuras - 12 garabatos, que consisten en 5 cuadrados y una figura de 2x2:



Aquí vale la pena decir cuál es el problema de satisfacción booleana o el problema SAT. En términos generales, puede formularse como el hallazgo de tales valores de variables booleanas en las que la expresión dada se vuelve verdadera. En términos generales, esta es una tarea completa de NP, sin embargo, hay muchos trucos que ayudan a resolverlo de manera efectiva. Para hacer esto, se han desarrollado muchas aplicaciones especiales llamadas solucionadores SAT. Usaré un solucionador SAT llamado minisat. Para resolver este problema, es necesario reescribir la expresión de entrada en forma conjuntiva normal, es decir, en forma de un producto de sumas lógicas de variables. Cada paréntesis en forma normal conjuntiva aquí se llama una cláusula, que es el "o" lógico de algunos literales, es decir, variables booleanas o sus negaciones. Por ejemplo:

(x1 V no x3) (x2 V x4) (x2 V x3 V no X4)

Necesitaba traducir la tarea de mosaico en la tarea SAT. Tome una figura de pentamino y póngala en el campo de juego de todas las formas posibles, incluidos los cambios, giros y reflexiones. Para cada posición de la figura, asociamos una variable booleana y asumiremos que si en nuestra solución final esta figura está presente en esta posición en particular, entonces la variable será verdadera y, si no, falsa. Hacemos esto para todas las figuras.

Ahora elaboremos una fórmula que describa nuestro problema, es decir, en realidad impondremos restricciones a nuestras variables. Lo primero que debe hacer es asegurarse de que todas las celdas de nuestro campo de juego estarán cubiertas con al menos una figura. Para hacer esto, para cada celda de 64, encontramos todas las figuras y posiciones de estas figuras que cubren esta celda y componimos una cláusula a partir de las variables que se asignan a estas posiciones de las figuras. Lo segundo que debe hacer es eliminar la intersección de las formas. Esto se puede hacer en un ciclo doble, simplemente clasificando todas las posiciones posibles de todas las figuras y determinando si el par tiene celdas comunes. Si lo hay, entonces se cruzan y necesita agregar una cláusula de la forma (no x_i V no x_j), donde x_i es la variable asignada a la primera posición, y x_j es la segunda posición. Esta cláusula es verdadera cuando x_i y x_j no son iguales a uno al mismo tiempo, es decir, excluye intersecciones. Y finalmente, la tercera cosa a considerar es que cada figura puede estar presente en el campo de juego solo una vez. Para hacer esto, también revisamos todas las posiciones de cada figura en un ciclo doble y para cada par de posiciones de la misma figura hacemos una cláusula similar a la anterior y que consta de dos negativos. Es decir, cuando aparecen dos figuras idénticas (pero en diferentes posiciones), una de estas cláusulas dará falso y, en consecuencia, excluirá dicha solución.

Todo era una teoría, y ahora pasemos a la práctica. Cada figura tiene un número del 1 al d para distinguirla de otras e imprimir convenientemente. Luego cree una matriz del campo de juego y codifique las celdas correspondientes del campo de juego como ocupadas / no ocupadas por la figura:

. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 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 . . . . . .

Ahora, para cada pieza, es necesario encontrar todas las posiciones posibles en el campo de juego mediante turnos, giros y reflexiones. Comencemos con giros y reflexiones. En total, hay 8 posibles transformaciones de giros y reflexiones, incluida una transformación trivial que deja la figura intacta. Para estas transformaciones, creo 8 matrices correspondientes, como se muestra a continuación. Después de la rotación o reflexión, la figura puede ir más allá del campo de juego, por lo que es necesario devolverla nuevamente al campo de juego. También debe tenerse en cuenta que algunas figuras pueden transformarse en sí mismas después de la transformación, y tales casos deben excluirse. Agrego opciones únicas a la clase de Orientación. El resultado es el siguiente código:

  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; } 

Este código se aplica a cada una de las figuras, y luego, las orientaciones únicas recibidas se desplazan a lo largo de los ejes xey creando todas las posiciones posibles de cada figura. Como resultado, tenemos el siguiente número de posiciones diferentes para cada una de las figuras:

---------- 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

Luego asignamos una variable booleana a cada posición posible y creamos una fórmula, como se describió anteriormente. Después de eso, llamamos a minisat directamente desde la aplicación, que devuelve una solución: un conjunto de nuestras variables con los valores asignados verdadero o falso. Sabiendo a qué posiciones se asignaron estas variables, imprimimos la solución:

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


Que sigue

Naturalmente, detenerse en esto no sería tan interesante. Por lo tanto, la primera pregunta que surgió para mí fue "¿cuántas soluciones diferentes existen que no difieren en giros triviales y reflexiones del campo de juego?". Para hacer esto, hay un modo en el solucionador SAT que le permite agregar cláusulas sin perder la información existente, lo que acelera significativamente el proceso en comparación con como si la solución se buscara desde cero. La siguiente solución se puede encontrar agregando una cláusula que contenga la negación de todas las variables presentes en la solución anterior. Después de agregar este procedimiento y comparar la nueva solución con las anteriores, teniendo en cuenta los giros y las reflexiones del campo de juego, obtuve 1364 opciones diferentes.

Otra extensión interesante que implementé fue el estudio de varias otras formas del campo de juego y las figuras. Y finalmente, el estudio de los campos de juego tridimensionales fue muy interesante. Pero este es un tema para otro artículo.

Actualización

Después de agregar una condición adicional: para cada figura de una cláusula: debe haber al menos una posición de esta figura en el campo de juego, el cálculo se ha vuelto mucho más rápido. Además, se ha solucionado un error, como resultado de lo cual el número de todas las opciones únicas posibles es 16146.