En Habré había varios artículos sobre cómo resolver crucigramas japoneses, donde los autores idearon varias formas de cómo resolver dichos crucigramas. En el comentario al artículo
Resolver crucigramas japoneses en color con la velocidad de la luz, sugerí que dado que resolver crucigramas japoneses es un problema de NP completo, deben resolverse utilizando la herramienta adecuada, es decir, el solucionador SAT. Como mi idea se encontró con escepticismo, decidí intentar implementarla y comparar los resultados con otros enfoques. Lo que vino de esto se puede encontrar debajo del corte.
Como sabes, un crucigrama japonés o un nomograma es un rompecabezas lógico en el que debes restaurar la imagen en un rectángulo usando los números ubicados a la izquierda en los encabezados de las filas y arriba en los encabezados de las columnas. Estos números corresponden al orden y la longitud de los bloques de celdas llenas sucesivamente en la fila o columna correspondiente, y al instalar bloques, debe haber al menos una celda vacía entre ellos. Aquí considero solo crucigramas de dos colores, donde cada celda se puede pintar o no. De hecho, para resolver este problema, es necesario encontrar la posición de cada bloque. Cabe señalar que una tarea puede tener una o varias soluciones, así como ninguna solución. El solucionador también debe informar esto.
Es fácil entender que el problema en el caso general es exhaustivo y los autores de numerosas aplicaciones intentan encontrar el algoritmo de solución más rápido
escribiendo sus propias bicicletas de varios trucos, en lugar de utilizar los métodos bien desarrollados utilizados en el problema de la satisfacción booleana. Sin embargo, esta declaración requiere pruebas, así que decidí reformular el problema de resolver el crucigrama japonés en una forma conjuntivamente normal y usar uno de los solucionadores de SAT conocidos para resolverlo, confirmarlo o refutarlo.
Para representar este problema en forma conjuntivamente normal, introducimos una variable booleana para cada celda en el campo y una variable para cada posible posición de cada bloque en filas y columnas. Para una celda de un campo booleano, una variable significará si una celda dada está coloreada o no, y para una posición de un bloque booleano, una variable significará si este bloque está presente en esta posición o no. Escribimos las relaciones necesarias entre las variables (cláusulas):
1. Cada bloque declarado en una fila o columna debe aparecer al menos en una posición. Esto corresponde a una cláusula de la forma (X1 V X2 V ... XN), donde X1, X2 ... XN son todas las posiciones posibles de este bloque en una fila o columna.
2. Cada bloque en una fila o columna no debe aparecer más de una vez. Esto corresponde a muchas cláusulas de la forma (no Xi) V (no Xj), donde Xi, Xj (i! = J) son todas las posiciones posibles de este bloque en una fila o columna.
3. El orden correcto de los bloques. Dado que es necesario mantener el orden correcto de disposición de los bloques, así como eliminar su intersección, es necesario agregar cláusulas de la forma (no Xi) V (no Xj), donde Xi, Xj son variables que corresponden a las posiciones de diferentes bloques que tienen un orden o intersección incorrectos.
4. Una celda manchada debe estar contenida dentro de al menos un bloque cuya posición incluya esta celda. Esto corresponde a una cláusula de la forma ((no Xk) V X1 V X2 ... XN), donde Xk es la variable correspondiente a la celda, y X1, X2 ... XN son las variables correspondientes a las posiciones de los bloques que contienen esta celda.
5. Cada celda vacía no debe estar contenida en ninguna posición posible de un solo bloque. Esto corresponde a muchas cláusulas de la forma Xi V (no Xj), donde Xi es la variable correspondiente a la celda, y Xj es la variable correspondiente a una posición de cualquier bloque que contenga esta celda.
Por lo tanto, el problema se formula en forma de forma conjuntivamente normal y se puede resolver utilizando el solucionador SAT. Además, si no hay solución, el solucionador SAT determinará que no hay solución.
Ahora ha llegado el momento de confirmar o refutar mi suposición de que el solucionador SAT se encargará de resolver crucigramas japoneses más rápido que otros algoritmos. Para verificar esto, tomé ejemplos del sitio web
Survey of Paint-by-Number Puzzle Solvers . En este sitio hay una tabla que compara la velocidad de varias aplicaciones para resolver crucigramas japoneses y un buen conjunto de ejemplos, desde los más livianos que pueden ser resueltos por todos hasta los complejos que solo una aplicación resuelve. Estos resultados se obtuvieron en una computadora con un procesador AMD Phenom II X4 810 de cuatro núcleos a 2.6GHz. Memoria de 64-bit: 8 Gb. Usé una computadora Intel® Core (TM) i7-2600K CPU @ 3.40GHz Memoria 16 Gb.
Como resultado, obtuve los siguientes resultados:
======== sample-nin/webpbn-00001.nin ======== Start read data. 16 lines were read Solver started. vars = 150 Clauses = 562 SATISFIABLE apsnono finished. real 0m0,610s user 0m0,004s sys 0m0,002s ========= sample-nin/webpbn-00006.nin ======== Start read data. 41 lines were read Solver started. vars = 1168 Clauses = 10215 SATISFIABLE apsnono finished. real 0m0,053s user 0m0,028s sys 0m0,000s ========= sample-nin/webpbn-00016.nin ======== Start read data. 69 lines were read Solver started. vars = 7484 Clauses = 191564 SATISFIABLE apsnono finished. real 0m0,368s user 0m0,186s sys 0m0,008s ========= sample-nin/webpbn-00021.nin ======== Start read data. 40 lines were read Solver started. vars = 1240 Clauses = 11481 SATISFIABLE apsnono finished. real 0m0,095s user 0m0,034s sys 0m0,000s ========= sample-nin/webpbn-00023.nin ======== Start read data. 22 lines were read Solver started. vars = 311 Clauses = 1498 SATISFIABLE apsnono finished. real 0m0,147s user 0m0,006s sys 0m0,000s ========= sample-nin/webpbn-00027.nin ======== Start read data. 51 lines were read Solver started. vars = 2958 Clauses = 38258 SATISFIABLE apsnono finished. real 0m0,089s user 0m0,050s sys 0m0,010s ========= sample-nin/webpbn-00065.nin ======== Start read data. 75 lines were read Solver started. vars = 7452 Clauses = 134010 SATISFIABLE apsnono finished. real 0m0,272s user 0m0,166s sys 0m0,009s ========= sample-nin/webpbn-00436.nin ======== Start read data. 76 lines were read Solver started. vars = 6900 Clauses = 134480 SATISFIABLE apsnono finished. real 0m0,917s user 0m0,830s sys 0m0,005s ========= sample-nin/webpbn-00529.nin ======== Start read data. 91 lines were read Solver started. vars = 10487 Clauses = 226237 SATISFIABLE apsnono finished. real 0m0,286s user 0m0,169s sys 0m0,005s ========= sample-nin/webpbn-00803.nin ======== Start read data. 96 lines were read Solver started. vars = 9838 Clauses = 278533 SATISFIABLE apsnono finished. real 0m0,827s user 0m0,697s sys 0m0,008s ========= sample-nin/webpbn-01611.nin ======== Start read data. 116 lines were read Solver started. vars = 25004 Clauses = 921246 SATISFIABLE apsnono finished. real 0m3,467s user 0m3,301s sys 0m0,084s ========= sample-nin/webpbn-01694.nin ======== Start read data. 96 lines were read Solver started. vars = 13264 Clauses = 391427 SATISFIABLE apsnono finished. real 0m0,964s user 0m0,822s sys 0m0,016s ========= sample-nin/webpbn-02040.nin ======== Start read data. 116 lines were read Solver started. vars = 26445 Clauses = 1182535 SATISFIABLE apsnono finished. real 0m7,512s user 0m7,354s sys 0m0,122s ========= sample-nin/webpbn-02413.nin ======== Start read data. 41 lines were read Solver started. vars = 1682 Clauses = 15032 SATISFIABLE apsnono finished. real 0m0,258s user 0m0,053s sys 0m0,001s ========= sample-nin/webpbn-02556.nin ======== Start read data. 111 lines were read Solver started. vars = 11041 Clauses = 340630 SATISFIABLE apsnono finished. real 0m0,330s user 0m0,136s sys 0m0,009s ========= sample-nin/webpbn-02712.nin ======== Start read data. 95 lines were read Solver started. vars = 13212 Clauses = 364416 SATISFIABLE apsnono finished. real 0m6,503s user 0m6,365s sys 0m0,032s ========= sample-nin/webpbn-03541.nin ======== Start read data. 111 lines were read Solver started. vars = 19249 Clauses = 676595 SATISFIABLE apsnono finished. real 0m5,008s user 0m4,785s sys 0m0,100s ========= sample-nin/webpbn-04645.nin ======== Start read data. 121 lines were read Solver started. vars = 19159 Clauses = 793580 SATISFIABLE apsnono finished. real 0m4,739s user 0m4,477s sys 0m0,107s ========= sample-nin/webpbn-06574.nin ======== Start read data. 51 lines were read Solver started. vars = 2932 Clauses = 33191 SATISFIABLE apsnono finished. real 0m0,231s user 0m0,176s sys 0m0,000s ========= sample-nin/webpbn-06739.nin ======== Start read data. 81 lines were read Solver started. vars = 10900 Clauses = 256833 SATISFIABLE apsnono finished. real 0m0,782s user 0m0,730s sys 0m0,008s ========= sample-nin/webpbn-07604.nin ======== Start read data. 111 lines were read Solver started. vars = 18296 Clauses = 478535 SATISFIABLE apsnono finished. real 0m1,524s user 0m1,324s sys 0m0,026s ========= sample-nin/webpbn-08098.nin ======== Start read data. 39 lines were read Solver started. vars = 1255 Clauses = 10950 SATISFIABLE apsnono finished. real 0m0,216s user 0m0,133s sys 0m0,000s ========= sample-nin/webpbn-09892.nin ======== Start read data. 91 lines were read Solver started. vars = 13887 Clauses = 419787 SATISFIABLE apsnono finished. real 0m12,048s user 0m11,858s sys 0m0,088s ========= sample-nin/webpbn-10088.nin ======== Start read data. 116 lines were read Solver started. vars = 23483 Clauses = 1020515 SATISFIABLE apsnono finished. real 0m17,472s user 0m16,795s sys 0m0,321s ========= sample-nin/webpbn-10810.nin ======== Start read data. 121 lines were read Solver started. vars = 25726 Clauses = 895436 SATISFIABLE apsnono finished. real 0m0,898s user 0m0,562s sys 0m0,026s ========= sample-nin/webpbn-12548.nin ======== Start read data. 88 lines were read Solver started. vars = 13685 Clauses = 486012 SATISFIABLE apsnono finished. real 3m1,682s user 2m58,537s sys 0m1,507s ========= sample-nin/webpbn-18297.nin ======== Start read data. 79 lines were read Solver started. vars = 9708 Clauses = 272394 SATISFIABLE apsnono finished. real 0m16,643s user 0m16,326s sys 0m0,210s ========= sample-nin/webpbn-22336.nin ======== Start read data. 159 lines were read Solver started. vars = 67137 Clauses = 5420886 SATISFIABLE apsnono finished. real 1m46,555s user 1m43,336s sys 0m3,075s
¿Qué conclusiones se pueden sacar de esto?
- El solucionador SAT resolvió todos los ejemplos que resuelven otras aplicaciones, incluso webpbn-22336, que solo resuelve una aplicación.
- El solucionador SAT resuelve fácilmente muchos ejemplos que la mayoría de las aplicaciones no pueden resolver.
- En la mayoría de los casos, el tiempo de solución es mejor para el solucionador SAT que para otras aplicaciones.
- Utilicé un solucionador SAT de subproceso único; si utiliza un solucionador SAT de subproceso múltiple, los resultados serán aún mejores.
- Al usar el solucionador SAT, no hay necesidad de inventar sus propios algoritmos, que ya, con una alta probabilidad, alguien inventó.
En conclusión, podemos agregar que el solucionador SAT puede recibir más de una solución, si la hay. Para hacer esto, agregue una cláusula de la forma ((no X1) V (no X2) V ... (no XN)), donde X1, X2 ... XN son las variables correspondientes a las celdas rellenas en la solución anterior.