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.