Когда всё решает «да» или «нет»: SAT-солверы и оптимизация в PySAT

В предыдущих работах я много писал про линейное и целочисленное программирование (PuLP, OR-Tools, pyomo), про задачи о назначениях, коммивояжёра, раскрой и генерацию столбцов. Сегодня сделаю шаг в соседнюю, но удивительно мощную область: удовлетворение булевой формулы (SAT). Это тот самый фундамент, на котором стоит вся теория NP-полноты, и одновременно крайне практичный инструмент, который иногда «уделывает» классические MIP-солверы на комбинаторных задачах. Разберём, что такое SAT, какие алгоритмы заставляют современные солверы переваривать миллионы переменных, познакомимся с библиотекой PySAT и доступными через неё солверами, а в финале решим прикладную оптимизационную задачу с помощью MaxSAT. Материал будет полезен специалистам по математической оптимизации и ML-инженерам, которым нужен ещё один инструмент в портфеле. А управленцы и владельцы процессов, возможно, узнают в примерах свою боль: ручное составление расписаний, конфигурирование заказов, распределение ограниченного ресурса - всё это аккуратно ложится на SAT и считается за секунды.

https://habr.com/ru/articles/1048634/

#sat #PySAT #математическое_моделирование #раскраска_графов #оптимизация_процессов #составление_расписаний #бизнесоптимизация #математическое_программирование #Boolean_satisfiability #MaxSAT