Нейросеть без нейросети: как обучить классификатор Iris через SAT и запустить это на GPU
Вступление
В прошлой статье я показывал,как мы в 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. На практике это означает простую вещь:
и 
. А если у вас есть множество точек в этом 3D-пространстве за экраном, и вы начнёте их анимировать и вращать их, а потом воспользуетесь этой формулой для рендеринга всех точек на экране, то это будет выглядеть, как 3D-сцена или 3D-объект. Давайте попробуем эту формулу в деле.
