ВступлениеВ прошлой статье я показывал,как мы в AGIQ Solver Enterprise применили квантово‑вдохновлённый популяционный подход на GPU для NP‑задач и получили ускорение на практических постановках в 50–100 раз по сравнению с последовательным перебором и плохо распараллеливаемыми схемами.Сегодня — следующий шаг:покажу,как задачи машинного обучения можно кодировать в SAT/MaxSAT, а затем решать обычным NP‑солвером — тем же AGIQ Solver Enterprise.О чём статья (и что мы НЕ делаем)Мы не будем пытаться “запихнуть” в SAT весь мир DL (ResNet/LLM/градиенты/батчи). Это плохая идея: там, где нужна дифференцируемая оптимизация, SGD остаётся королём.Зато есть большой класс ML‑задач, где: модель дискретная или может быть дискретизирована, важны ограничения (fairness/монотонность/запреты/политики), важна проверяемость и воспроизводимость решения, нужен глобальный поиск (а не локальная оптимизация по градиенту).Вот здесь SAT/MaxSAT — это не экзотика,а универсальный язык “правила + ограничения + оптимизация”.Почему SAT вообще способен “кодировать что угодно”В теории, любой NP‑вопрос можно редуцировать к SAT. На практике это означает простую вещь: Читать далее