1. Тихая алгоритмическая революция в информатике

Откройте любой учебник по теоретической информатике, и вы увидите суровое предупреждение: «Задача выполнимости булевых формул (Boolean Satisfiability Problem, SAT) является NP-полной. Поскольку её временная сложность в худшем случае растёт экспоненциально как \(O(2^n)\) от числа переменных \(n\), крупные экземпляры задачи практически неразрешимы (intractable)».

С точки зрения чистой комбинаторики этот вывод кажется неоспоримым. Формула всего лишь со \(n = 100\) булевыми переменными допускает \(2^{100} \approx 1,26 \times 10^{30}\) возможных наборов значений истинности. Даже если бы суперкомпьютер проверял по \(10^{12}\) наборов в секунду с момента Большого взрыва (13,8 млрд лет назад), к сегодняшнему дню он исследовал бы менее \(10^{-8}\) пространства поиска. И действительно, около 1990 года лучшие в мире SAT-солверы заходили в тупик на формулах из \(100\) переменных и \(400\) дизъюнктов (клауз).

Однако в XXI веке инженерная реальность опровергает эту интуицию миллионы раз в день. Современные промышленные SAT- и SMT-солверы — такие как MiniSat, Glucose, Lingeling, CaDiCaL, Kissat и Z3 от Microsoft Research — при формальной верификации микропроцессоров, оптимизации компиляторов и разрешении зависимостей пакетов буднично решают гигантские формулы, содержащие \(10\,000\,000\) (\(10^7\)) переменных и \(50\,000\,000\) (\(5 \times 10^7\)) дизъюнктов, всего за несколько секунд.

Когда Дональд Кнут (Donald E. Knuth) в 2015 году опубликовал том 4B (раздел 7.2.2.2) «Искусства программирования» (TAOCP), он посвятил SAT-солверам более 300 страниц, назвав прорыв конца 1990-х — начала 2000-х годов одной из величайших алгоритмических революций в истории компьютерных наук. Если раньше сведение задачи к SAT означало приговор о её практической неразрешимости, то сегодня трансляция комбинаторной задачи в SAT — это главный инженерный способ мгновенно решить её с помощью универсального решателя.

2. Конъюнктивная нормальная форма (КНФ), преобразование Цейтина и теорема Кука — Левина (1971)

2.1 Конъюнктивная нормальная форма (КНФ) и линейное кодирование Цейтина

На вход SAT-солверу подаётся пропозициональная формула \(\Phi\) над \(n\) булевыми переменными \(V = \{x_1, \dots, x_n\}\) со значениями в \(\{0, 1\}\). Переменная \(x_v\) или её отрицание \(\neg x_v\) называется литералом \(\ell\); дизъюнкция (логическое ИЛИ, \(\lor\)) литералов образует дизъюнкт (клаузу / Clause) \(C_i = \bigvee_{j=1}^{k_i} \ell_{i,j}\); а конъюнкция (логическое И, \(\land\)) \(m\) дизъюнктов образует формулу в конъюнктивной нормальной форме (КНФ / CNF):

При наивном раскрытии скобок по закону дистрибутивности \(A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)\) размер произвольной логической схемы в КНФ взрывается экспоненциально. В 1968 году советский математик Григорий Самуилович Цейтин предложил преобразование Цейтина (Tseitin Transformation): для выхода каждого логического вентиля \(g\) вводится новая вспомогательная переменная \(y_g\), а локальная эквивалентность \(y_g \leftrightarrow \text{gate}(a, b)\) записывается всего 3–4 дизъюнктами. Например, вентиль И \(y_g \leftrightarrow (a \land b)\) кодируется тремя дизъюнктами:

Благодаря преобразованию Цейтина любая булева схема из \(|G|\) вентилей за строго линейное время и линейную память \(O(|G|)\) переводится в равновыполнимую (equisatisfiable) 3-КНФ формулу.

2.2 Теорема Кука — Левина и пропасть сложности между 2-SAT и 3-SAT

В 1971 году Стивен Кук и Леонид Левин независимо доказали теорему Кука — Левина: любая задача распознавания из класса \(\text{NP}\) сводится за полиномиальное время к SAT путём кодирования пространственно-временной таблицы вычислений недетерминированной машины Тьюринга за \(p(n)\) шагов (состояний \(S_{t,q}\), положения головки \(H_{t,i}\) и символов на ленте \(T_{t,i,\sigma}\)) в виде КНФ-формулы.

Между \(k = 2\) и \(k = 3\) литералами в каждом дизъюнкте (\(k\)-SAT) лежит пропасть:

• 2-SAT решается за линейное время \(O(n + m)\): бинарный дизъюнкт \((\ell_1 \lor \ell_2)\) эквивалентен двум направленным импликациям \((\neg \ell_1 \Rightarrow \ell_2) \land (\neg \ell_2 \Rightarrow \ell_1)\). В графе импликаций над \(2n\) литералами алгоритм Тарьяна находит компоненты сильной связности (SCC) за время \(O(n+m)\): формула выполнима тогда и только тогда, когда ни одна переменная \(x_v\) не лежит в одной компоненте сильной связности со своим отрицанием \(\neg x_v\).
• 3-SAT является NP-полной: тернарный дизъюнкт \((\ell_1 \lor \ell_2 \lor \ell_3)\) эквивалентен \((\neg \ell_1 \land \neg \ell_2) \Rightarrow \ell_3\) — гиперребру, требующему одновременной истинности двух посылок. Согласно гипотезе экспоненциального времени (ETH), для 3-SAT не существует субэкспоненциального алгоритма \(2^{o(n)}\) в худшем случае.

3. Классический алгоритм DPLL (1962) и трагедия хронологического возврата

Алгоритм DPLL (Davis, Putnam, Logemann, Loveland, 1962) сочетает поиск в глубину с единичным распространением (Unit Propagation / Boolean Constraint Propagation, BCP):

Единичное распространение (BCP): Если при текущем частичном присваивании все литералы дизъюнкта \(C = (\ell_1 \lor \dots \lor \ell_{k-1} \lor \ell_k)\), кроме \(\ell_k\), приняли значение False (\(0\)), а \(\ell_k\) ещё не присвоен, то \(C\) называется единичным дизъюнктом (Unit Clause). Солвер немедленно принудительно полагает \(\ell_k = \text{True}\) (\(1\)), запуская цепную реакцию домино до насыщения или до обращения всех литералов некоторого дизъюнкта в False (Конфликт).

Почему DPLL не мог преодолеть барьер в 100 переменных? Из-за хронологического бэктрекинга (Chronological Backtracking). Если на уровне решения \(d = 1\) выбрано \(x_1 = 0\), затем на уровнях \(d = 2 \dots 49\) сделаны 48 независимых присваиваний переменным \(x_2, \dots, x_{49}\), а на уровне \(d = 50\) присвоено \(x_{50} = 1\), что немедленно вызывает конфликт исключительно из-за \(x_1 = 0\) и \(x_{50}\) в дизъюнктах \((x_1 \lor \neg x_{50} \lor \pm x_{51})\) и \((x_1 \lor x_{50} \lor \pm x_{52})\), то DPLL слепо откатывается лишь на один шаг к уровню \(d = 49\), инвертирует ни в чём не повинную переменную \(x_{49}\) и повторяет одно и то же фиаско во всех \(2^{48} \approx 2,81 \times 10^{14}\) бесполезных поддеревьях (пробуксовка / thrashing)!

4. Революция CDCL: граф импликаций, резолюция 1-UIP и нехронологический прыжок

Предложенная в GRASP (Marques-Silva & Sakallah, 1996) и доведённая до совершенства в Chaff (Moskewicz et al., 2001) архитектура CDCL (Conflict-Driven Clause Learning — обучение дизъюнктам, управляемое конфликтами) заменила слепой откат анализом первопричин конфликта.

  flowchart TD
    Start["Вход: КНФ-формула Φ (Уровень решения d = 0)"] --> BCP["Распространение булевых ограничений (BCP)<br/>Быстрое единичное распространение через два наблюдаемых литерала (2WL)"]
    BCP --> CheckConflict{"Конфликтный дизъюнкт κ<br/>опровергнут?"}
    CheckConflict -- "Нет конфликта" --> CheckAllAssigned{"Все переменные<br/>присвоены?"}
    CheckAllAssigned -- "Да" --> SAT["ВЫПОЛНИМА (SAT)<br/>Вернуть выполняющий набор σ"]
    CheckAllAssigned -- "Нет" --> Branch["Ветвление (Decision): d ← d + 1<br/>Выбрать переменную с макс. активностью VSIDS<br/>Задать полярность через Phase Saving"]
    Branch --> BCP
    CheckConflict -- "Да (Конфликт!)" --> CheckLevelZero{"На корневом уровне<br/>d == 0?"}
    CheckLevelZero -- "Да" --> UNSAT["НЕВЫПОЛНИМА (UNSAT)<br/>Вывести сертификат доказательства DRAT"]
    CheckLevelZero -- "Нет (d > 0)" --> Analyze["Анализ конфликта (Резолюция 1-UIP)<br/>Обход графа импликаций назад от κ<br/>Резолюция до тех пор, пока не останется 1 литерал уровня d (First UIP)"]
    Analyze --> Learn["Обучение дизъюнкту и обновление VSIDS<br/>Добавить C_learned в базу (вычислить LBD)<br/>Увеличить активность VSIDS задействованных переменных"]
    Learn --> Backjump["Нехронологический прыжок (Backjump)<br/>Прыжок сразу на уровень утверждения d_back (2-й макс. уровень в C_learned)<br/>C_learned мгновенно срабатывает как единичный дизъюнкт в BCP!"]
    Backjump --> BCP

4.1 Граф импликаций, булева резолюция и первая уникальная точка импликации (1-UIP)

Каждый присвоенный литерал \(\ell@d\) хранит свой уровень решения \(d\) и дизъюнкт-причину (Antecedent / Reason Clause) \(\text{reason}(\ell)\). При опровержении дизъюнкта \(\kappa\) CDCL инициализирует \(C \leftarrow \kappa\) и движется назад по стеку присваиваний (Trail) текущего уровня \(d_{\text{curr}}\), последовательно применяя правило булевой резолюции:

Вершина \(u@d_{\text{curr}}\) графа импликаций называется уникальной точкой импликации (UIP), если любой ориентированный путь от вершины решения \(\ell_{\text{dec}}@d_{\text{curr}}\) к вершине конфликта \(\Lambda\) проходит через \(u\) (доминатор). Ближайшая к конфликту точка UIP называется первой UIP (First UIP / 1-UIP). Алгебраически обратная резолюция достигает 1-UIP в тот самый момент, когда в рабочем дизъюнкте \(C\) остаётся ровно один литерал текущего уровня решения \(d_{\text{curr}}\)!

При \(x_1 = 0@1, x_2 = 0@2, x_3 = 1@3\), решении \(x_4 = 1@5\) и дизъюнктах \(\omega_1 = (x_1 \lor \neg x_4 \lor x_5)\), \(\omega_2 = (\neg x_4 \lor \neg x_5 \lor x_6)\), \(\omega_3 = (x_2 \lor \neg x_6 \lor x_7)\), \(\omega_4 = (\neg x_3 \lor \neg x_6 \lor x_8)\), ведущих к конфликту \(\kappa = (\neg x_7 \lor \neg x_8)\), два шага резолюции \(\kappa\) с \(\omega_4\) (по \(x_8\)) и с \(\omega_3\) (по \(x_7\)) сразу дают обученный дизъюнкт 1-UIP:

4.2 Нехронологический прыжок назад (Backjumping) и уровень утверждения

Поскольку уровни в \(C_{\text{learned}}\) равны \(\{5, 3, 2\}\), солвер прыгает сразу на второй по величине уровень решения (уровень утверждения) \(d_{\text{back}} = 3\)! На уровне \(3\) литералы \(x_2@2\) и \(\neg x_3@3\) остаются ложными, а \(\neg x_6\) становится свободным, благодаря чему \(C_{\text{learned}}\) мгновенно становится утверждающим единичным дизъюнктом и принудительно устанавливает \(\neg x_6 = 1@3\) (\(x_6 = 0@3\)) через BCP!

5. Инженерные чудеса: два наблюдаемых литерала (2WL), VSIDS и LBD

1. Два наблюдаемых литерала (Two-Watched Literals, 2WL, Chaff 2001): Пока в дизъюнкте есть хотя бы два неопровергнутых литерала, он не может стать ни единичным, ни конфликтным. Поэтому солвер следит только за двумя литералами \(w_1, w_2\) в каждом дизъюнкте. Самое главное: при прыжке назад (Backjump) отмена присваиваний автоматически сохраняет инвариант 2WL, поэтому откат требует ровно ноль обновлений указателей (\(O(1)\))!
2. VSIDS (Variable State Independent Decaying Sum) и Phase Saving: Переменные, участвующие в резолюции конфликта, получают прибавку \(+\Delta\) к активности, а \(\Delta \leftarrow \Delta / \gamma\) (\(\gamma = 0.95\)) растёт после каждого конфликта, фокусируя ветвление на текущем «горячем» узле.
3. LBD (Literal Block Distance / «Клеевые дизъюнкты») и быстрые рестарты: Солвер Glucose (Audemard & Simon, 2009) определяет \(\text{LBD}(C)\) как число различных уровней решений в дизъюнкте \(C\). Дизъюнкты с \(\text{LBD} = 2\) (Glue Clauses) связывают текущую точку UIP напрямую с одним прошлым блоком решений и сохраняются в базе навсегда.

6. Полная реализация ядра CDCL-солвера на Python

Ниже приведена полная автономная реализация CDCL-солвера на Python с поддержкой BCP, графа импликаций, резолюции 1-UIP, нехронологического прыжка и VSIDS:

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112

from typing import List, Dict, Optional, Set, Tuple

class CDCLSolver:
    '''Minimal Conflict-Driven Clause Learning (CDCL) SAT Solver with 1-UIP & VSIDS.'''
    def __init__(self, num_vars: int, clauses: List[List[int]]):
        self.num_vars = num_vars
        self.clauses: List[List[int]] = [list(set(c)) for c in clauses]
        self.assigns: Dict[int, bool] = {}
        self.trail: List[int] = []
        self.level: Dict[int, int] = {}
        self.reason: Dict[int, Optional[List[int]]] = {}
        self.decision_level: int = 0
        self.activity: Dict[int, float] = {v: 0.0 for v in range(1, num_vars + 1)}
        for c in self.clauses:
            for lit in c:
                self.activity[abs(lit)] += 1.0
        self.var_inc: float = 1.0
        self.var_decay: float = 0.95

    def value_lit(self, lit: int) -> Optional[bool]:
        var = abs(lit)
        if var not in self.assigns:
            return None
        return self.assigns[var] if lit > 0 else not self.assigns[var]

    def assign(self, lit: int, level: int, reason: Optional[List[int]]) -> None:
        var = abs(lit)
        self.assigns[var] = (lit > 0)
        self.trail.append(lit)
        self.level[var] = level
        self.reason[var] = reason

    def bcp(self) -> Optional[List[int]]:
        changed = True
        while changed:
            changed = False
            for clause in self.clauses:
                unassigned_lit = None
                num_unassigned = 0
                satisfied = False
                for lit in clause:
                    val = self.value_lit(lit)
                    if val is True:
                        satisfied = True
                        break
                    elif val is None:
                        num_unassigned += 1
                        unassigned_lit = lit
                if satisfied:
                    continue
                if num_unassigned == 0:
                    return clause
                if num_unassigned == 1 and unassigned_lit is not None:
                    self.assign(unassigned_lit, self.decision_level, clause)
                    changed = True
        return None

    def analyze_conflict(self, conflict_clause: List[int]) -> Tuple[List[int], int]:
        learned: Set[int] = set(conflict_clause)
        def count_curr_level(cset: Set[int]) -> int:
            return sum(1 for lit in cset if self.level[abs(lit)] == self.decision_level)

        idx = len(self.trail) - 1
        while count_curr_level(learned) > 1:
            while True:
                pivot_lit = self.trail[idx]
                idx -= 1
                if -pivot_lit in learned and self.level[abs(pivot_lit)] == self.decision_level:
                    break
            pivot_var = abs(pivot_lit)
            antecedent = self.reason[pivot_var]
            assert antecedent is not None
            self.activity[pivot_var] += self.var_inc
            learned.remove(-pivot_lit)
            for lit in antecedent:
                if lit != pivot_lit:
                    learned.add(lit)

        learned_clause = list(learned)
        for lit in learned_clause:
            self.activity[abs(lit)] += self.var_inc
        self.var_inc /= self.var_decay
        levels = sorted({self.level[abs(lit)] for lit in learned_clause}, reverse=True)
        backjump_level = levels[1] if len(levels) > 1 else 0
        return learned_clause, backjump_level

    def backtrack(self, target_level: int) -> None:
        while self.trail and self.level[abs(self.trail[-1])] > target_level:
            lit = self.trail.pop()
            var = abs(lit)
            del self.assigns[var], self.level[var], self.reason[var]
        self.decision_level = target_level

    def solve(self) -> Tuple[bool, Optional[Dict[int, bool]]]:
        if self.bcp() is not None:
            return False, None
        while True:
            unassigned = [v for v in range(1, self.num_vars + 1) if v not in self.assigns]
            if not unassigned:
                return True, dict(self.assigns)
            branch_var = max(unassigned, key=lambda v: self.activity[v])
            self.decision_level += 1
            self.assign(branch_var, self.decision_level, reason=None)
            while True:
                conflict = self.bcp()
                if conflict is None:
                    break
                if self.decision_level == 0:
                    return False, None
                learned_clause, backjump_level = self.analyze_conflict(conflict)
                self.clauses.append(learned_clause)
                self.backtrack(backjump_level)

7. Статистическая физика и фазовый переход в случайном \(k\)-SAT (\(\alpha_c \approx 4,267\))

Для случайной формулы 3-SAT с \(n\) переменными и \(m = \alpha n\) дизъюнктами (плотность ограничений \(\alpha = m / n\)) метод первого момента даёт математическое ожидание числа решений \(\mathbb{E}[Z]\):

Используя метод полости (Cavity Method) и одношаговое нарушение репличной симметрии (1RSB) из теории спиновых стёкол, Мезар, Паризи и Дзеккина (2002) нашли точный критический порог фазового перехода случайного 3-SAT:

  flowchart TD
    subgraph PhaseTransition["Фазовый переход случайного 3-SAT в зависимости от плотности α = m/n"]
        S1["1. Недоопределённая жидкая фаза (α < 3,86 : Easy-SAT)<br/>• Решения образуют единый гигантский связный кластер на кубе {0,1}^n<br/>• Быстрое нахождение решения за полиномиальное время"]
        S2["2. Стекольная фаза дробления и замораживания (3,86 < α < 4,267 : Hard-SAT)<br/>• При α_d ≈ 3,86 (переход 1RSB) пространство решений распадается на экспоненциальное число изолированных островов!<br/>• При α_f ≈ 4,254 переменные внутри кластеров жёстко замораживаются (Freezing)"]
        S3["3. Критический порог выполнимости (α_c ≈ 4,267 : Экспоненциальный пик сложности)<br/>• Вероятность SAT скачком падает с 1 до 0<br/>• Любое резолюционное опровержение требует экспоненциальной длины 2^Ω(n) (Хватал — Семереди)"]
        S4["4. Переопределённая фаза (α > 4,267 : Easy-UNSAT)<br/>• Высокая плотность дизъюнктов вызывает противоречия на малой глубине<br/>• Размер доказательства и время работы падают с ростом α"]
    end
    S1 -->|"α_d ≈ 3,86 (Дробление)"| S2
    S2 -->|"α_c ≈ 4,267 (Порог UNSAT)"| S3
    S3 -->|"α > 4,267 (Мелкие конфликты)"| S4

В точке \(\alpha_c \approx 4,267\) случайный гиперграф является экспандером без узких мест, поэтому любое резолюционное опровержение имеет экспоненциальную длину \(2^{\Omega(n)}\) (Chvátal & Szemerédi, 1988). Напротив, реальные промышленные задачи обладают модульной структурой сообществ (Community Structure) и малыми множествами «чёрного хода» (Backdoor Sets) (Ansótegui et al. 2012; Williams, Gomes, Selman 2003), что позволяет CDCL расщеплять формулы с 10 миллионами переменных за секунды.

8. Триумфы в реальном мире и 200-терабайтное математическое доказательство

1. Компьютерная математика и 200-ТБ доказательство DRAT (Heule, Kullmann, Marek 2016): С помощью метода Cube-and-Conquer на 800 ядрах было доказано, что булева проблема пифагоровых троек (\(a^2 + b^2 = c^2\)) выполнима при \(N = 7824\) (SAT), но невыполнима при \(N = 7825\) (UNSAT), с генерацией формально верифицированного DRAT-сертификата объёмом 200 Терабайт, а также решены число Шура \(S(5) = 160\) (2018) и гипотеза Келлера в размерности 7 (2020).
2. Формальная верификация микросхем EDA (CEC и BMC): схемы Miter (XOR между RTL-спецификацией и вентильной реализацией) проверяются SAT-солверами перед выпуском каждого современного процессора.
3. Пакетные менеджеры (Debian apt, Rust Cargo, Dart PubGrub, uv) и SMT-солверы (\(\text{DPLL}(T)\): Z3 и cvc5): объединяя ядро CDCL с решателями теорий первого порядка, они лежат в основе символьного исполнения и облачного движка безопасности AWS Zelkova.