16.12.2018 14:59
andy_p 33 10400 Источник
На Хабре было несколько статей по решению японских кроссвордов, где авторы придумывали различные способы как такие кроссворды решать. В комментарии к статье Решение цветных японских кроссвордов со скоростью света я высказал мысль, что, поскольку, решение японских кроссвордов является 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 — переменные, соответствующие закрашенным клеткам в предыдущем решении.

Комментарии (33)


  1. KvanTTT
    16.12.2018 18:18
    #19506894

    А исходники в открытом виде есть?


    1. qw1
      16.12.2018 23:29
      #19507622

      Так-то их полно, https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Offline_SAT_solvers

      Интересно, каким пользовался автор.


      1. andy_p Автор
        16.12.2018 23:36
        #19507630
        +1

        Я пробовал два — glucose 3.0 и lingeling.


        1. alan008
          17.12.2018 17:58
          #19511718

          KvanTTT имел в виду исходники самого решения на солвере.


      1. KvanTTT
        17.12.2018 00:16
        #19507712
        +1

        Я имел в виду исходники самого решения на солвере.


  1. Igor_ku
    16.12.2018 23:36
    #19507632

    Как раз проходили в универе эту формулу. Спасибо, так сказать, за пример из реально жизни, получилось довольно интересно :)


  1. Hixon10
    17.12.2018 01:40
    #19507830
    +1

    Спасибо вам за статью!

    Очень приятно видеть, как выкладки из computer science применяются в реальной жизни. А решение задачи через сводимость — это вообще бомба. Отличный пример того, что алгоритмы в институте учить нужно, и они применимы на практике.


    1. andy_p Автор
      17.12.2018 09:32
      #19508408

      Почитайте другие мои статьи здесь на Хабре про использование SAT солверов.


  1. DustCn
    17.12.2018 02:59
    #19507924

    Валидацию бы решения добавить. Время работы, по идее, должно возрастать с увеличением задачи. В приведенных данных зависимость есть, но иногда сильно быстрее получается. Если задача с полным перебором — это странно.
    Я не видел исходников и сужу только по косвенным данным, вполне возможно что там все правильно.


  1. anonymous
    17.12.2018 09:04
    #19508344

    В статье webpbn.com/survey автор пишет о 'Solving vs. Validation':

    A program to do puzzle validation has a bit of a tougher job than a simple solver. A solver can stop after finding one solution. A validator must try to find a second. In the case of a puzzle that only has one solution, it must completely explore the solution space, eliminating every possible alternative solution.

    Далее он сравнивает в основном солверы, которые могут находить более одного решения.
    In the run-time tests performed for this survey, I always ask the solvers to find two solutions, unless the solver doesn't support that option.
    Как я понял по вашему описанию, сейчас бенчмарки замеряют режим «найти первое возможное решение и выйти». Для корректного сравнения с другими солверами возможно правильнее все же сравнивать в режиме «найти как минимум два решения».


    1. andy_p Автор
      17.12.2018 09:11
      #19508358

      Есть режим поиска 10 первых решений. Следующие решения находятся очень быстро, поскольку SAT солвер использует знание, оставшееся от поиска первого решения.


    1. RedStone
      17.12.2018 10:29
      #19508602

      Вы хотите найти два разных решения для одного и того же японского кроссворда?
      По-хорошему тут нужна некая внешняя валидация. Когда выхлоп от SAT-решателя обрабатывается и сравнивается с известным решением для этого кроссворда. Всегда есть вероятность, что решатель случайно попал в правильное решение, просто потому что в задаче может быть огромное число переменных и он что-то там подобрал, чтобы сделать КНФ истинной, но начальные условия оставляют ровно один вариант, если всё-таки нашлось какое-то другое решение и кодировка 100% правильная, то значит плохой решатель.


      1. anonymous
        17.12.2018 10:56
        #19508756

        Не нужно никакой внешней валидации. Вся валидация решения сводится к тому, чтобы из найденного решения сгенерировать описания строк и столбцов (это тривиальная операция) и сравнить их с начальными описаниями.


        1. RedStone
          17.12.2018 11:04
          #19508814

          Ровно это я и назвал внешней валидацией, потому что она проходит вне SAT решателя.


          1. andy_p Автор
            17.12.2018 11:37
            #19508986

            Ну для быстрой валидации достаточно взглянуть на сгенертрованную картинку. Я же вввожу результат в таком виде.


  1. RedStone
    17.12.2018 09:04
    #19508346

    Клоз == дизъюнкт. Второй вариант всё-таки как-то лучше звучит. Да и в дискретке вы не найдете термина «клоз».
    Как уже выше отмечали — неплохо бы привести результат. Выполняющий набор для какого-нибудь небольшого примера. Циферки-то может и красивые, а вот что за ними прячется не ясно.


    1. andy_p Автор
      17.12.2018 09:17
      #19508376

      Клоз — это русскоязычный разговорный термин от английского clause.
      Например, как «хард диск» происходит от «hard disk».


      1. RedStone
        17.12.2018 09:28
        #19508392

        Вы простите меня, но я попробовал вчитаться, появились вопросы к вашему алгоритму, было бы круто, если бы был ещё пример кодирования японского кроссворда по вашему алгоритму.
        Самое первое — фактически вы работаете с матрицей n*m, а у всех переменных по одному индексу. Понятно, что в формулах подразумеваются именно переменные из уже готовой SAT кодировки, но формулы воспринимаются очень трудно.
        Не понятно что скрывается за словом «блок», для человека не решавшего японские кроссворды, смутно припоминаю, что цифрами на полях задаётся число закрашенных клеток подряд ну и собственно порядок таких последовательностей. А какой смысл вкладывается в это понятие в смысле SAT кодировки?
        Второе условие вообще не должно оказывать никакого влияния на количество появлений «блока», потому что это дизъюнкт. Допустим у нас три возможных позиции блока, пусть им соответствуют переменные с номерами 1, 2, 3. Если блок может стоять в позициях 1 и 2(соответственно они истины, а 3 ложная), то по формуле два получим -1V-2V-3, это можно переписать как (false V false V true == true). Получается, что единственный вариант, когда это «ограничение» сыграет, это ситуация, когда блок может стоять где угодно. Для подобных ограничений лучше использовать XOR, это я по своему опыту говорю.
        То же самое про шаг 3, он ничего не ограничивает.
        В шагах 4 и 5 я вообще ничего не понял.
        Не имея «на руках» доказательств решения этих кроссвордов, я могу говорить, что что-то у вас там находится, но в ряд ли это то, что надо.


        1. andy_p Автор
          17.12.2018 09:36
          #19508424

          > Допустим у нас три возможных позиции блока, пусть им соответствуют переменные с номерами 1, 2, 3

          Нет, для исключения дублирования сгенерятся три клоза:
          -1 V -2
          -1 V -3
          -2 V -3

          XOR не в днф не поддерживается.


    1. andy_p Автор
      17.12.2018 09:27
      #19508388

      > Как уже выше отмечали — неплохо бы привести результат. Выполняющий набор для какого-нибудь небольшого примера. Циферки-то может и красивые, а вот что за ними прячется не ясно.

      Да это запросто, только это будет немаленький файл в формате DIMACS. Даже самый маленький пример имеет 150 переменных и 562 клоза:

      Solver started. vars = 150
      Clauses = 562


      1. RedStone
        17.12.2018 09:30
        #19508394

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


        1. andy_p Автор
          17.12.2018 09:39
          #19508428

          Я лучше исходник выложу, а там сами генерите.


          1. RedStone
            17.12.2018 10:22
            #19508558

            Не сочтите меня грубияном, но при наличии хорошего текстового описания алгоритма, я должен быть в состоянии написать код сам. А в том, что написано у вас я всё ещё мало что понял.
            В пункте 2 вы меня убедили, был невнимателен. Если вы не против несколько вопросов про пункт 1. Блок это несколько закрашенных клеток подряд? Переменные X1...XN это все клетки строки или столбца? Каким образом формула из первого шага связана с конкретным блоком?


            1. andy_p Автор
              17.12.2018 11:42
              #19509024

              Нет, все проще. Например, есть один блок в строке длиной три. Строка имеет длину 10. Стало быть, существует 7 возможных позиций этого блока в строке. Каждой такой позиции соответстаует одна переменная. Поскольку блог должен стоять где-то в этой строке, хотя-бы одна переменная должна быть true. Из этого следует условие 1.


              1. hfinn
                17.12.2018 11:47
                #19509064

                8


                1. andy_p Автор
                  17.12.2018 11:52
                  #19509100

                  Сорри, ошибся. Конечно 8.


                  1. hfinn
                    17.12.2018 12:18
                    #19509308

                    Свой алгоритм когда отлаживал, тоже путался. Спасибо за ссылку на webpbn, странно, что она мне не попалась раньше.


  1. amarao
    17.12.2018 11:50
    #19509080

    Первый раз вижу кальку clause как «клоз». Условие?


    1. slavam2605
      17.12.2018 20:16
      #19512424

      К сожалению, clause — устоявшийся термин в англоязычной литературе, а так как большинство статей публикуются на английском, неизбежно вырос рускоязычный сленг «клоз». Среди коллег еще иногда использовался вариант «скобки».


  1. SerVB
    18.12.2018 17:57
    #19517934

    Тоже благодарю за описание применения SAT. Мне как студенту интересно узнавать приложения того, что изучаю. Тем более, что сам иногда на досуге решаю нонограммы :)
    Тем не менее, если подходить к вопросу занудно, вижу проблему. Японские кроссворды должны решаться только логикой, но не перебором. Если решение единственно, Ваш алгоритм выдаст правильный ответ. Но если решений несколько? Насколько я понял, алгоритм не делит решения на "правильные" и "подходящие". Я вот только не знаю, есть ли нонограммы, у которых логически есть только одно решение, но формально подходит несколько раскрасок. Если такие существуют, Ваш алгоритм может давать неправильные ответы на них. Если не существуют, то это хорошо. В любом случае, Ваш солвер будет давать решения на невозможные для решения кроссворды вроде «Зимы» с Вики: https://ru.m.wikipedia.org/wiki/Японский_кроссворд .


    1. KvanTTT
      19.12.2018 10:44
      #19520850
      +1

      Японские кроссворды должны решаться только логикой, но не перебором.

      Что значит логикой? SAT — это и есть логика, которая сильно оптимизирует перебор.


      1. SerVB
        19.12.2018 14:11
        #19522190

        Под словом «логика» имеется в виду не булевская логика, а логика-алгоритм решения. Нельзя гадать, нужно поочередно закрашивать клетки, где точно будет рисунок, и помечать те клетки, где точно рисунка нет. В нонограммах утверждается, что такой легкий алгоритм обязан привести к единственному ответу. А если не приводит, то нонограмма неправильна.
        Но выполнимость SAT – это как раз перебор, а не логика, говоря моими терминами.


    1. anonymous
      19.12.2018 11:55
      #19521232

      Я вот только не знаю, есть ли нонограммы, у которых логически есть только одно решение, но формально подходит несколько раскрасок.

      Насколько я понял под «логически» вы понимаете метод решения line-by-line, в котором не используются методы вида «закрасим вот эту произвольную клетку и посмотрим, что будет дальше». С этой точки зрения все паззлы можно разделить на два больших класса: те, которые решаются итеративным применением построчных алгоритмов (логические) и все остальные.

      Так вот первая группа паззлов всегда имеет не более одного решения (то, к которому и можно прийти «логически»). С точки зрения солвера сложных паззлов (второй группы) нет никакого разделения между «правильным» и «подходящим» решениями — они все правильные. Другой вопрос в том, что составитель паззла, скорее всего, имел ввиду одно из решений.

      Думаю некорректно будет противопоставлять «логику» и «перебор»: cамый популярный метод решения паззлов второй группы — это бэктрекинг, который представляет собой очень даже логичный перебор. Например, указанный вами пример «Зима» — хоть и второго типа, но имеет единственное правильное решение и оно достигается путем единственного логического предположения: «предположим, что клетка (10, 18) — пустая», которое приводит к противоречию. Закрашиваем (10,18) и дальше все решается так же — просто построчно.