Em Habré, havia vários artigos sobre como resolver palavras cruzadas em japonês, onde os autores criaram várias maneiras de resolver tais palavras cruzadas. No comentário ao artigo
Resolvendo palavras cruzadas em cores japonesas com a velocidade da luz, sugeri que, como resolver palavras cruzadas em japonês é um problema completo do NP, elas devem ser resolvidas usando a ferramenta apropriada, a saber, o solucionador SAT. Como minha idéia foi recebida com ceticismo, decidi tentar implementá-la e comparar os resultados com outras abordagens. O que veio disso pode ser encontrado sob o corte.
Como você sabe, palavras cruzadas ou nomograma em japonês são um quebra-cabeça lógico no qual você precisa restaurar a imagem em um retângulo usando os números localizados à esquerda nos cabeçalhos das linhas e acima nos cabeçalhos das colunas. Esses números correspondem à ordem e comprimento dos blocos de células preenchidas sucessivamente na linha ou coluna correspondente e, ao instalar blocos, deve haver pelo menos uma célula vazia entre eles. Aqui considero apenas palavras cruzadas de duas cores, nas quais cada célula pode ser pintada ou não. De fato, para resolver esse problema, é necessário encontrar a posição de cada bloco. Note-se que uma tarefa pode ter uma ou várias soluções, bem como nenhuma solução. O solucionador também deve relatar isso.
É fácil entender que o problema no caso geral é exaustivo e os autores de inúmeras aplicações tentam encontrar o algoritmo de solução mais rápido
escrevendo suas próprias bicicletas de vários truques, em vez de usar os métodos bem desenvolvidos usados no problema de satisfação booleana. No entanto, essa declaração requer prova, então decidi reformular o problema de resolver as palavras cruzadas japonesas de uma forma conjuntamente normal e usar um dos conhecidos solucionadores SAT para resolvê-lo, confirmá-lo ou refutá-lo.
Para representar esse problema de forma conjuntamente normal, introduzimos uma variável booleana para cada célula no campo e uma variável para cada posição possível de cada bloco em linhas e colunas. Para uma célula de um campo booleano, uma variável significará se uma determinada célula é colorida ou não e, para uma posição de um bloco booleano, uma variável significará se esse bloco está presente nessa posição ou não. Escrevemos as relações necessárias entre as variáveis (cláusulas):
1. Cada bloco declarado em uma linha ou coluna deve aparecer pelo menos em uma posição. Isso corresponde a uma cláusula do formulário (X1 V X2 V ... XN), em que X1, X2 ... XN são todas as posições possíveis desse bloco em uma linha ou coluna.
2. Cada bloco em uma linha ou coluna deve aparecer não mais de uma vez. Isso corresponde a muitas cláusulas do formulário (não Xi) V (não Xj), em que Xi, Xj (i! = J) são todas as posições possíveis desse bloco em uma linha ou coluna.
3. A ordem correta dos blocos. Como é necessário manter a ordem correta de arranjo dos blocos, bem como eliminar sua interseção, é necessário adicionar cláusulas da forma (não Xi) V (não Xj), onde Xi, Xj são variáveis correspondentes às posições dos diferentes blocos que têm a ordem ou interseção incorreta.
4. Uma célula manchada deve estar contida em pelo menos um bloco cuja posição inclua essa célula. Isso corresponde a uma cláusula do formulário ((não Xk) V X1 V X2 ... XN), onde Xk é a variável correspondente à célula e X1, X2 ... XN são as variáveis correspondentes às posições dos blocos que contêm essa célula.
5. Cada célula vazia não deve estar contida em nenhuma posição possível de um único bloco. Isso corresponde a muitas cláusulas no formato Xi V (não Xj), onde Xi é a variável correspondente à célula e Xj é a variável correspondente a uma posição de qualquer bloco que contenha essa célula.
Assim, o problema é formulado na forma de uma forma conjuntamente normal e pode ser resolvido usando o solucionador SAT. Além disso, se não houver solução, o solucionador SAT determinará que não há solução.
Agora chegou a hora de confirmar ou refutar minha suposição de que o solucionador SAT lidará com a resolução de palavras cruzadas em japonês mais rapidamente do que outros algoritmos. Para verificar isso, peguei exemplos no site
Survey of Paint-by-Number Puzzle Solvers . Neste site, há uma tabela comparando a velocidade de vários aplicativos para resolver palavras cruzadas em japonês e um bom conjunto de exemplos - dos mais leves, que são resolvidos por todos, aos complexos, que apenas um aplicativo resolve. Esses resultados foram obtidos em um computador com processador AMD Phenom II X4 810 de quatro núcleos e CPU de 2,6 GHz e memória de 8 Gb. Usei um computador Intel® Core (TM) CPU i7-2600K a 3,40GHz de memória de 16 Gb.
Como resultado, obtive os seguintes 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
Que conclusões podem ser tiradas disso?
- O solucionador SAT resolveu todos os exemplos resolvidos por outros aplicativos, mesmo o webpbn-22336, que é resolvido por apenas um aplicativo.
- O SAT Solver resolve facilmente muitos exemplos que não podem ser resolvidos pela maioria das aplicações.
- Na maioria dos casos, o tempo de solução é melhor para o solucionador SAT do que para outras aplicações.
- Usei um solucionador SAT de rosca única; se você usar um solucionador SAT de rosca múltipla, os resultados serão ainda melhores.
- Ao usar o solucionador SAT, não há necessidade de inventar seus próprios algoritmos, que já, com alta probabilidade, alguém inventaram.
Em conclusão, podemos acrescentar que o solucionador SAT pode receber mais de uma solução, se houver. Para fazer isso, adicione uma cláusula do formulário ((não X1) V (não X2) V ... (não XN)), em que X1, X2 ... XN são as variáveis correspondentes às células preenchidas na solução anterior.