Sur Habré, il y avait plusieurs articles sur la résolution des mots croisés japonais, où les auteurs ont trouvé différentes façons de résoudre ces mots croisés. Dans le commentaire de l'article
Résoudre les mots croisés de couleur japonaise avec la vitesse de la lumière, j'ai suggéré que puisque la résolution des mots croisés japonais est un problème NP-complet, ils doivent être résolus en utilisant l'outil approprié, à savoir le solveur SAT. Puisque mon idée a été accueillie avec scepticisme, j'ai décidé d'essayer de la mettre en œuvre et de comparer les résultats avec d'autres approches. Ce qui en est ressorti se trouve sous la coupe.
Comme vous le savez, un mot croisé ou un nomogramme japonais est un casse-tête logique dans lequel vous devez restaurer l'image dans un rectangle en utilisant les chiffres situés à gauche dans les en-têtes de ligne et au-dessus dans les en-têtes de colonne. Ces nombres correspondent à l'ordre et à la longueur des blocs de cellules remplies successivement dans la ligne ou la colonne correspondante, et lors de l'installation des blocs, il doit y avoir au moins une cellule vide entre eux. Ici, je ne considère que les mots croisés bicolores, où chaque cellule peut être peinte ou non. En effet, pour résoudre ce problème, il faut trouver la position de chaque bloc. Il convient de noter qu'une tâche peut avoir une ou plusieurs solutions, ainsi que pas de solutions du tout. Le solveur doit également le signaler.
Il est facile de comprendre que le problème dans le cas général est exhaustif et les auteurs de nombreuses applications essaient de trouver l'algorithme de solution le plus rapide en
écrivant leurs propres vélos de différentes astuces, au lieu d'utiliser des méthodes bien développées utilisées dans le problème de satisfiabilité booléenne. Cependant, cette déclaration nécessite des preuves, j'ai donc décidé de reformuler le problème de la résolution du puzzle de mots croisés japonais sous une forme conjoncturellement normale et d'utiliser l'un des solveurs SAT bien connus pour le résoudre, le confirmer ou le réfuter.
Pour représenter ce problème sous une forme normale conjonctive, nous introduisons une variable booléenne pour chaque cellule du champ et une variable pour chaque position possible de chaque bloc dans les lignes et les colonnes. Pour une cellule d'un champ booléen, une variable signifiera si une cellule donnée est colorée ou non, et pour une position d'un bloc booléen, une variable signifiera si ce bloc est présent à cette position ou non. Nous écrivons les relations nécessaires entre les variables (clauses):
1. Chaque bloc déclaré dans une ligne ou une colonne doit apparaître au moins dans une position. Cela correspond à une clause de la forme (X1 V X2 V ... XN), où X1, X2 ... XN sont toutes les positions possibles de ce bloc dans une ligne ou une colonne.
2. Chaque bloc d'une ligne ou d'une colonne ne doit pas apparaître plus d'une fois. Cela correspond à de nombreuses clauses de la forme (pas Xi) V (pas Xj), où Xi, Xj (i! = J) sont toutes les positions possibles de ce bloc dans une ligne ou une colonne.
3. L'ordre correct des blocs. Puisqu'il est nécessaire de maintenir l'ordre correct de disposition des blocs, ainsi que d'éliminer leur intersection, il est nécessaire d'ajouter des clauses de la forme (pas Xi) V (pas Xj), où Xi, Xj sont des variables correspondant aux positions de différents blocs qui ont le mauvais ordre ou se croisent.
4. Une cellule colorée doit être contenue dans au moins un bloc dont la position inclut cette cellule. Cela correspond à une clause de la forme ((pas Xk) V X1 V X2 ... XN), où Xk est la variable correspondant à la cellule, et X1, X2 ... XN sont les variables correspondant aux positions des blocs contenant cette cellule.
5. Chaque cellule vide ne doit être contenue dans aucune position possible d'un seul bloc. Cela correspond à de nombreuses clauses de la forme Xi V (pas Xj), où Xi est la variable correspondant à la cellule, et Xj est la variable correspondant à une position de tout bloc contenant cette cellule.
Ainsi, le problème est formulé sous la forme d'une forme normale conjonctive et peut être résolu en utilisant le solveur SAT. De plus, s'il n'y a pas de solution, le solveur SAT déterminera qu'il n'y a pas de solution.
Le moment est maintenant venu de confirmer ou de réfuter mon hypothèse selon laquelle le solveur SAT parviendra à résoudre les mots croisés japonais plus rapidement que les autres algorithmes. Pour vérifier cela, j'ai pris des exemples du site Web
Survey of Paint-by-Number Puzzle Solvers . Sur ce site, il y a un tableau comparant la vitesse de diverses applications pour résoudre les mots croisés japonais et un bon ensemble d'exemples - des plus légers, qui sont résolus par tout le monde, aux plus complexes, qu'une seule application résout. Ces résultats ont été obtenus sur un ordinateur équipé d'un processeur AMD Phenom II X4 810 cadencé à 64 bits à 2,6 GHz. Mémoire: 8 Go. J'ai utilisé un ordinateur Intel® Core (TM) i7-2600K avec une mémoire de 3,40 GHz et 16 Go.
En conséquence, j'ai obtenu les résultats suivants:
======== 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
Quelles conclusions peut-on en tirer?
- Le solveur SAT a résolu tous les exemples résolus par d'autres applications, même webpbn-22336, qui est résolu par une seule application.
- Le solveur SAT résout facilement de nombreux exemples qui ne peuvent pas être résolus par la plupart des applications.
- Dans la plupart des cas, le temps de solution est meilleur pour le solveur SAT que pour d'autres applications.
- J'ai utilisé un solveur SAT monothread, si vous utilisez un solveur SAT multithread, les résultats seront encore meilleurs.
- Lorsque vous utilisez le solveur SAT, il n'est pas nécessaire d'inventer vos propres algorithmes, ce que déjà, avec une forte probabilité, quelqu'un a inventé.
En conclusion, nous pouvons ajouter que le solveur SAT peut recevoir plus d'une solution, le cas échéant. Pour ce faire, ajoutez une clause de la forme ((pas X1) V (pas X2) V ... (pas XN)), où X1, X2 ... XN sont les variables correspondant aux cellules remplies dans la solution précédente.