Как стать автором
Обновить

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

А исходники в открытом виде есть?
Я пробовал два — glucose 3.0 и lingeling.

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

Я имел в виду исходники самого решения на солвере.
Я добавил в свой солвер опцию для использования SAT-солвера, некоторые кроссворды стали решаться в сотни раз быстрее, чем с моим на коленке написанным бэктрэкингом. На основе идей из этой статьи вот такой получился код, если кому-то еще интересно. В ближайшее время планирую дополнить алгоритм генерации дизъюнктов и для цветных кроссвордов тоже.
Как раз проходили в универе эту формулу. Спасибо, так сказать, за пример из реально жизни, получилось довольно интересно :)
Спасибо вам за статью!

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

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

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

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

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

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

Solver started. vars = 150
Clauses = 562

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

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

8

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

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

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

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

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

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

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

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

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

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


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

Публикации

Истории