1. La révolution algorithmique silencieuse de l’informatique

Ouvrez n’importe quel manuel d’informatique théorique et vous y trouverez cet avertissement solennel : « Le problème de satisfaisabilité booléenne (SAT) est NP-complet. Sa complexité temporelle dans le pire des cas croissant exponentiellement en $O(2^n)$ avec le nombre de variables $n$, les grandes instances sont fondamentalement intraitables. »

Sur le plan purement combinatoire, le constat semble sans appel. Une formule portant sur $n = 100$ variables booléennes admet $2^{100} \approx 1,26 \times 10^{30}$ affectations de vérité possibles. Même si un supercalculateur inspectait $10^{12}$ affectations par seconde depuis le Big Bang (il y a 13,8 milliards d’années), il aurait exploré moins de $10^{-8}$ de l’espace de recherche aujourd’hui. De fait, vers 1990, les meilleurs solveurs SAT butaient sur des formules d’à peine $100$ variables et $400$ clauses.

Pourtant, au XXIᵉ siècle, la pratique industrielle dément cette intuition des millions de fois par jour. Les solveurs SAT et SMT modernes — tels que MiniSat, Glucose, Lingeling, CaDiCaL, Kissat et Z3 (Microsoft Research) — résolvent quotidiennement des instances de vérification formelle de microprocesseurs, d’optimisation de compilateurs et de gestion de paquets contenant $10\,000\,000$ ($10^7$) variables et $50\,000\,000$ ($5 \times 10^7$) clauses en quelques secondes.

Dans le volume 4B (section 7.2.2.2) de The Art of Computer Programming publié en 2015, Donald E. Knuth a consacré plus de 300 pages aux seuls solveurs SAT, saluant les avancées de la fin des années 1990 et du début des années 2000 comme l’une des plus grandes révolutions algorithmiques de l’histoire de l’informatique. Autrefois, réduire un problème à SAT revenait à prouver son insolubilité pratique ; aujourd’hui, traduire un problème combinatoire en SAT est la stratégie royale pour le résoudre instantanément.

2. Forme normale conjonctive (CNF), transformation de Tseitin et théorème de Cook-Levin (1971)

2.1 Forme normale conjonctive (CNF) et encodage linéaire de Tseitin

Un solveur SAT prend en entrée une formule propositionnelle $\Phi$ sur $n$ variables booléennes $V = \{x_1, \dots, x_n\}$ à valeurs dans $\{0, 1\}$. Un littéral $\ell \in \{x_v, \neg x_v\}$ est une variable ou sa négation ; une clause $C_i = \bigvee_{j=1}^{k_i} \ell_{i,j}$ est une disjonction (OU logique, $\lor$) de littéraux ; et une formule en forme normale conjonctive (CNF) est une conjonction (ET logique, $\land$) de $m$ clauses :

Si l’on convertissait naïvement un circuit booléen arbitraire en CNF par application répétée de la distributivité $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$, la taille de la formule exploserait exponentiellement. En 1968, Grigori Tseitin a résolu ce problème grâce à la transformation de Tseitin : on introduit une variable auxiliaire $y_g$ pour la sortie de chaque porte logique $g$ du circuit et l’on encode l’équivalence locale $y_g \leftrightarrow \text{porte}(a, b)$ en seulement 3 ou 4 clauses. Par exemple, une porte ET $y_g \leftrightarrow (a \land b)$ se traduit par exactement trois clauses :

Tout circuit comportant $|G|$ portes est ainsi converti en temps et en espace strictement linéaires $O(|G|)$ en une formule 3-CNF équisatisfaisable.

2.2 Le théorème de Cook-Levin et la falaise de complexité entre 2-SAT et 3-SAT

En 1971, Stephen Cook et Leonid Levin ont démontré indépendamment le théorème de Cook-Levin : tout problème de décision appartenant à la classe $\text{NP}$ peut être réduit en temps polynomial à SAT en encodant le tableau de calcul d’une machine de Turing non déterministe sur $p(n)$ étapes (états $S_{t,q}$, positions de tête $H_{t,i}$, symboles du ruban $T_{t,i,\sigma}$) sous forme de clauses CNF.

Lorsque chaque clause contient au plus $k$ littéraux ($k$-SAT), une falaise abrupte sépare $k = 2$ et $k = 3$ :

• 2-SAT se résout en temps linéaire $O(n + m)$ : une clause binaire $(\ell_1 \lor \ell_2)$ équivaut à deux implications dirigées déterministes $(\neg \ell_1 \Rightarrow \ell_2) \land (\neg \ell_2 \Rightarrow \ell_1)$. Dans le graphe d’implication à $2n$ sommets, l’algorithme de Tarjan identifie les composantes fortement connexes (CFC / SCC) en temps $O(n+m)$ : la formule est satisfaisable si et seulement si aucune variable $x_v$ n’appartient à la même CFC que $\neg x_v$.
• 3-SAT est NP-complet : une clause ternaire $(\ell_1 \lor \ell_2 \lor \ell_3)$ s’écrit $(\neg \ell_1 \land \neg \ell_2) \Rightarrow \ell_3$, une hyperarête nécessitant deux prémisses simultanées. Sous l’hypothèse du temps exponentiel (ETH), aucun algorithme déterministe ne peut résoudre 3-SAT en temps sous-exponentiel $2^{o(n)}$ dans le pire cas.

3. L’algorithme DPLL classique (1962) et le piège du retour sur trace chronologique

L’algorithme DPLL (Davis, Putnam, Logemann, Loveland, 1962) repose sur la recherche en profondeur couplée à la propagation unitaire (Unit Propagation / Boolean Constraint Propagation, BCP) :

Propagation unitaire (BCP) : Si, sous l’affectation partielle courante, tous les littéraux d’une clause $C = (\ell_1 \lor \dots \lor \ell_{k-1} \lor \ell_k)$ sauf $\ell_k$ valent False ($0$) et que $\ell_k$ est non affecté, $C$ est une clause unitaire. Le solveur force immédiatement $\ell_k = \text{True}$ ($1$), déclenchant une cascade domino d’implications jusqu’à saturation ou jusqu’à ce qu’une clause devienne entièrement fausse (Conflit).

Pourquoi DPLL plafonnait-il autour de 100 variables ? À cause du retour sur trace chronologique (Chronological Backtracking). Si le solveur fixe $x_1 = 0$ au niveau de décision $d = 1$, effectue 48 choix totalement indépendants $x_2, \dots, x_{49}$ aux niveaux $d = 2 \dots 49$, puis choisit $x_{50} = 1$ au niveau $d = 50$, provoquant un conflit local uniquement dû à $x_1 = 0$ et $x_{50}$ via les clauses $(x_1 \lor \neg x_{50} \lor \pm x_{51})$ et $(x_1 \lor x_{50} \lor \pm x_{52})$, DPLL est incapable d’identifier que la faute remonte au niveau 1. Il recule d’un seul cran au niveau $d = 49$, inverse l’innocente variable $x_{49}$ et répète exactement le même échec à travers $2^{48} \approx 2,81 \times 10^{14}$ sous-arbres inutiles (piétinement / thrashing) !

4. La révolution CDCL : graphe d’implication, résolution 1-UIP et saut arrière

Introduit dans GRASP (Marques-Silva & Sakallah, 1996) et porté à maturité dans Chaff (Moskewicz et al., 2001), l’apprentissage de clauses dirigé par les conflits (CDCL) remplace l’aveuglement chronologique par le diagnostic causal.

  flowchart TD
    Start["Entrée : Formule CNF Φ (Niveau de décision d = 0)"] --> BCP["Propagation des contraintes booléennes (BCP)<br/>Propagation unitaire rapide via Deux Littéraux Surveillés (2WL)"]
    BCP --> CheckConflict{"Clause de conflit κ<br/>falsifiée ?"}
    CheckConflict -- "Aucun conflit" --> CheckAllAssigned{"Toutes les variables<br/>affectées ?"}
    CheckAllAssigned -- "Oui" --> SAT["SATISFAISABLE (SAT)<br/>Renvoyer le modèle σ"]
    CheckAllAssigned -- "Non" --> Branch["Branchement (Decision) : d ← d + 1<br/>Choisir la variable avec activité VSIDS maximale<br/>Affecter la polarité via Phase Saving"]
    Branch --> BCP
    CheckConflict -- "Oui (Conflit !)" --> CheckLevelZero{"Au niveau racine<br/>d == 0 ?"}
    CheckLevelZero -- "Oui" --> UNSAT["INSATISFAISABLE (UNSAT)<br/>Émettre le certificat de preuve DRAT"]
    CheckLevelZero -- "Non (d > 0)" --> Analyze["Analyse de conflit (Résolution 1-UIP)<br/>Remonter le graphe d'implication depuis κ<br/>Résoudre jusqu'à n'avoir qu'un seul littéral du niveau d (First UIP)"]
    Analyze --> Learn["Apprendre la clause & incrémenter VSIDS<br/>Ajouter C_learned à la base (calculer LBD)<br/>Augmenter le score VSIDS des variables impliquées"]
    Learn --> Backjump["Saut arrière non chronologique (Backjump)<br/>Sauter directement au niveau d'assertion d_back (2e plus haut niveau dans C_learned)<br/>C_learned devient immédiatement unitaire dans BCP !"]
    Backjump --> BCP

4.1 Graphe d’implication, résolution booléenne et premier point d’implication unique (1-UIP)

Chaque littéral affecté $\ell@d$ conserve son niveau de décision $d$ et sa clause antécédente (raison) $\text{reason}(\ell)$. Lorsqu’une clause $\kappa$ est falsifiée, CDCL initialise $C \leftarrow \kappa$ et remonte la pile d’affectation (Trail) au niveau courant $d_{\text{curr}}$ en appliquant itérativement la règle de résolution booléenne :

Dans le graphe d’implication, un sommet $u@d_{\text{curr}}$ est un point d’implication unique (Unique Implication Point, UIP) si tout chemin dirigé allant du littéral de décision $\ell_{\text{dec}}@d_{\text{curr}}$ au sommet de conflit $\Lambda$ passe obligatoirement par $u$ (dominateur). Le UIP le plus proche du conflit est appelé premier UIP (First UIP / 1-UIP). Algébriquement, la résolution arrière atteint le 1-UIP à l’instant précis où la clause de travail $C$ ne contient plus qu’un seul littéral appartenant au niveau de décision courant $d_{\text{curr}}$ !

Dans notre exemple avec $x_1 = 0@1, x_2 = 0@2, x_3 = 1@3$, la décision $x_4 = 1@5$ et les clauses $\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)$ menant au conflit $\kappa = (\neg x_7 \lor \neg x_8)$, deux étapes de résolution de $\kappa$ avec $\omega_4$ (pivot $x_8$) puis $\omega_3$ (pivot $x_7$) isolent immédiatement la clause apprise 1-UIP :

4.2 Saut arrière non chronologique (Backjumping) et niveau d’assertion

Les niveaux présents dans $C_{\text{learned}}$ étant $\{5, 3, 2\}$, le solveur saute directement au deuxième niveau de décision le plus élevé (niveau d’assertion) $d_{\text{back}} = 3$ ! Au niveau $3$, $x_2@2$ et $\neg x_3@3$ sont toujours faux tandis que $\neg x_6$ redevient libre : $C_{\text{learned}}$ agit instantanément comme une clause unitaire asserteuse et force $\neg x_6 = 1@3$ ($x_6 = 0@3$) via BCP !

5. Miracles d’ingénierie : deux littéraux surveillés (2WL), VSIDS et LBD

1. Deux littéraux surveillés (Two-Watched Literals, 2WL, Chaff 2001) : Puisque $90\%$ du temps CPU est consacré à BCP, 2WL s’appuie sur l’invariant suivant : tant qu’une clause comporte au moins deux littéraux non falsifiés (libres ou vrais), elle ne peut devenir ni unitaire ni conflictuelle. Le solveur ne surveille donc que deux littéraux $w_1, w_2$ par clause. Lors d’un saut arrière (Backjump), la désaffectation des variables préserve automatiquement cet invariant : le retour arrière ne nécessite aucune mise à jour de pointeurs ($O(1)$, coût zéro) !
2. VSIDS (Variable State Independent Decaying Sum) & Phase Saving : Chaque variable impliquée dans la résolution d’un conflit reçoit un bonus d’activité $+\Delta$, tandis que $\Delta \leftarrow \Delta / \gamma$ ($\gamma = 0.95$) croît après chaque conflit. Cette moyenne mobile exponentielle concentre le branchement sur le goulot d’étranglement actif.
3. LBD (Literal Block Distance / Clauses « Glue ») & Redémarrages rapides : Glucose (Audemard & Simon, 2009) mesure la qualité d’une clause apprise par le nombre $\text{LBD}(C)$ de niveaux de décision distincts qu’elle contient. Les clauses avec $\text{LBD} = 2$ (clauses de colle / Glue Clauses) lient directement l’UIP courant à un unique bloc de décision passé et sont conservées indéfiniment.

6. Implémentation Python complète d’un moteur CDCL

Voici une implémentation Python autonome et complète d’un solveur CDCL intégrant BCP, graphe d’implication, résolution 1-UIP, saut arrière non chronologique et 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. Physique statistique et transition de phase du $k$-SAT aléatoire ($\alpha_c \approx 4,267$)

Pourquoi les solveurs CDCL écrasent-ils des instances industrielles à $10^7$ variables mais échouent-ils sur des formules 3-SAT aléatoires de $700$ variables ? Pour une formule 3-SAT aléatoire à $n$ variables et $m = \alpha n$ clauses (densité de contraintes $\alpha = m / n$), la méthode du premier moment donne l’espérance du nombre de solutions $Z$ :

Grâce à la méthode de la cavité et à la brisure de symétrie des répliques à une étape (1RSB) issue de la physique des verres de spin, Mézard, Parisi et Zecchina (2002) ont établi le seuil critique exact du 3-SAT aléatoire :

  flowchart TD
    subgraph PhaseTransition["Transition de phase du 3-SAT aléatoire selon la densité α = m/n"]
        S1["1. Phase liquide sous-contrainte (α < 3,86 : Easy-SAT)<br/>• Les solutions forment un unique amas géant connexe sur {0,1}^n<br/>• Résolution rapide en temps polynomial"]
        S2["2. Phase vitreuse de fragmentation et gel (3,86 < α < 4,267 : Hard-SAT)<br/>• À α_d ≈ 3,86 (transition 1RSB), l'espace des solutions éclate en un nombre exponentiel d'îlots isolés !<br/>• À α_f ≈ 4,254, les variables se figent rigidement dans chaque amas (Freezing)"]
        S3["3. Seuil critique de satisfaisabilité (α_c ≈ 4,267 : Pic de dureté exponentiel)<br/>• La probabilité de SAT chute brutalement de 1 à 0<br/>• Toute réfutation par résolution exige une taille exponentielle 2^Ω(n) (Chvátal–Szemerédi)"]
        S4["4. Phase sur-contrainte (α > 4,267 : Easy-UNSAT)<br/>• La forte densité de clauses déclenche des contradictions à faible profondeur<br/>• Le temps de résolution diminue quand α augmente"]
    end
    S1 -->|"α_d ≈ 3,86 (Fragmentation)"| S2
    S2 -->|"α_c ≈ 4,267 (Transition UNSAT)"| S3
    S3 -->|"α > 4,267 (Conflits rapides)"| S4

Au point critique $\alpha_c \approx 4,267$, l’hypergraphe aléatoire est un graphe expanseur dépourvu de goulots d’étranglement locaux, ce qui impose à toute preuve par résolution une longueur exponentielle $2^{\Omega(n)}$ (Chvátal & Szemerédi, 1988). Les instances industrielles réelles possèdent au contraire une structure cachée :

1. Modularité et structure communautaire (Ansótegui et al. 2012) : les circuits et logiciels sont composés de modules faiblement couplés par un petit nombre de variables d’interface, que la résolution 1-UIP identifie immédiatement comme dominateurs pour générer des clauses Glue ($\text{LBD}=2$).
2. Petits ensembles « Backdoor » (Williams, Gomes, Selman 2003) : il suffit souvent d’affecter quelques dizaines de variables clés $B \subset V$ ($|B| \ll n$) pour que le reste de la formule à 10 millions de variables s’effondre intégralement par propagation unitaire !

8. Triomphes industriels et preuve mathématique de 200 téraoctets

1. Mathématiques assistées par ordinateur et preuve DRAT de 200 To (Heule, Kullmann, Marek 2016) : Peut-on bicolorer $\{1, \dots, N\}$ sans créer de triplet pythagoricien $a^2 + b^2 = c^2$ monochrome ? Par Cube-and-Conquer, Heule et al. ont prouvé sur 800 cœurs que $N = 7824$ est satisfaisable (SAT) mais que $N = 7825$ est insatisfaisable (UNSAT), produisant un certificat de preuve formelle DRAT de 200 téraoctets vérifié bit à bit ! Ils ont ensuite résolu le nombre de Schur $S(5) = 160$ (2018) et la conjecture de Keller en dimension 7 (2020).
2. Vérification formelle EDA (CEC et BMC) : depuis le bogue FDIV du Pentium d’Intel (1994), chaque processeur est vérifié en construisant un circuit Miter (XOR entre spécification RTL et circuit synthétisé) soumis à un solveur SAT.
3. Gestionnaires de paquets (Debian apt, Rust Cargo, Dart PubGrub, uv) : l’algorithme PubGrub exécute directement CDCL sur les contraintes de versions et traduit le graphe de résolution 1-UIP en explications claires lors des conflits.
4. De SAT à SMT ($\text{DPLL}(T)$ : Z3 et cvc5) : en couplant CDCL avec des solveurs de théories (arithmétique linéaire, vecteurs de bits, tableaux), les solveurs SMT propulsent l’exécution symbolique et le moteur de sécurité cloud AWS Zelkova.