Когда всё решает «да» или «нет»: 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

Не квантовый компьютер, но уже полезно: обзор AGIQ Solver Enterprise как GPU‑решателя для тяжёлых задач оптимизации

На рынке софта для оптимизации есть две крайности. С одной стороны — академические и промышленные решатели, которые невероятно мощны, но часто требуют либо очень аккуратной постановки, либо серьёзной экспертизы, либо терпения. С другой — бесконечный поток «революционных» продуктов, которые обещают всё, а в реальности оказываются очередной метаэвристикой с красивым лендингом. На этом фоне AGIQ Solver Enterprise оказывается любопытным кейсом. Не потому, что это «магия на видеокарте» или «квантовый компьютер для бедных», а потому что продукт пытается занять вполне конкретную нишу: быстрый поиск хороших решений в сложных булевых и оптимизационных задачах за счёт GPU и квантово-вдохновлённой логики поиска . Ниже — разбор, что это вообще такое, где оно действительно может пригодиться, почему здесь вообще всплывает слово «квантовый», и как с этим работать на практике.

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

#AGIQ_Solver_Enterprise #GPUвычисления #квантововдохновлённые_алгоритмы #оптимизация #MaxSAT #SAT_solver #GPGPU #параллельные_вычисления #булева_оптимизация #комбинаторные_задачи

MOSA-EA introduced by Xiaoyu Qin and myself is an #evolutionaryalgorithm for hard combinatorial optimisation problems. It builds on a decade of theoretical research on non-elitist, self-adaptive, population-based evolutionary algorithms.

It has excellent performance, particularly on random #MAXSAT and #NKlandscape problem instances.

Python and C/C++ source code available here:

https://github.com/ChengCheng-Qin/mosa-ea