Лениво просматриваю выложенный недавно коллегами из «Сириуса» список курсов, проведенных у школьников… Так, а это что такое? «Поиск комбинаторных объектов с помощью SAT-солверов»? «Мы сделали решатель судоку, японских кроссвордов и прочего»?

В памяти всплывает мысль о том, что переборные NP-задачи сводимы одна к другой, и в частности, сводимы к поиску выполнимости булевой формулы. Эту мысль один из авторов Хабра высказывал здесь, и честно говоря, для меня она подобна магии.

Конечно, как человек, прошедший курс дискретной математики и сложности алгоритмов теоретически я знаю, что задачи сводимы одна к другой. Но обычно заниматься этим сложно, и лучше я поверю на слово профессорам и другим умным людям.

Но тут же это предлагается… ШКОЛЬНИКАМ! Внутри зашевелилось шило в п... творческое начало и заявило: «Ну это, наверное, несложно прикрутить, раз ученикам предлагают. Неужели я не разберусь?? Вон, обещают, что питоновскую библиотеку используют, а питон я в целом знаю...»

А времени было около 9 вечера, что несколько притупило мой критический взгляд на сложность проблемы… (собственно, далее хроники 4-часового программирования)

21:02 Первый этап квеста — пытаюсь установить библиотеку в Питон. По опыту работы с нейронными сетями уже знаю, что, собственно код иногда занимает меньше времени, чем конфигурирование пакетов.

С помощью классического pip install pycosat не устанавливается, выдает ошибку в духе Microsoft Visual C++ 14.0 is required.

Лезем искать источник проблемы, попадаем на Stackoverflow, где находим маленькую ссылку на требуемый Visual C++ 2015 Build Tools, видимо, включающее компилятор C++.

Скачиваем, пытаемся установить… ого, требует 4 Гб! Мне вообще-то только компилятор нужен, ну да ладно.

Пока сия штука скачивается и устанавливается, ходим по выложенным с «Сириуса» ссылкам в программе… Да, не густо — примеры Питон проектов, да список возможных заданий по курсу. Ни презентации, ни видео, чтобы по-быстрому понять, как работать с библиотекой.

Ладно, начнем с разбора примеров. Заходим в queens_pycosat.py… Ого, да это по ходу решение знакомой мне задачи о расстановки ферзей на шахматной доске (задача — расставить 8 ферзей так, чтобы они не били друг друга).

21:10-21:30 Разбираемся и пытаемся запустить.

Общая логика начинает прослеживаться:

SAT-солвер получает условия в формате П (Переменная) (П1, П2, П3),(-П1, П2 и т.д.), где каждая переменная булева (True/False).

Соответственно, в задаче надо спроектировать набор переменных так, чтобы покрыть все её условия.

В данном случае в качестве переменной будет занятость клетки доски ферзем (или ладьей, я упростил задачу); всего, соответственно, 8x8 = 64 булевых переменных, отражающих занятость каждой клетки поля.

Первое условие будет выглядеть как (П1 или П2 или П3… или П8) — одно из полей на 1 горизонтали должно быть занято. Записывается целыми числами в виде массива — [1,2,3...8]
Повторяем для всех горизонталей — (П9… П16) и т.д.

Теперь условие — на одной горизонтали должно стоять НЕ больше 1 ладьи!
Делаем это через записи пар [не П1 или не П2] (если на одном стоит — на другом стоять не должно). Записывается целыми числами в виде отрицания [-1,-2],[-1,-3] и так далее.

То же самое для вертикалей и, в случае ферзей, для диагоналей. Естественно, всё это генерируется автоматически.

В результате получается формула в формате так называемом КНФ (конъюнктивная нормальная форма) — (П1 или П2… П8) И (не П1 или не П2) И (...). Внутри элементов стоят условия ИЛИ, снаружи — И.

Да, я не сразу такой умный был, это сейчас, когда уже разобрался…

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

Запускаем, получаем:

| | | | | | | |x|
| | | | | | |x| |
| | | | | |x| | |
| | | | |x| | | |
| | | |x| | | | |
| | |x| | | | | |
| |x| | | | | | |
|x| | | | | | | |

Работает!

21:35 Немного ознакомившись с документацией по библиотеке узнаем, что есть вызовы для поиска одного решения или всех решений.

А скажи-ка нам друг любезный, сколько есть расстановок ладей на доске 8x8? Найдешь ли все?

Машина задумалась, а я начал гуглить таблицу факториалов.
Спустя минуту солвер ответил — «найдено 40320 решений». Проверяем — действительно 8!, всё верно.

Убрал условие на то, что ладьи не бьют друг друга по вертикали… а сколько теперь будет? Должно быть 8^8=16777216. Тут до меня дошло, что считать он будет долго — прерываем процесс.

Также нашел быстрый способ вывести 4 решения, не вычисляя все — из всё той же самой библиотеки. Делается так — находим решение, после чего добавляем его в исключения булевой формулы…


В общем, получаем еще несколько решений «ладейной задачи»:

| | | | | | | |x|
| | | | | | |x| |
| | | | | |x| | |
| | | | |x| | | |
| | | |x| | | | |
| |x| | | | | | |
| | |x| | | | | |
|x| | | | | | | |

21:45
Я: В целом всё понятно, если что, теперь смогу прикрутить. Пойду, почитаю книжку, и спа-ать…

ТВОРЧЕСКОЕ НАЧАЛО: Ну, ты же понял, как всё работает. А давай напишем простенькую решалку японских кроссвордов! Возьмем самый простой случай — на каждом строке и столбце будет не больше одной цифры (и, соответственно, одного блока). Ты просто сгенерируешь перебором возможные варианты по строке/столбцу, это здесь быстро, а затем загрузишь его в солвер. Давай сделаем, а?

Я: (не чувствуя засады) Ну, давай… вроде правда недолго…

Для простоты возьмем только квадратные кроссворды NxN — заодно и код вывода результата можно взять готовый, и думать, где горизонтали и вертикали не нужно…

22:10 Оно не работает :((
Пробуем для кроссворда 3x3, в формате 1-0-1 (пока только блоки по горизонтали, вертикаль не учитываем). Оно выдает все пустые клетки, зараза, даже не учитывает заполненные блоки…

Ладно, детально вникаем в формат передачи данных в солвер. И тут обнаруживается нечто, мягко говоря, непредвиденное…

Итак, как я решаю «по-быстрому» сделать решатель кроссворда?

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

Для условия [1] при 3 клетках в строке получаются условия, соответствующие элементам:
[X__],[_X_],[__X]
или, в формате солвера,
[1,-2,-3],[-1,2,-3],[-1,-2,3]

А теперь смотрим внимательно, раскрывая в виде логической формулы…
Это условия:
[1 и -2 и -3] ИЛИ [-1, 2...] ИЛИ [...]

Внутри И, снаружи ИЛИ. А в КНФ должно быть внутри ИЛИ, снаружи И. Это другая форма булевой функции — ДНФ, дизъюнктивная нормальная форма!

Засада. Собственно, варианта два — либо придумать условия для кроссворда в КНФ, либо придумать, как сконвертировать ДНФ в КНФ (ну кто-то же должен был об этом подумать, тем более что обе — булевские формулы!)

22:50 Закончил перекус. Как сделать условия для КНФ не придумал (уже позднее нашел, что в статье они описаны, но программировать их долго, да и, честно говоря, неспортивно).

Так что ищем конвертатор ДНФ в КНФ. По интернету разбросаны формальные описания преобразований в академическом стиле… зачем они мне? Втыкать в них сейчас я точно не собираюсь, мне бы задачку решить. Так, видим единственную(!) библиотеку на Питоне вроде с подходящим названием и функциями. Сейчас будем подключать…

23:10 Она работает забавно — делает дополнительные переменные, и через них приводит ДНФ в КНФ. По-видимому, честно сделать КНФ достаточно сложно…

Так, и она тоже не работает! В чем дело?

Подаем тестовый вход ДНФ: lstall = [[1,2,3]]. Т.е, мы ожидаем, что валидным решением будет только [1,2,3] (соответствует полностью заполненной строке [XXX])

Библиотека выдает КНФ: cnf = [[-1, -2, -3, 4], [1, -4], [2, -4], [3, -4]]
Непонятно, но очень интересно. Ну, допустим, я тебе поверю…

Просим pycosat найти все решения для cnf:
[1, 2, 3, 4]
[1, 2, -3, -4]
[1, -2, -3, -4]
[1, -2, 3, -4]
[-1, -2, -3, -4]
[-1, -2, 3, -4]
[-1, 2, -3, -4]
[-1, 2, 3, -4]

Вместо ожидаемого одного их восемь! Что делать?

Внимательно смотрим и понимаем, что корректное решение возникает только тогда, когда сгенерированная переменная 4 принимает значение True. Добавим это как условие в процедуру генерации КНФ библиотекой?

Сгенерированная КНФ в поправленной библиотеке: cnf2 = [[-1, -2, -3, 4], [1, -4], [2, -4], [3, -4], [4]]
Просим pycosat найти все решения для cnf2:
Всего решений 1: [1, 2, 3, 4]

Ура, то, что нужно! Четвертую техническую переменную мы, очевидно, отбросим при выводе.
Проверяем на других тестах — тоже работает!

23:10 Она решает! Вот кроссворд 1-3-1 по вертикали и горизонтали:

| |x| |
|x|x|x|
| |x| |

Вот двойное решение кроссворда 1-0-1 по вертикали и горизонтали:

1
| | |x|
| | | |
|x| | |
2
|x| | |
| | | |
| | |x|

Я: Так, у меня всё работает, я молодец. Ого, уже 11 вечера. Спа-ать…

ТВОРЧЕСКОЕ НАЧАЛО: Ты понимаешь, что тебе до решения любых японских кроссвордов осталось совсем чуть-чуть? Надо только написать одну рекурсивную процедуру, которая будет выдавать все варианты строки не для одного блока, а для N…

Я: Ну… вроде должно быть несложно, да…

00:00 В полночь голова тупит уже варит не так хорошо, но я продолжаю отлаживать рекурсию.

Условия японского кроссворда — между блоками должен быть хотя бы один пробел, но может быть и не один.

Так что при условии [1,2,1] на 6 клеток программа должна генерировать единственный вариант
[X_XX_X],
а на 7 клеток уже 4 варианта:
[X_XX_X_],
[X_XX__X],
[X__XX_X],
[_X_XX_X],

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

00:30 Неужели работает?

3x3
rows = [[1,1],[0],[1,1]]
cols = [[1,1],[0],[1,1]]

Единственный ответ:
|X| |X|
| | | |
|X| |X|

4x4
rows = [[1,1],[0],[0],[1,1]]
cols = [[1],[1],[1],[1]]

Два решения:
1
| |X| |X|
| | | | |
| | | | |
|X| |X| |
2
|X| |X| |
| | | | |
| | | | |
| |X| |X|

На чем бы еще проверить?

Так, где бы взять машиноориентированное описание кроссвордов… На этом сайте нет, на этом — нет… Ладно, черт с ним, ручками перебью.

00:50 Оно и правда работает О_О
Вот краб с jcrosswords.ru/crossword/65, решенный моим солвером. Максимальный протестированный размер — 10x10, сейчас мне очень лениво перебивать бОльшие кроссворды в программу…

|x|_|x|_|_|_|_|x|_|x|
|x|x|x|_|_|_|_|x|x|x|
|_|x|_|_|_|_|_|_|x|_|
|_|x|_|x|_|_|x|_|x|_|
|_|x|x|x|x|x|x|x|x|_|
|_|_|x|x|x|x|x|x|_|_|
|x|x|x|x|x|x|x|x|x|x|
|_|_|x|x|x|x|x|x|_|_|
|x|x|_|x|x|x|x|_|x|x|
|x|_|_|_|_|_|_|_|_|x|

— Я: Ого, уже час ночи! Подождите, прошло всего 4 часа от момента, когда я ничего не знал о SAT-солвере? Так, а как это было вообще?

(по-быстрому пишутся короткие заметки о произошедшем...)

---

Послесловие.

Утро. На Хабре найдена статья про решатель на Rust. Загрузка с сайтов кроссвордов не работает, но пройдя на указанный в статье Github мы находим на сайте кроссвордов Webpbn спрятанную ссылку на экспорт кроссвордов в машиночитаемом формате. Нам подойдет вариант «Format for version 1 of Kyle Keen's Python solver», он такой же, как у нас.

Когда не надо перебивать кроссворды ручками, дело идет быстрее. Быстро выясняется, что максимум, что солвер способен решать — кроссворды в районе 30x30. Основная проблема — та самая генерация вариантов отдельных строк, в случае кучи блоков этих условий ОЧЕНЬ много и всё начинает тормозить:

1. Во-первых, долго генерятся варианты строк. Генерация только всех вариантов для строки [2,1,3,1,4] длины 60 занимает уже около полминуты… (их всего 2118760, если кому интересно)
2. Также конвертация ДНФ->КНФ порождает слишком много условий и доп переменных…

Но если блоков немного, то даже большие кроссворды решаются за осмысленное время.


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


В оригинальной публикации по SAT-солверу более честно генерируются условия и переменные — поэтому там решение быстрее и, вероятно, занимает меньше памяти. У меня при решении лошади уходит около 2.7Гб оперативки, а некоторые сложные штуки занимают до всех установленных 12, после чего начинают бешено свопить на диск…

Еще из выводов:

1. До меня дошло, почему большинство быстро загугленных примеров по pycosat — решения судоку. Правила судоку гораздо проще кладутся на солвер, потому что не надо описывать сложные взаимоотношения между блоками и клетками, в основом только условия «каждая цифра — в каждой строке» и «только одна цифра в одной строке».
Но судоку я люблю гораздо меньше, так что о выбранном решении не жалею.

2. Мне понравилось, как можно смешивать ДНФ и КНФ. Не хочешь писать правильные условия — не надо, сгенерируй только все варианты. Конечно, это не оптимально, но работает.

Конечно рекордов по скорости решения кроссвордов я не поставил, но время провел неплохо. Самое главное — I can do it! :) Чего и вам желаю!