Решение японских кроссвордов с помощью 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™ 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
Какие из этого можно сделать выводы?
- SAT солвер решил все примеры, которые решаются другими приложениями, даже webpbn-22336, который решается только одним приложением.
- SAT солвер легко решает много примеров, которые не могут быть решены большинством приложений.
- Время решения в большинстве случаев лучше у SAT солвера, чем у других приложений.
- Я использовал однопоточный SAT солвер, если использовать многопоточный SAT солвер, результаты будут еще лучше.
- При использовании SAT солвера нет необходимости изобретать свои алгоритмы, которые уже, с большой вероятностью, кто-то изобретёл.
В заключении можно добавить, что SAT солвер может получать более одного решения, если таковые существуют. Для этого необходимо добавить один клоз вида ((not X1) V (not X2) V… (not XN)), где X1, X2… XN — переменные, соответствующие закрашенным клеткам в предыдущем решении.
