Как SAT-солверы решают задачи про разрезания
и почему прямоугольник 5×9 всё-таки режется на уголки
На математических кружках для начинающих часто дают задачи, в которых нужно разрезать клетчатую фигуру на одинаковые маленькие кусочки. Классический пример — L-образный «уголок» из трёх клеток. Формулировка выглядит безобидно: можно ли разрезать данный прямоугольник на такие уголки без наложений и пропусков?
Первое рассуждение почти всегда арифметическое. Каждый уголок состоит из трёх клеток, значит, общее число клеток обязано делиться на 3. Это необходимое условие сразу отсекает множество случаев. Например, прямоугольники вида 3×(2n+1) выглядят подозрительно, а 3×(2n), наоборот, легко режутся. Возникает ощущение, что картина ясна и будто бы число клеток должно делиться ещё и на 6.
Однако эта интуиция быстро ломается. Прямоугольник 5×9 состоит из 45 клеток и тем не менее допускает разрезание на такие уголки. Простой арифметики оказывается недостаточно. Чтобы понять, почему так происходит, приходится либо искать хитрые конструктивные идеи, либо сменить сам способ мышления о задаче.
Вместо того чтобы искать разрезание как геометрический объект, можно попытаться описать задачу в чисто логических терминах. Именно здесь появляется SAT-солвер — инструмент, который на первый взгляд кажется слишком простым для подобных задач, но на практике оказывается удивительно мощным.
SAT-солвер — это программа, предназначенная для решения задачи булевой выполнимости. На вход ей подаётся логическая формула, составленная из булевых переменных и операций «и», «или» и «не». Вопрос, который решает SAT-солвер, формулируется предельно строго: существуют ли такие значения переменных, при которых вся формула становится истинной. Если такие значения существуют, формула выполнима; если нет — невыполнима.
Простейший пример — формула вида «(x или y) и (x или не y)». Она выполнима, потому что при x = истина вся формула становится истинной независимо от значения y. SAT-солвер должен обнаружить этот факт и, как правило, вернуть не только ответ «выполнимо», но и конкретное присваивание переменных.
С теоретической точки зрения SAT занимает центральное место в теории вычислительной сложности. Согласно теореме Кука — Левина, задача булевой выполнимости является NP-полной. Это означает, что в общем случае к ней можно свести любую задачу из класса NP и что не существует алгоритма, который гарантированно решал бы все SAT-задачи за полиномиальное время. В худшем случае сложность остаётся экспоненциальной, и этого принципиально нельзя избежать.
Тем не менее, начиная с конца 1990-х и особенно в 2000-х годах, произошёл резкий скачок в практической эффективности SAT-решателей. Современные алгоритмы научились справляться с формулами, содержащими десятки и сотни тысяч переменных и миллионы ограничений. Это стало возможным благодаря развитию алгоритмов семейства DPLL, анализу конфликтов, обучению на противоречиях и множеству эвристик и оптимизаций. В результате SAT-солверы превратились в мощные инженерные инструменты, широко применяемые в верификации программ и аппаратуры, автоматизации проектирования электронных схем, анализе программ и задачах искусственного интеллекта.
Как всё это связано с задачей про уголки? Связь возникает в тот момент, когда мы меняем постановку задачи. Мы больше не спрашиваем: «как именно разрезать прямоугольник». Вместо этого мы задаём вопрос: «существует ли разрезание вообще».
Для этого мы перечисляем все возможные способы положить уголок внутри прямоугольника. Каждое допустимое положение становится отдельной булевой переменной. Истинность переменной означает, что соответствующий уголок выбран, ложность — что он не используется. После этого геометрия почти полностью исчезает, уступая место логике.
