1. Histoire : La mère de tous les problèmes NP-Complets
Jusqu'au début des années 1970, la notion de "problème difficile" était floue. On savait que certains problèmes prenaient un temps exponentiel, mais on ignorait s'ils étaient liés entre eux. En 1971, le mathématicien canado-américain Stephen Cook publie un article révolutionnaire : "The Complexity of Theorem-Proving Procedures". Indépendamment et presque simultanément (1973), le mathématicien soviétique Leonid Levin arrive à la même conclusion de l'autre côté du rideau de fer.
Le Théorème de Cook-Levin : Ils ont prouvé mathématiquement que n'importe quel algorithme s'exécutant sur un ordinateur peut être traduit en une gigantesque formule logique (SAT). Par conséquent, si l'on trouve un algorithme rapide pour résoudre SAT, on peut résoudre TOUS les problèmes de la classe NP rapidement.
SAT fut ainsi le tout premier problème prouvé NP-complet. L'année suivante (1972), Richard Karp s'en servit comme "point de départ" pour montrer que 21 autres problèmes célèbres (dont 3-SAT, le Voyageur de Commerce, le Sac à dos, la Coloration, etc.) étaient eux aussi NP-complets par réduction à partir de SAT.
2. Définition Mathématique (FNC)
Problème 3-SAT :
Soit un ensemble de $n$ variables booléennes $x_1, x_2, \dots, x_n \in \{\text{Vrai}, \text{Faux}\}$.
Une formule $\Phi$ est en Forme Normale Conjonctive (FNC) si elle est un ET ($\wedge$) de $m$ clauses. Dans 3-SAT, chaque clause est un OU ($\vee$) d'exactement 3 littéraux (une variable $x_i$ ou sa négation $\neg x_i$).
$$ \Phi = (x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_4 \vee \neg x_3) \wedge \dots $$
Question : Existe-t-il une assignation des variables telle que $\Phi$ s'évalue à VRAI (c'est-à-dire que toutes les clauses soient satisfaites) ?
Note : 2-SAT (clauses de 2 littéraux) est résoluble en temps polynomial. La difficulté explose brutalement dès qu'on passe à 3 littéraux.
3. Exercice : Craquez le code logique
L'ordinateur agit comme le Vérificateur Polynomial : à chaque clic, il évalue les clauses. Règle du jeu : Cliquez sur les variables pour changer leur état (Gris = Indéfini, Vert = Vrai, Rouge = Faux). Votre but est de rendre toutes les clauses Vertes.
État de la formule :
Clauses validées : 0 / 0
L'ordinateur explore l'arbre de recherche. S'il échoue, il prouve que la formule est insatisfaisable.