Hacker News Digest

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

На примере Судоку автор демонстрирует, как преобразовать правила игры в систему булевых ограничений. Для каждой клетки (i,j) и цифры k вводится переменная x_{i,j,k}, где true означает, что клетка содержит цифру k. Правила игры переводятся в ограничения: каждая клетка должна содержать ровно одну цифку (x_{i,j,1} ∨ x_{i,j,2} ∨ ... ∨ x_{i,j,9} и ¬x_{i,j,k} ∨ ¬x_{i,j,l} для k≠l), каждая цифра должна встречаться ровно один раз в строке, столбце и под-сетке. SAT-солвер находит удовлетворяющее всем этим ограничениям присвоение значений переменным, решая головоломку.

• SAT и MILP-солверы недооценены: первые хорошо знакомы инженерам, вторые — нет, хотя MILP позволяет естественно выразить оптимизацию и ограничения.
• Исторически открытые MILP-солверы отставали от коммерческих, что сдерживало их использование.
• SAT-солверы и MILP-солверы дополняют друг друга: SAT хорошо для задач «есть/нет», MILP — для задач оптимизации.
• Практически любую задачу можно выразить как MILP, и SAT-солверы могут быть использованы для решения MILP.

Сложные LeetCode-задачи — простые задачи на ограничения

Интервьюер спросил: «Минимальное количество монет для сдачи 37¢ при номиналах [10, 9, 1]».
Жадный алгоритм даёт 10 монет, оптимум — 4. Ручное ДП сложно, а в MiniZinc — три строки:

int: total; array[int] of int: values = [10,9,1];
array[index_set(values)] of var 0..: coins;
constraint sum(c in index_set(coins)) (coins[c]*values[c]) == total;
solve minimize sum(coins);

Запускаем онлайн, получаем ответы за секунды.

---

Другие «сложные» задачи

1. Максимальная прибыль на акциях
   Дано: цены за день.
   Решение: купить до продать, максимизировать prices[sell]-prices[buy].

   array[int] of int: prices;
   var int: buy; var int: sell;
   constraint sell > buy;
   solve maximize prices[sell]-prices[buy];
   

2. Три числа дают 0 в сумме
   Нужно ли среди списка выбрать 3 числа со знаками ±1, чтобы сумма была 0?

   array[int] of int: nums;
   array[index_set(nums)] of var {-1,0,1}: coef;
   constraint sum(i in index_set(nums)) (nums[i]*coef[i]) = 0;
   constraint sum(i in index_set(nums)) (abs(coef[i])) = 3;
   solve satisfy;
   

3. Самый большой прямоугольник в гистограмме
   Ширина столбцов = 1, высоты заданы.

   array[int] of int: h;
   var 1..length(h): x; var 1..length(h): dx; var 1..max(h): y;
   constraint x+dx <= length(h);
   constraint forall(i in x..x+dx) (y <= h[i]);
   solve maximize (dx+1)*y;
   

---

Плюсы и минусы солверов

• + Код в 3–5 строк, добавление новых ограничений бесплатно.
• – Сложность работы непредсказуема, медленнее «идеального» алгоритма.
• – На собеседовании спросят «а сложность?» — ответа нет.

Вывод: если нужен рабочий код быстро — бери солвер; если нужна гарантированная скорость — пиши алгоритм вручную.

• Кто-то предлагает решать «задачи на подбор монет» и прочие LeetCode-загадки не вручную, а вызывать готовый constraint-/SAT-/SMT-солвер — быстро и универсально.
• Интервьюеры возражают: «мы хотим увидеть, как ты сам пишешь алгоритм, а не вызываешь библиотеку; иначе как проверить сложность и масштабируемость?»
• Сторонники солверов отвечают: в продакшене важен рабочий результат, а не «олимпиадная остроумность»; к тому же солвер легко добавляет новые ограничения.
• Часть комментаторов считает, что LC-интервью вообще плохо предсказывают рабочие навыки и дискриминируют тех, кто не зубрит шаблоны.
• Итог: constraint-solvers — мощный инструмент, но на типовом собеседовании их использование чаще всего «вне правил», поэтому приходится писать ручное решение, даже если в реальной жизни ты бы просто вызвал OR-Tools.