SAT-солверы из PySAT: как «да» или «нет» решают комбинаторные задачи быстрее MIP

Автор, ранее писавший о линейном и целочисленном программировании (PuLP, OR-Tools, pyomo), теперь погружается в SAT — область, на которой строится теория NP-полноты. SAT-солверы, по его опыту, иногда «уделывают» классические MIP-решатели на комбинаторных задачах.

В статье разбирается, что такое SAT, какие алгоритмы позволяют солверам обрабатывать миллионы переменных, и как библиотека PySAT даёт доступ к десяткам современных решателей. В конце рассматривается прикладная оптимизационная задача через MaxSAT.

Материал нацелен на специалистов по математической оптимизации, ML-инженеров, а также на управленцев, которые сталкиваются с ручным составлением расписаний, конфигурированием заказов и распределением ресурсов — всё это, как обещает автор, «ложится на SAT и считается за секунды».