Комментарии 37
Интересно, каким пользовался автор.
Очень приятно видеть, как выкладки из computer science применяются в реальной жизни. А решение задачи через сводимость — это вообще бомба. Отличный пример того, что алгоритмы в институте учить нужно, и они применимы на практике.
Я не видел исходников и сужу только по косвенным данным, вполне возможно что там все правильно.
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.Как я понял по вашему описанию, сейчас бенчмарки замеряют режим «найти первое возможное решение и выйти». Для корректного сравнения с другими солверами возможно правильнее все же сравнивать в режиме «найти как минимум два решения».
По-хорошему тут нужна некая внешняя валидация. Когда выхлоп от SAT-решателя обрабатывается и сравнивается с известным решением для этого кроссворда. Всегда есть вероятность, что решатель случайно попал в правильное решение, просто потому что в задаче может быть огромное число переменных и он что-то там подобрал, чтобы сделать КНФ истинной, но начальные условия оставляют ровно один вариант, если всё-таки нашлось какое-то другое решение и кодировка 100% правильная, то значит плохой решатель.
Как уже выше отмечали — неплохо бы привести результат. Выполняющий набор для какого-нибудь небольшого примера. Циферки-то может и красивые, а вот что за ними прячется не ясно.
Например, как «хард диск» происходит от «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 я вообще ничего не понял.
Не имея «на руках» доказательств решения этих кроссвордов, я могу говорить, что что-то у вас там находится, но в ряд ли это то, что надо.
Да это запросто, только это будет немаленький файл в формате DIMACS. Даже самый маленький пример имеет 150 переменных и 562 клоза:
Solver started. vars = 150
Clauses = 562
В пункте 2 вы меня убедили, был невнимателен. Если вы не против несколько вопросов про пункт 1. Блок это несколько закрашенных клеток подряд? Переменные X1...XN это все клетки строки или столбца? Каким образом формула из первого шага связана с конкретным блоком?
Нет, все проще. Например, есть один блок в строке длиной три. Строка имеет длину 10. Стало быть, существует 7 возможных позиций этого блока в строке. Каждой такой позиции соответстаует одна переменная. Поскольку блог должен стоять где-то в этой строке, хотя-бы одна переменная должна быть true. Из этого следует условие 1.
Тоже благодарю за описание применения SAT. Мне как студенту интересно узнавать приложения того, что изучаю. Тем более, что сам иногда на досуге решаю нонограммы :)
Тем не менее, если подходить к вопросу занудно, вижу проблему. Японские кроссворды должны решаться только логикой, но не перебором. Если решение единственно, Ваш алгоритм выдаст правильный ответ. Но если решений несколько? Насколько я понял, алгоритм не делит решения на "правильные" и "подходящие". Я вот только не знаю, есть ли нонограммы, у которых логически есть только одно решение, но формально подходит несколько раскрасок. Если такие существуют, Ваш алгоритм может давать неправильные ответы на них. Если не существуют, то это хорошо. В любом случае, Ваш солвер будет давать решения на невозможные для решения кроссворды вроде «Зимы» с Вики: https://ru.m.wikipedia.org/wiki/Японский_кроссворд .
Японские кроссворды должны решаться только логикой, но не перебором.
Что значит логикой? SAT — это и есть логика, которая сильно оптимизирует перебор.
Под словом «логика» имеется в виду не булевская логика, а логика-алгоритм решения. Нельзя гадать, нужно поочередно закрашивать клетки, где точно будет рисунок, и помечать те клетки, где точно рисунка нет. В нонограммах утверждается, что такой легкий алгоритм обязан привести к единственному ответу. А если не приводит, то нонограмма неправильна.
Но выполнимость SAT – это как раз перебор, а не логика, говоря моими терминами.
Я вот только не знаю, есть ли нонограммы, у которых логически есть только одно решение, но формально подходит несколько раскрасок.
Насколько я понял под «логически» вы понимаете метод решения line-by-line, в котором не используются методы вида «закрасим вот эту произвольную клетку и посмотрим, что будет дальше». С этой точки зрения все паззлы можно разделить на два больших класса: те, которые решаются итеративным применением построчных алгоритмов (логические) и все остальные.
Так вот первая группа паззлов всегда имеет не более одного решения (то, к которому и можно прийти «логически»). С точки зрения солвера сложных паззлов (второй группы) нет никакого разделения между «правильным» и «подходящим» решениями — они все правильные. Другой вопрос в том, что составитель паззла, скорее всего, имел ввиду одно из решений.
Думаю некорректно будет противопоставлять «логику» и «перебор»: cамый популярный метод решения паззлов второй группы — это бэктрекинг, который представляет собой очень даже логичный перебор. Например, указанный вами пример «Зима» — хоть и второго типа, но имеет единственное правильное решение и оно достигается путем единственного логического предположения: «предположим, что клетка (10, 18) — пустая», которое приводит к противоречию. Закрашиваем (10,18) и дальше все решается так же — просто построчно.
Решение японских кроссвордов с помощью SAT солвера