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