Хабрахабр

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

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

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

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

Каждый блок, объявленный в строке или столбце обязан появиться хотя-бы в одной позиции. 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 солвера.

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

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть