Решение японских кроссвордов с помощью 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 — переменные, соответствующие закрашенным клеткам в предыдущем решении.
    Поделиться публикацией

    Похожие публикации

    Комментарии 36

      +1
      А исходники в открытом виде есть?
        +1
        Так-то их полно, https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Offline_SAT_solvers

        Интересно, каким пользовался автор.
          +2
          Я пробовал два — glucose 3.0 и lingeling.
            0

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

            +4
            Я имел в виду исходники самого решения на солвере.
          0
          Как раз проходили в универе эту формулу. Спасибо, так сказать, за пример из реально жизни, получилось довольно интересно :)
            +2
            Спасибо вам за статью!

            Очень приятно видеть, как выкладки из computer science применяются в реальной жизни. А решение задачи через сводимость — это вообще бомба. Отличный пример того, что алгоритмы в институте учить нужно, и они применимы на практике.
              0
              Почитайте другие мои статьи здесь на Хабре про использование SAT солверов.
              +1
              Валидацию бы решения добавить. Время работы, по идее, должно возрастать с увеличением задачи. В приведенных данных зависимость есть, но иногда сильно быстрее получается. Если задача с полным перебором — это странно.
              Я не видел исходников и сужу только по косвенным данным, вполне возможно что там все правильно.
                0
                В статье 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.
                Как я понял по вашему описанию, сейчас бенчмарки замеряют режим «найти первое возможное решение и выйти». Для корректного сравнения с другими солверами возможно правильнее все же сравнивать в режиме «найти как минимум два решения».
                  0
                  Есть режим поиска 10 первых решений. Следующие решения находятся очень быстро, поскольку SAT солвер использует знание, оставшееся от поиска первого решения.
                    0
                    Вы хотите найти два разных решения для одного и того же японского кроссворда?
                    По-хорошему тут нужна некая внешняя валидация. Когда выхлоп от SAT-решателя обрабатывается и сравнивается с известным решением для этого кроссворда. Всегда есть вероятность, что решатель случайно попал в правильное решение, просто потому что в задаче может быть огромное число переменных и он что-то там подобрал, чтобы сделать КНФ истинной, но начальные условия оставляют ровно один вариант, если всё-таки нашлось какое-то другое решение и кодировка 100% правильная, то значит плохой решатель.
                      0
                      Не нужно никакой внешней валидации. Вся валидация решения сводится к тому, чтобы из найденного решения сгенерировать описания строк и столбцов (это тривиальная операция) и сравнить их с начальными описаниями.
                        0
                        Ровно это я и назвал внешней валидацией, потому что она проходит вне SAT решателя.
                          0

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

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

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

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

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

                        Solver started. vars = 150
                        Clauses = 562

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

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

                                  0
                                  8
                                    0

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

                                      0
                                      Свой алгоритм когда отлаживал, тоже путался. Спасибо за ссылку на webpbn, странно, что она мне не попалась раньше.
                        +2
                        Первый раз вижу кальку clause как «клоз». Условие?
                          –1
                          К сожалению, clause — устоявшийся термин в англоязычной литературе, а так как большинство статей публикуются на английском, неизбежно вырос рускоязычный сленг «клоз». Среди коллег еще иногда использовался вариант «скобки».
                          0

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

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

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

                              0

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

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

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

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

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


                                Не понимаю, почему. Возможно, это можно более строго доказать?..
                              0
                              Такой вопрос: а есть ли поддержка случайности? Чтобы каждый раз получать правильные, но разные решения. Как это можно сдеалть?
                                0
                                Нет, поддержки случайности нет.
                                Если очень хочется, можно запускать SAT солвер с разным seed.

                              Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                              Самое читаемое