Остаются два принципиальных условия

Остаются два принципиальных условия. Каждая клетка прямоугольника должна быть покрыта хотя бы одним выбранным уголком. И ни одна клетка не должна быть покрыта дважды, то есть нельзя одновременно выбрать два уголка, которые перекрываются. Оба условия естественным образом записываются в виде булевых формул в конъюнктивной нормальной форме — именно в том виде, с которым SAT-солверы умеют работать особенно эффективно.

После этого задача полностью готова. Мы передаём SAT-солверу набор логических ограничений и задаём единственный вопрос: существует ли присваивание переменных, при котором все они выполняются. Если ответ положительный, найденное присваивание буквально и есть корректное разрезание прямоугольника. Если отрицательный — никакого разрезания не существует в принципе, и это уже не эвристическое рассуждение, а строгий логический вывод.

Именно поэтому пример с прямоугольником 5×9 так показателен. Для него не существует простого инварианта, который «на глаз» запрещал бы разрезание. Но SAT-солвер спокойно перебирает логическое пространство возможностей и находит допустимую конфигурацию. А если бы её не существовало, он столь же уверенно доказал бы невозможность.

Самое удивительное в этом подходе — его универсальность. Мы не писали специальный алгоритм для разрезания уголками, не анализировали симметрии и не придумывали конструктивные трюки. Мы просто свели задачу к вопросу о логической выполнимости. Точно так же SAT-солверы применяются к судоку, расписаниям экзаменов, задачам упаковки, верификации программ и тысячам других задач, которые внешне выглядят совершенно по-разному.