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

Вступление
В прошлой статье я показывал,как мы в AGIQ Solver Enterprise ^[1] применили квантово‑вдохновлённый популяционный подход на GPU для NP‑задач и получили ускорение на практических постановках в 50–100 раз по сравнению с последовательным перебором и плохо распараллеливаемыми схемами.

Сегодня — следующий шаг:покажу,как задачи машинного обучения ^[2] можно кодировать в SAT/MaxSAT, а затем решать обычным NP‑солвером — тем же AGIQ Solver Enterprise.

О чём статья (и что мы НЕ делаем)
Мы не будем пытаться “запихнуть” в SAT весь мир DL (ResNet/LLM/градиенты/батчи). Это плохая идея: там, где нужна дифференцируемая оптимизация, SGD остаётся королём.

Зато есть большой класс ML‑задач, где:
модель дискретная или может быть дискретизирована,
важны ограничения (fairness/монотонность/запреты/политики),
важна проверяемость и воспроизводимость решения,
нужен глобальный поиск (а не локальная оптимизация по градиенту).

Вот здесь SAT/MaxSAT — это не экзотика,а универсальный язык “правила + ограничения + оптимизация”.

Почему SAT вообще способен “кодировать что угодно”
В теории, любой NP‑вопрос можно редуцировать к SAT. На практике это означает простую вещь:

1. Вы выбираете булевы переменные (что именно мы решаем?).

2. Вы пишете ограничения (что запрещено? что обязательно?).

3. Если есть “качество” (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) для каждого порога.

Дальше ключевой момент:мы превращаем ошибку ^[3] классификации в штраф.
Для каждого объекта и каждой пары (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 шага)

1. Генерируем CNF + map (кодировщик).

2. Решаем CNF в AGIQ Solver Enterprise и берём best assignment.

3. Декодируем 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; } = "";
    }
}
 [4]

Декодер: 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; } = "";
    }
}
 [4]

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

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

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

1. Начинайте с переменных: что именно “решаем”
   Хороший признак: переменные описывают выбор (select/assign/route/schedule),а не каждую микродеталь мира.

2. Отделяйте hard и soft
   Hard: структурные ограничения (валидность решения).
   Soft: целевая функция через штрафы/награды.

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

3. Дискретизация — это не зло, это управление сложностью
   SAT любит дискретное. Если модель непрерывная — выбирайте осмысленную сетку параметров (как мы сделали с порогами), или ограничьте семейство.

4. Делайте декодер и верификатор “в комплекте”
   SAT‑решение без декодирования и независимой проверки — это просто битовая строка. Для честной инженерии:
   декодер: bits → параметры
   верификатор: проверка метрики на исходных данных

5. Ищите структуру, которая даёт максимум качества за минимум переменных
   В Iris ключевая структура была известна (лепестки),поэтому мы выбрали компактную гипотезу и получили высокий результат при vars<=64.

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

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

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

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

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

1. выбираем компактную модель,

2. переводим обучение в MaxSAT (ошибка = штраф),

3. решаем на NP‑солвере,

4. декодируем и считаем метрики.

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