Вступление
В прошлой статье я показывал,как мы в 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. На практике это означает простую вещь:

Вы выбираете булевы переменные (что именно мы решаем?).
Вы пишете ограничения (что запрещено? что обязательно?).
Если есть “качество” (accuracy,loss, стоимость) — вы переводите его в MaxSAT/Weighted MaxSAT: “за нарушение — штраф; за соблюдение — награда”.

И дальше солвер ищет такое присваивание переменных, которое:
удовлетворяет жёстким ограничениям (hard),
и максимально выполняет мягкие (soft) — то есть оптимизирует вашу цель.

Демонстрация:Iris → SAT‑обучение порогового классификатора
Датасет Iris — классика (150 объектов,3 класса). Важно,что для Iris хорошо работает простая интерпретируемая модель на двух признаках лепестка:

Правило (структура модели фиксирована):
если petal_length < T1 → setosa
иначе если petal_width < T2 → versicolor
иначе → virginica

Это похоже на маленькое дерево решений глубины 2.
Мы НЕ задаём “правильные T1/T2”,мы только задаём:
набор возможных кандидатов T1 и T2 (дискретизация),
и просим солвер выбрать пару, которая минимизирует число ошибок.

Как это кодируется в MaxSAT/Max‑3SAT
Мы вводим булевы переменные:
selT1[i]:выбран ли i‑й кандидат порога T1
selT2[j]:выбран ли j‑й кандидат порога T2

Добавляем “ровно один выбран” (exactly-one) для каждого порога.

Дальше ключевой момент:мы превращаем ошибку классификации в штраф.
Для каждого объекта и каждой пары (i,j):
если модель с (T1[i],T2[j]) ошибается на этом объекте,мы добавляем soft‑клаузы вида:
¬selT1[i] ∨ ¬selT2[j] ∨ D
где D — фиктивная переменная,жёстко зафиксированная в false,чтобы держать формально 3‑литерные клаузы.

Итог: солвер точно минимизирует число ошибок (в выбранной дискретизации порогов), а не “оптимизирует абстрактные условия”.

Результат на полной Iris (150/150)
В нашем прогоне solвер выбрал:
T1(petal_length) = 2.6333
T2(petal_width) = 1.7500

И получил:
Accuracy:144/150 = 96%
Ошибки — в основном на границе versicolor vs virginica (что ожидаемо и для классических моделей).

Как воспроизвести (2 шага)

Генерируем CNF + map (кодировщик).
Решаем CNF в AGIQ Solver Enterprise и берём best assignment.
Декодируем assignment → получаем T1, T2 → считаем accuracy (декодер).

Кодировщик:Iris → CNF

#nullable enable
using System;
using System.Collections.Generic;
using System.Globalization;
using System.IO;
using System.Linq;
using System.Text;
using System.Text.Json;

static class Program
{
    // ======== НАСТРОЙКИ (ПРАВИТЬ ТОЛЬКО ТУТ) ========
    private const string IrisCsvPath = "iris.csv"; // CSV (150 строк)
    private const string OutCnfPath = "iris_thr.cnf"; // CNF для AGIQ
    private const string OutMapPath = "iris_thr.map.json"; // JSON для декодера

    // Кол-во кандидатов порогов для каждого из двух разрезов
    private const int K1 = 8; // для petal_length
    private const int K2 = 8; // для petal_width

    // Веса
    private const int DummyHard = 20000; // фиксируем D=false
    private const int HardWeight = 1500; // "почти hard" exactly-one на селекторах
    private const int WErr = 5; // штраф за ошибку (повтор penalty-клаузы)

    // Якорные пороги (почти оптимальные для Iris)
    private const double AnchorPetalLength = 2.45;
    private const double AnchorPetalWidth = 1.75;

    public static int Main()
    {
        CultureInfo.DefaultThreadCurrentCulture = CultureInfo.InvariantCulture;

        if (!File.Exists(IrisCsvPath))
        {
            Console.WriteLine($"ERROR:{IrisCsvPath} not found. Put iris.csv рядом с exe.");
            return 2;
        }

        var data = LoadIrisCsv(IrisCsvPath);
        if (data.Count < 150) Console.WriteLine($"Warning:rows={data.Count} (expected 150)");

        // 1) Собираем кандидаты порогов
        var t1 = BuildThresholdCandidates(data.Select(r => r.X[2]).ToArray(), K1, AnchorPetalLength); // petal_length
        var t2 = BuildThresholdCandidates(data.Select(r => r.X[3]).ToArray(), K2, AnchorPetalWidth); // petal_width

        // 2) Переменные:
        // selT1[0..K1-1] => DIMACS 1..K1
        // selT2[0..K2-1] => DIMACS (K1+1)..(K1+K2)
        // aux for at-least-one ladder:(K1-3) + (K2-3)
        // D last
        int selT1Start = 1;
        int selT2Start = selT1Start + K1;

        int auxT1Start = selT2Start + K2;
        int auxT1Count = K1 - 3;

        int auxT2Start = auxT1Start + auxT1Count;
        int auxT2Count = K2 - 3;

        int D = auxT2Start + auxT2Count; // last var
        int vars = D;

        if (vars > 64)
        {
            Console.WriteLine($"ERROR:vars={vars} > 64. Reduce K1/K2.");
            return 3;
        }

        var clauses = new List<string>(capacity: 200_000);

        // 3) Жёстко фиксируем D=false
        for (int r = 0; r < DummyHard; r++)
            clauses.Add($"{-D} {-D} {-D} 0");

        // 4) Exactly-one для T1 и T2 (повторяем HardWeight раз)
        for (int rep = 0; rep < HardWeight; rep++)
        {
            AddExactlyOneLadder3Cnf(clauses, Enumerable.Range(selT1Start, K1).ToArray(), auxT1Start, D);
            AddExactlyOneLadder3Cnf(clauses, Enumerable.Range(selT2Start, K2).ToArray(), auxT2Start, D);
        }

        // 5) Soft penalty за ошибки классификации
        // Модель:if PL < T1 => 0; else if PW < T2 => 1; else 2
        // Для каждого примера и каждой пары (t1_i,t2_j),которая ошибочна,добавляем:
        // (¬selT1_i ∨ ¬selT2_j ∨ D) повторённо WErr раз.
        int penaltyClauses = 0;
        for (int i = 0; i < data.Count; i++)
        {
            int y = data[i].Label;
            double pl = data[i].X[2];
            double pw = data[i].X[3];

            for (int a = 0; a < K1; a++)
            {
                for (int b = 0; b < K2; b++)
                {
                    int pred = Predict(pl, pw, t1[a], t2[b]);
                    if (pred == y) continue;

                    int vA = selT1Start + a;
                    int vB = selT2Start + b;

                    // penalty if (vA=true AND vB=true)
                    for (int w = 0; w < WErr; w++)
                    {
                        clauses.Add($"{-vA} {-vB} {D} 0");
                        penaltyClauses++;
                    }
                }
            }
        }

        // 6) Пишем DIMACS CNF
        using (var w = new StreamWriter(OutCnfPath, false, new UTF8Encoding(false), 1 << 20))
        {
            w.WriteLine("c AGIQ Iris(150) threshold classifier -> Max-3SAT strict 3-CNF");
            w.WriteLine("c model:if petal_length < T1 => setosa; else if petal_width < T2 => versicolor; else virginica");
            w.WriteLine($"c K1={K1} K2={K2} vars={vars} clauses={clauses.Count}");
            w.WriteLine($"c weights:DummyHard={DummyHard} HardWeight={HardWeight} WErr={WErr} penaltyClauses={penaltyClauses}");
            w.WriteLine($"p cnf {vars} {clauses.Count}");
            foreach (var cl in clauses) w.WriteLine(cl);
        }

        // 7) Пишем mapping JSON для декодера
        var map = new MapFile
        {
            IrisCsv = Path.GetFullPath(IrisCsvPath),
            K1 = K1,
            K2 = K2,
            T1 = t1,
            T2 = t2,
            SelT1Start = selT1Start,
            SelT2Start = selT2Start,
            D = D,
            Model = "if PL < T1 => 0; else if PW < T2 => 1; else => 2"
        };

        File.WriteAllText(OutMapPath, JsonSerializer.Serialize(map, new JsonSerializerOptions { WriteIndented = true }), Encoding.UTF8);

        Console.WriteLine($"Wrote:{OutCnfPath}");
        Console.WriteLine($"Wrote:{OutMapPath}");
        Console.WriteLine($"vars={vars},clauses={clauses.Count:n0}");
        Console.WriteLine($"T1 candidates:{string.Join(",", t1.Select(x => x.ToString("F2", CultureInfo.InvariantCulture)))}");
        Console.WriteLine($"T2 candidates:{string.Join(",", t2.Select(x => x.ToString("F2", CultureInfo.InvariantCulture)))}");
        return 0;
    }

    private static int Predict(double petalLength, double petalWidth, double t1, double t2)
    {
        if (petalLength < t1) return 0;
        if (petalWidth < t2) return 1;
        return 2;
    }

    // Exactly-one for vars v[0..n-1] (n>=3) as strict 3-CNF:
    // at least one via ladder (n-3 aux):
    // (v1 ∨ v2 ∨ y1)
    // (¬y1 ∨ v3 ∨ y2)
    // ...
    // (¬y_{n-3} ∨ v_{n-1} ∨ v_n)
    // at most one pairwise padded with D:
    // (¬vi ∨ ¬vj ∨ D)
    private static void AddExactlyOneLadder3Cnf(List<string> cls, int[] v, int auxStart, int D)
    {
        int n = v.Length;
        if (n < 3) throw new InvalidOperationException("Need n>=3");

        // at least one
        if (n == 3)
        {
            cls.Add($"{v[0]} {v[1]} {v[2]} 0");
        }
        else
        {
            int auxCount = n - 3;
            // first
            cls.Add($"{v[0]} {v[1]} {auxStart} 0");
            // middle
            for (int i = 0; i < auxCount - 1; i++)
            {
                int yi = auxStart + i;
                int yi1 = auxStart + i + 1;
                int vi = v[i + 2];
                cls.Add($"{-yi} {vi} {yi1} 0");
            }
            // last
            int yLast = auxStart + auxCount - 1;
            cls.Add($"{-yLast} {v[n - 2]} {v[n - 1]} 0");
        }

        // at most one
        for (int i = 0; i < n; i++)
            for (int j = i + 1; j < n; j++)
                cls.Add($"{-v[i]} {-v[j]} {D} 0");
    }

    private sealed record IrisRow(double[] X, int Label);

    private static List<IrisRow> LoadIrisCsv(string path)
    {
        var list = new List<IrisRow>(160);
        foreach (var line in File.ReadLines(path))
        {
            if (string.IsNullOrWhiteSpace(line)) continue;
            if (line.StartsWith("sepal", StringComparison.OrdinalIgnoreCase)) continue;

            var p = line.Split(',', StringSplitOptions.RemoveEmptyEntries | StringSplitOptions.TrimEntries);
            if (p.Length < 5) continue;

            double f0 = double.Parse(p[0], CultureInfo.InvariantCulture);
            double f1 = double.Parse(p[1], CultureInfo.InvariantCulture);
            double f2 = double.Parse(p[2], CultureInfo.InvariantCulture);
            double f3 = double.Parse(p[3], CultureInfo.InvariantCulture);

            int label = p[4] switch
            {
                "setosa" or "Iris-setosa" => 0,
                "versicolor" or "Iris-versicolor" => 1,
                "virginica" or "Iris-virginica" => 2,
                _ => throw new InvalidOperationException("Unknown label:" + p[4])
            };

            list.Add(new IrisRow(new[] { f0, f1, f2, f3 }, label));
        }
        return list;
    }

    private static double[] BuildThresholdCandidates(double[] values, int k, double anchor)
    {
        // k candidates:quantiles + обязательно anchor (если в диапазоне)
        var arr = (double[])values.Clone();
        Array.Sort(arr);

        var cand = new SortedSet<double>();

        // quantiles
        for (int i = 1; i <= k; i++)
        {
            double q = i / (double)(k + 1); // exclude extremes
            double pos = q * (arr.Length - 1);
            int a = (int)Math.Floor(pos);
            int b = Math.Min(a + 1, arr.Length - 1);
            double t = pos - a;
            double v = arr[a]*(1 - t) + arr[b] * t;
            cand.Add(Math.Round(v, 4));
        }

        // anchor
        if (anchor >= arr[0] && anchor <= arr[^1])
            cand.Add(Math.Round(anchor, 4));

        // reduce/enlarge to exactly k by taking evenly spread items
        var all = cand.ToArray();

        if (all.Length == k) return all;

        if (all.Length > k)
        {
            // pick k evenly from sorted
            var res = new double[k];
            for (int i = 0; i < k; i++)
            {
                int idx = (int)Math.Round(i * (all.Length - 1) / (double)(k - 1));
                res[i] = all[idx];
            }
            return res;
        }
        else
        {
            // if not enough,add neighbors from array
            var res = new List<double>(all);
            int step = Math.Max(1, arr.Length / 20);
            for (int i = 0; res.Count < k && i < arr.Length; i += step)
                res.Add(Math.Round(arr[i], 4));
            res.Sort();
            // trim to k
            while (res.Count > k) res.RemoveAt(res.Count - 1);
            return res.ToArray();
        }
    }

    private sealed class MapFile
    {
        public string IrisCsv { get; set; } = "";
        public int K1 { get; set; }
        public int K2 { get; set; }
        public double[] T1 { get; set; } = Array.Empty<double>();
        public double[] T2 { get; set; } = Array.Empty<double>();
        public int SelT1Start { get; set; }
        public int SelT2Start { get; set; }
        public int D { get; set; }
        public string Model { get; set; } = "";
    }
}

Декодер: CNF solution → thresholds → accuracy

#nullable enable
using System;
using System.Collections.Generic;
using System.Globalization;
using System.IO;
using System.Linq;
using System.Text.Json;

static class Program
{
    // ======== НАСТРОЙКИ ========
    private const string MapPath = "iris_thr.map.json";
    private const string IrisCsvPathOverride = "iris.csv";
    private const string AssignmentHex = "0x6BCBAE0838E12008"; // ВСТАВЬТЕ СЮДА ВАШЕ РЕШЕНИЕ ИЗ AGIQ

    public static int Main()
    {
        CultureInfo.DefaultThreadCurrentCulture = CultureInfo.InvariantCulture;

        if (!File.Exists(MapPath))
        {
            Console.WriteLine($"ERROR:{MapPath} not found.");
            return 2;
        }

        var map = JsonSerializer.Deserialize<MapFile>(File.ReadAllText(MapPath))
        ?? throw new InvalidOperationException("Bad map json");

        string irisPath = File.Exists(IrisCsvPathOverride) ? IrisCsvPathOverride : map.IrisCsv;
        if (!File.Exists(irisPath))
        {
            Console.WriteLine($"ERROR:iris.csv not found:{irisPath}");
            return 3;
        }

        ulong assign = ParseHexU64(AssignmentHex);

        var data = LoadIrisCsv(irisPath);

        int idxT1 = DecodeSelectedIndex(assign, map.SelT1Start, map.K1);
        int idxT2 = DecodeSelectedIndex(assign, map.SelT2Start, map.K2);

        double T1 = map.T1[idxT1];
        double T2 = map.T2[idxT2];

        Console.WriteLine($"Selected T1(petal_length) = {T1:F4} (index {idxT1})");
        Console.WriteLine($"Selected T2(petal_width) = {T2:F4} (index {idxT2})");
        Console.WriteLine($"Model:{map.Model}");
        Console.WriteLine();

        int correct = 0;
        int[,] cm = new int[3, 3];

        for (int i = 0; i < data.Count; i++)
        {
            int pred = Predict(data[i].X[2], data[i].X[3], T1, T2);
            cm[data[i].Label, pred]++;
            if (pred == data[i].Label) correct++;
        }

        double acc = 100.0 * correct / data.Count;

        Console.WriteLine($"Accuracy:{correct}/{data.Count} = {acc:F2}%");
        Console.WriteLine("Confusion matrix (rows=true,cols=pred):");
        for (int r = 0; r < 3; r++)
            Console.WriteLine($"{cm[r, 0],4} {cm[r, 1],4} {cm[r, 2],4}");

        return 0;
    }

    private static int Predict(double petalLength, double petalWidth, double t1, double t2)
    {
        if (petalLength < t1) return 0;
        if (petalWidth < t2) return 1;
        return 2;
    }

    private static int DecodeSelectedIndex(ulong assign, int startVar, int k)
    {
        // startVar is DIMACS var id of first selector
        // exactly-one expected; if multiple,set first; if none,return 0
        for (int i = 0; i < k; i++)
        {
            int varId = startVar + i;
            if (((assign >> (varId - 1)) & 1UL) != 0) return i;
        }
        return 0;
    }

    private static ulong ParseHexU64(string s)
    {
        s = s.Trim();
        if (s.StartsWith("0x", StringComparison.OrdinalIgnoreCase)) s = s[2..];
        return ulong.Parse(s, NumberStyles.HexNumber, CultureInfo.InvariantCulture);
    }

    private sealed record IrisRow(double[] X, int Label);

    private static List<IrisRow> LoadIrisCsv(string path)
    {
        var list = new List<IrisRow>(160);
        foreach (var line in File.ReadLines(path))
        {
            if (string.IsNullOrWhiteSpace(line)) continue;
            if (line.StartsWith("sepal", StringComparison.OrdinalIgnoreCase)) continue;

            var p = line.Split(',', StringSplitOptions.RemoveEmptyEntries | StringSplitOptions.TrimEntries);
            if (p.Length < 5) continue;

            double f0 = double.Parse(p[0], CultureInfo.InvariantCulture);
            double f1 = double.Parse(p[1], CultureInfo.InvariantCulture);
            double f2 = double.Parse(p[2], CultureInfo.InvariantCulture);
            double f3 = double.Parse(p[3], CultureInfo.InvariantCulture);

            int label = p[4] switch
            {
                "setosa" or "Iris-setosa" => 0,
                "versicolor" or "Iris-versicolor" => 1,
                "virginica" or "Iris-virginica" => 2,
                _ => throw new InvalidOperationException("Unknown label:" + p[4])
            };

            list.Add(new IrisRow(new[] { f0, f1, f2, f3 }, label));
        }
        return list;
    }

    private sealed class MapFile
    {
        public string IrisCsv { get; set; } = "";
        public int K1 { get; set; }
        public int K2 { get; set; }
        public double[] T1 { get; set; } = Array.Empty<double>();
        public double[] T2 { get; set; } = Array.Empty<double>();
        public int SelT1Start { get; set; }
        public int SelT2Start { get; set; }
        public int D { get; set; }
        public string Model { get; set; } = "";
    }
}

Почему это “научно корректно”, а не подгон
Мы фиксируем класс модели (структуру дерева решений) и оптимизируем параметры внутри него — это то же самое, что вы делаете в ML, когда выбираете “логистическая регрессия” или “дерево глубины 2”, а затем учите параметры. Мы не “вшиваем ответ”; мы задаём гипотезу и оптимизируем её по данным.

Более строгий вариант (и хороший план для продолжения):
разделить данные на train/test или k‑fold,
обучать пороги на train, оценивать на test,
и/или расширить пространство: дать солверу выбирать не только значения порогов, но и признаки/направления сравнения/структуру дерева (в пределах лимита переменных).

Практические правила: как кодировать задачи в SAT и не утонуть
Если вы хотите переносить “любые задачи” в SAT/MaxSAT,нужно придерживаться инженерных правил, иначе формула взорвётся по размеру.

Начинайте с переменных: что именно “решаем”
Хороший признак: переменные описывают выбор (select/assign/route/schedule),а не каждую микродеталь мира.
Отделяйте hard и soft
Hard: структурные ограничения (валидность решения).
Soft: целевая функция через штрафы/награды.

И следите за масштабами: hard должны доминировать, иначе солвер начнёт “покупать” нарушения структуры ради выгодных soft.

Дискретизация — это не зло, это управление сложностью
SAT любит дискретное. Если модель непрерывная — выбирайте осмысленную сетку параметров (как мы сделали с порогами), или ограничьте семейство.
Делайте декодер и верификатор “в комплекте”
SAT‑решение без декодирования и независимой проверки — это просто битовая строка. Для честной инженерии:
декодер: bits → параметры
верификатор: проверка метрики на исходных данных
Ищите структуру, которая даёт максимум качества за минимум переменных
В Iris ключевая структура была известна (лепестки),поэтому мы выбрали компактную гипотезу и получили высокий результат при vars<=64.

Почему переход “нейросети → SAT” потенциально огромен
Где SAT/MaxSAT выигрывает у классического “обучения градиентом”:

Точность в смысле оптимума: в дискретных пространствах можно реально оптимизировать “сколько ошибок/штрафов” без локальных минимумов (в пределах выбранной дискретизации).
Ограничения как граждане первого класса:монотонность, запреты, комплаенс, логические правила — всё это естественно задаётся в CNF.
Объяснимость: решение часто декодируется в правила/структуру (пороги,выборы,граф), а не в миллионы float‑весов.
Верифицируемость: решение можно проверить детерминированно, без “плавающих” чисел.
Репродуцируемость: один и тот же инстанс → одни и те же метрики; вариативность только от рандома солвера и параметров.

Ограничения тоже есть: SAT не заменит DL в задачах восприятия (изображения/звук) без сильной предварительной дискретизации, а большие постановки требуют аккуратного моделирования.

Чем мы решали CNF
Для решения получившейся Max‑3SAT‑формулы мы использовали AGIQ Solver Enterprise. Он хорошо подходит для таких задач, потому что умеет эффективно крутить большие популяции решений на GPU и искать оптимумы в NP‑пространстве.

Заключение
В этом посте мы показали не “магический трюк”, а практический паттерн:

выбираем компактную модель,
переводим обучение в MaxSAT (ошибка = штраф),
решаем на NP‑солвере,
декодируем и считаем метрики.

Если захотите прогнать это на своих данных или поставить пилот — мы выдаём тестовые ключи для AGIQ Solver Enterprise бесплатно,чтобы можно было спокойно проверить идею на реальных задачах.

Нейросеть без нейросети: как обучить классификатор Iris через SAT и запустить это на GPU