Решение японских кроссвордов с помощью SAT солвера

в 14:59, , рубрики: sat, Алгоритмы, японские кроссворды

На Хабре было несколько статей по решению японских кроссвордов, где авторы придумывали различные способы как такие кроссворды решать. В комментарии к статье Решение цветных японских кроссвордов со скоростью света я высказал мысль, что, поскольку, решение японских кроссвордов является NP-полной задачей, то и решать их надо с использованием соответствующего инструмента, а именно SAT солвером. Поскольку моя идея была встречена весьма скептически, я решил попробовать ее реализовать и сравнить результаты с другими подходами. Что из этого получилось можно узнать под катом.

Как известно, японский кроссворд или номограмма — это логическая головоломка в которой необходимо восстановить изображение в прямоугольнике с помощью чисел, расположенных слева в заголовках строк и сверху в заголовках столбцов. Эти числа соответствуют порядку и длине блоков закрашенных подряд клеток в соответствующей строке или столбце, причем при установке блоков между ними должна быть хотя бы одна незакрашенная клетка. Здесь я рассматриваю только двуцветные кроссворды, где каждая клетка может быть либо закрашенной либо нет. Фактически, для решения этой задачи необходимо найти позицию каждого блока. Следует отметить, что задача может иметь как одно так и несколько решений, а также не иметь решений вообще. Об этом солвер должен также сообщать.

Легко понять, что задача в общем случае является переборной и авторы многочисленных приложений пытаются найти наиболее быстрый алгоритм решения путем написания собственных велосипедов разных ухищрений, вместо того, чтобы использовать хорошо разработанные методы, используемые в задаче выполнимости булевых формул (Boolean satisfiability problem). Однако, это утверждение требует доказательства, поэтому я решил переформулировать задачу решения японского кроссворда в конъюнктивно-нормальную форму и использовать один из известных SAT солверов для ее решения, чтобы подтвердить его или опровергнуть.

Для представления этой задачи в конъюнктивно-нормальной форме, введем по одной булевой переменной для каждой клетки поля и по одной переменой для каждой возможной позиции каждого блока в строках и столбцах. Для клетки поля булева переменая будет означать, окрашена данная клетка или нет, а для позиции блока булева переменная будет означать, присутствует ли данный блок на этой позиции или нет. Запишем необходимые соотношения между переменными (клозы):

1. Каждый блок, объявленный в строке или столбце обязан появиться хотя-бы в одной позиции. Этому соответствует клоз вида (X1 V X2 V… XN), где X1, X2… XN — все возможные позиции данного блока в строке или столбце.

2. Каждый блок в строке или столбце должен появиться не более одного раза. Этому соответствует множество клозов вида (not Xi) V (not Xj), где Xi, Xj (i != j) — все возможные позиции данного блока в строке или столбце.

3. Правильный порядок блоков. Поскольку необходимо поддерживать правильный порядок расположения блоков, а также исключить их пересечение, необходимо добавить клозы, вида (not Xi) V (not Xj), где Xi, Xj — переменные, соответствующие позициям разных блоков, которые имеют неправильный порядок или пересекаются.

4. Окрашенная клетка должна содержаться внутри хотя бы одного блока, позиция которого включает данную клетку. Этому соответствует клоз вида ((not Xk) V X1 V X2… XN), где Xk — переменная, соответствующая клетке, а X1, X2… XN — переменные, соответствующие позициям блоков, содержащих данную клетку.

5. Каждая пустая клетка не должна содержаться ни в одной возможной позиции ни одного блока. Этому соответствует множество клозов вида Xi V (not Xj), где Xi — переменная, соответствующая клетке, а Xj — переменная, соответствующая одной позиции какого-либо блока, содержащая данную клетку.

Таким образом, задача сформулирована в виде конъюнктивно-нормальной формы и может быть решена с помощью SAT солвера. При этом если решения не существует, SAT солвер определит, что решения нет.

Теперь настал черед подтвердить или опровергнуть мое предположение о том, что SAT солвер справится с решением японских кроссвордов быстрее, чем другие алгоритмы. Для проверки этого я взял примеры с сайта Survey of Paint-by-Number Puzzle Solvers. На данном сайте есть таблица сравнения скорости работы различных приложений для решения японских кроссвордов и хороший набор примеров — от самых легких, которые решаются всеми, до сложных, которые решает только одно приложение. Эти результаты были получены на компьютере с CPU 2.6GHz AMD Phenom II X4 810 quad-core 64-bit processor Memory: 8 Gb. Я использовал компьютер Intel® Core(TM) i7-2600K CPU @ 3.40GHz Memory 16 Gb.

В результате, я получил следующие результаты:

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

Какие из этого можно сделать выводы?

  1. SAT солвер решил все примеры, которые решаются другими приложениями, даже webpbn-22336, который решается только одним приложением.
  2. SAT солвер легко решает много примеров, которые не могут быть решены большинством приложений.
  3. Время решения в большинстве случаев лучше у SAT солвера, чем у других приложений.
  4. Я использовал однопоточный SAT солвер, если использовать многопоточный SAT солвер, результаты будут еще лучше.
  5. При использовании SAT солвера нет необходимости изобретать свои алгоритмы, которые уже, с большой вероятностью, кто-то изобретёл.

В заключении можно добавить, что SAT солвер может получать более одного решения, если таковые существуют. Для этого необходимо добавить один клоз вида ((not X1) V (not X2) V… (not XN)), где X1, X2… XN — переменные, соответствующие закрашенным клеткам в предыдущем решении.

Автор: andy_p

Источник


* - обязательные к заполнению поля


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js