PySAT: как решать логические задачи с помощью SAT-солверов — гайд с кодом

Автор разбирает SAT (выполнимость булевой формулы) как альтернативу классическому MIP-решению: на комбинаторных задачах SAT-солверы часто обходят традиционные методы. В статье — устройство алгоритмов, обзор солверов в PySAT и пример решения задачи через MaxSAT.

Прикладные сценарии — ручные расписания, подбор совместимых комплектаций, дележ ресурсов. Материал ориентирован на тех, кто занимается математической оптимизацией или ML, и хочет добавить инструмент в арсенал.