Informatique et mathématiques de l'ingénieur

SAT est le problème NP-complet historique : c'est le premier dont on ait démontré qu'il concentre à lui seul la difficulté de toute une classe. Cette place lui vaut une réputation d'infranchissable, et pourtant les solveurs traitent aujourd'hui des instances de plusieurs millions de variables. Les deux faits sont vrais en même temps, et les concilier demande de regarder de près ce que « difficile » veut dire : une garantie sur le pire cas, jamais une prédiction sur l'instance qu'on a devant soi. Ce chapitre situe SAT dans la théorie, puis montre ce qui sépare réellement une instance résoluble d'une instance qui résiste.

Vérifier n'est pas trouver

La classe NP

Un problème de décision est dans NP si toute réponse « oui » admet un certificat de taille raisonnable, vérifiable en temps polynomial.

Un certificat est simplement la preuve que fournit quelqu'un qui prétend avoir résolu le problème. Devant un labyrinthe, le certificat est le trait tracé au stylo depuis l'entrée : le trouver peut demander des heures, vérifier qu'il ne traverse aucun mur demande de le suivre du doigt une fois.

Pour SAT, le certificat est une affectation. La vérifier consiste à parcourir la formule une fois et à contrôler que chaque clause contient un littéral vrai : c'est linéaire en la taille de la formule, quelle qu'elle soit.

Vérifier un certificat, littéralement

Voici un vérificateur complet. Il tient en six lignes, et il suffirait tel quel à contrôler la sortie d'un solveur sur une instance d'un million de clauses.

main.py

Sortie

>_ Prêt à exécuter…

Le coût de ce contrôle est le nombre total de littéraux, une fois. Rien dans ce code ne ressemble à une recherche, et c'est tout le propos : la vérification est d'une autre nature que la résolution.

NP ne veut pas dire « non polynomial »

Le sigle vient de nondeterministic polynomial, et désigne ce qu'une machine capable de deviner résoudrait en temps polynomial. Beaucoup de problèmes de NP sont d'ailleurs faciles : tout problème résoluble en temps polynomial est dans NP, puisqu'on peut vérifier en résolvant.
L'ensemble des problèmes faciles s'appelle P, et la question ouverte est de savoir si

P = NP

, c'est-à-dire si deviner apporte quelque chose. Personne ne le sait, et personne n'y croit vraiment.

Une asymétrie qu'il faut remarquer

Une réponse oui à SAT se certifie en une ligne : voici l'affectation, vérifiez.
Une réponse non n'a pas de certificat aussi évident. Comment convaincre que rien ne marche, sans tout essayer ? Cette question est celle de la classe co-NP, et savoir si toute instance insatisfiable admet une preuve courte est un problème ouvert, équivalent à

NP = \text{co-}NP

.
Elle a une traduction très concrète, au chapitre 6 : les preuves de réfutation que produisent les solveurs sont parfois gigantesques, et l'on sait démontrer qu'elles ne peuvent pas toujours être courtes.

Le théorème de Cook-Levin

NP-complétude

Un problème est NP-difficile si tout problème de NP s'y ramène par une réduction polynomiale.

Il est NP-complet s'il est de plus dans NP.

Théorème de Cook-Levin, 1971

SAT est NP-complet.

L'idée de la démonstration tient en une phrase : tout programme qui vérifie une solution peut être traduit en une formule. Des variables décrivent l'état de la mémoire à chaque instant de l'exécution, et des clauses disent que chaque instruction fait bien ce qu'elle doit faire.

Cette formule est satisfiable si et seulement s'il existe une entrée que le programme accepte. Autrement dit : exécuter un programme, c'est satisfaire une formule. C'est un énoncé qu'il vaut la peine de laisser décanter, parce qu'il est à la fois le résultat théorique et le mode d'emploi de tout le domaine.

Ce que ce résultat a rendu possible

Une fois SAT établi NP-complet, démontrer qu'un nouveau problème l'est aussi ne demande plus de repartir des programmes : il suffit de ramener SAT à ce problème. Karp a publié 21 réductions de ce genre dès 1972, et la liste compte aujourd'hui des milliers d'entrées.
Le même résultat, lu à l'envers, fonde toute l'ingénierie des solveurs : puisque tout problème de NP se ramène à SAT, un bon solveur SAT est un bon solveur pour tout problème de NP. Il vaut donc la peine d'y consacrer trente ans d'efforts, ce qui est exactement ce qui s'est passé.

SAT comme langage d'assemblage

La comparaison est parlante. Personne n'écrit d'assembleur à la main, et pourtant tout finit par y passer : les langages de haut niveau y sont compilés, et l'effort d'optimisation se concentre sur un petit nombre de compilateurs et de processeurs.
SAT joue ce rôle pour les problèmes combinatoires. On modélise en haut niveau, on compile en clauses, on lance un solveur que des dizaines d'équipes améliorent depuis trente ans, puis on retraduit la réponse. C'est exactement le circuit décrit au chapitre 3, et le théorème de Cook-Levin est ce qui garantit qu'il existe toujours.

Ce qu'est une réduction, et dans quel sens elle va

C'est le mot le plus employé du chapitre, et le plus souvent mal compris, parce que son sens est orienté.

Réduction polynomiale

Réduire le problème $A$ au problème $B$ , noté $A \leq_p B$ , c'est donner un algorithme de traduction, en temps polynomial, qui transforme toute instance de $A$ en une instance de $B$ ayant la même réponse.

Le sens de lecture, dans les deux directions

A \leq_p B

se lit de deux façons, et les deux servent.
Vers le haut. Si

B

est facile, alors

A

l'est aussi : il suffit de traduire puis de résoudre. C'est ce qu'on emploie en pratique, avec

B

= SAT et un bon solveur.
Vers le bas. Si

A

est difficile, alors

B

l'est aussi : sinon on résoudrait

A

en passant par

B

. C'est ce qu'on emploie en théorie, avec

A

= SAT, pour démontrer qu'un nouveau problème est NP-difficile.
La faute classique est d'inverser le sens. Réduire son problème à SAT ne prouve pas qu'il est difficile : cela prouve seulement qu'il n'est pas plus difficile que SAT.

Une réduction se vérifie dans les deux sens

Une traduction correcte doit garantir que l'instance produite est satisfiable si et seulement si l'instance de départ l'était.
Le sens « si l'original a une solution, la traduction en a une » se vérifie en construisant la solution traduite. Le sens inverse, « si la traduction a une solution, l'original en a une », est celui qu'on oublie, et c'est pourtant lui qui interdit à la traduction d'inventer des solutions qui n'existent pas.
Le chapitre 3 en a donné l'exemple concret : une modélisation à laquelle il manque une contrainte est une réduction fausse dans ce sens-là, et le solveur rend alors une solution parfaitement valide pour la formule et absurde pour le problème.

3-SAT

k

-SAT

$k$ -SAT est SAT restreint aux formules dont chaque clause compte exactement $k$ littéraux.

3-SAT est encore NP-complet, et c'est le format d'entrée des résultats théoriques. La réduction depuis SAT est courte et instructive.

Ramener une clause quelconque à des clauses de taille 3

Clause de 1 ou 2 littéraux. On la complète avec des variables fraîches. La clause $(a)$ devient $(a \vee p \vee q) \wedge (a \vee p \vee \neg q) \wedge (a \vee \neg p \vee q) \wedge (a \vee \neg p \vee \neg q)$ , qui force $a$ quelles que soient $p$ et $q$ .

Clause de plus de 3 littéraux. On la coupe en chaîne. La clause $(a_1 \vee a_2 \vee a_3 \vee a_4 \vee a_5)$ devient

$(a_1 \vee a_2 \vee y_1) \wedge (\neg y_1 \vee a_3 \vee y_2) \wedge (\neg y_2 \vee a_4 \vee a_5)$

Les $y_i$ jouent le rôle de « la clause n'est pas encore satisfaite, on continue ». Une clause de $k$ littéraux donne $k - 2$ clauses et $k - 3$ variables fraîches : la transformation est linéaire.

Le cas qui réussit. Si $a_3$ est vrai, la clause du milieu est satisfaite par lui. Il reste à régler les $y$ pour les deux autres : $y_1 = 1$ satisfait la première, $y_2 = 0$ satisfait la troisième. Il existe donc bien un réglage des variables fraîches, et c'est le sens de vérification qu'on oublie.

3 clausesunitaireen attente

c1(a1∨a2∨y1)⇒ y1 = 1
c2(¬y1∨a3∨y2)
c3(¬y2∨a4∨a5)⇒ y2 = 0

a1a2y1a3y2a4a5

vert = décidé, orange = déduit par propagation.

Propagation unitaire : y1 = 1, y2 = 0. Ces valeurs ne sont pas des choix, elles sont imposées.

La chaîne obtenue à partir de (a1 ∨ … ∨ a5). Avec tous les a à 0, la première clause impose y1 = 1, ce qui rend la deuxième unitaire et impose y2 = 1, ce qui falsifie la troisième. Propager pas à pas fait voir l'échec se transmettre exactement comme dans la clause d'origine. Remettre a3 à 1, puis propager, montre l'autre sens.

La frontière est entre 2 et 3

k

-SAT est NP-complet pour tout

k \geq 3

. Pour

k = 2

, le problème devient résoluble en temps linéaire.
Un littéral de plus par clause fait donc passer du temps linéaire au NP-complet. C'est l'un des sauts les plus nets de toute la théorie de la complexité, et le chapitre suivant est consacré à ce qui se trouve du bon côté de cette frontière.

Une conjecture qui précise la difficulté

La NP-complétude dit qu'on ne sait pas résoudre 3-SAT en temps polynomial. Elle n'interdit pas, en soi, un algorithme en

2^{\sqrt{n}}

, qui serait exponentiel et pourtant très utilisable.
L'hypothèse du temps exponentiel comble ce vide : elle affirme qu'il n'existe aucun algorithme pour 3-SAT en temps

2^{o(n)}

, autrement dit que l'exposant reste proportionnel au nombre de variables. Ce n'est pas un théorème, c'est une conjecture, plus forte que

P \neq NP

.
Elle a un intérêt pratique : elle explique pourquoi les meilleurs algorithmes connus se battent pour faire descendre la base, de

2^n

vers

1{,}31^n

, et non pour changer la forme de l'exposant. Personne ne cherche le miracle, tout le monde grignote la constante.

La transition de phase

Sur des instances 3-SAT tirées au hasard, avec $n$ variables et $m$ clauses, le comportement dépend presque uniquement du rapport $\alpha = m / n$ .

f(x) = 1 / (1 + exp(6 * (x - 4.26)))g(x) = exp(0 - (x - 4.26) * (x - 4.26) * 1.6)

La transition de phase du 3-SAT aléatoire. La courbe descendante est la proportion d'instances satisfiables, qui passe de presque 1 à presque 0 autour de α = 4,26. La cloche est le coût de résolution, maximal exactement au même endroit.

Les trois régimes, et pourquoi ils diffèrent

$\alpha$ petit, sous 4. Peu de clauses pour beaucoup de variables : les solutions abondent, et un solveur en trouve une presque sans revenir en arrière. Satisfiable et facile.

$\alpha$ grand, au-dessus de 5. Tant de clauses que la contradiction apparaît vite : quelques décisions suffisent à falsifier une clause, et la réfutation est courte. Insatisfiable et facile.

$\alpha$ voisin de 4,26. Les solutions sont rares mais pas absentes, et rien ne se décide localement. Le solveur doit explorer. Difficile, dans les deux réponses.

La reproduire soi-même

Le code ci-dessous tire des instances 3-SAT au hasard à différents rapports et les résout avec un solveur minuscule, dont le chapitre 7 expliquera le fonctionnement. Il n'y a rien à croire sur parole : la courbe apparaît.

main.py

Sortie

>_ Prêt à exécuter…

Deux choses à observer, et une à modifier

La descente est franche. Entre

\alpha = 3

\alpha = 6

, la proportion passe de 100 % à quelques pour cent. Le basculement est bien là où la figure l'annonçait.
Elle n'est ni verticale ni exactement à 4,26. Avec 18 variables, la moitié des instances sont encore satisfiables vers

\alpha = 4{,}6

, et la pente est douce. C'est un effet de petite taille : à

n

fini, le seuil est décalé vers le haut et la marche est arrondie. Elle ne devient une vraie discontinuité, exactement en 4,26, qu'à la limite des grands

n

.
À essayer. Remplacer N = 18 par N = 30 et relancer. Deux choses bougent ensemble : la marche se redresse, elle est encore à 100 % en 3,5 et tombe à 2 % en 6, et son milieu se rapproche de 4,3. Le temps de calcul, lui, est multiplié par cinq au voisinage du seuil : c'est la cloche de la figure précédente, mesurée au lieu d'être dessinée.

Ce que la transition de phase ne dit pas

Elle décrit des instances aléatoires uniformes, et rien d'autre. Les instances industrielles, celles qui viennent de la vérification de circuits ou de la planification, ont un rapport

\alpha

qui les placerait en plein pic de difficulté, et se résolvent pourtant en quelques secondes sur des millions de variables.
La raison est qu'elles ne sont pas aléatoires. C'est l'objet de la fin du chapitre.

Difficile en théorie, résolu en pratique

La NP-complétude est une garantie sur le pire cas

Elle dit qu'il existe des familles d'instances sur lesquelles tout algorithme connu explose. Elle ne dit rien de l'instance qu'on a devant soi.
Un solveur moderne traite quotidiennement des formules de plusieurs millions de variables issues de la vérification matérielle. La même machine échoue sur

\mathrm{PHP}_{14}

, le principe des tiroirs à 14 casiers, qui en compte 210.
La taille n'est donc pas le bon indicateur.

Ce que « structure » veut dire

Le mot revient constamment et reste vague tant qu'on ne lui donne pas de contenu. En voici un, précis et mesurable.

Porte dérobée

Un ensemble $S$ de variables est une porte dérobée si, une fois les variables de $S$ affectées, la propagation unitaire seule suffit à conclure sur toutes les autres.

La formule ci-dessous ne contient aucune clause unitaire : la propagation ne peut rien faire tant qu'aucune décision n'a été prise. Il suffit pourtant de décider une seule variable sur cinq pour que tout le reste tombe.

5 clausesen attente

c1(x∨y)
c2(¬x∨z)
c3(¬z∨w)
c4(¬y∨w)
c5(¬w∨u)

xyzwu

vert = décidé, orange = déduit par propagation.

Aucune variable n'est affectée : toutes les clauses attendent.

Aucune clause n'est unitaire au départ, et les boutons de propagation restent inertes. Poser x = 1, puis propager jusqu'au bout, décide z, w et u sans aucun autre choix. L'ensemble {x} est une porte dérobée de taille 1.

Pourquoi cette notion explique l'écart

Si une instance possède une porte dérobée de taille

k

, un solveur qui tombe sur les bonnes variables la résout en explorant au plus

2^k

possibilités, quelle que soit la taille totale de la formule.
Les instances industrielles en ont de très petites : quelques dizaines de variables sur des centaines de milliers. Elles décrivent des systèmes réels, où presque tout est déterminé par un petit nombre d'entrées, le reste n'étant que du calcul.
Les instances aléatoires au seuil n'en ont aucune de petite. Aucun sous-ensemble restreint ne commande les autres, parce que rien dans leur construction n'a créé de dépendances privilégiées.
Voilà l'écart entre trois millions de variables résolues en dix secondes et deux cents qui résistent une heure : ce n'est pas la taille, c'est le nombre de variables qui décident vraiment.

La bonne mesure reste introuvable

Les portes dérobées ne sont qu'une des explications proposées. On invoque aussi la largeur arborescente du graphe des variables, la présence de communautés de variables fortement liées entre elles et faiblement au reste, ou l'hétérogénéité des degrés.
Aucune de ces mesures ne prédit de façon fiable le temps de résolution, et toutes coûtent parfois plus cher à calculer que la résolution elle-même. Le seul moyen honnête de savoir si une instance passe reste de lancer le solveur, avec une limite de temps.

Ce que cela change dans la conduite d'un projet

Puisque aucune mesure ne prédit, la seule attitude raisonnable est expérimentale, et elle a trois règles.
Toujours poser une limite de temps. Un solveur sans limite ne rend jamais la main, et l'absence de réponse au bout d'une heure est déjà une information.
Mesurer sur des instances représentatives, pas sur la plus petite ni sur la plus grosse. Le comportement n'est pas monotone en la taille.
Changer d'encodage avant de changer de solveur. Un gain d'un facteur mille vient bien plus souvent d'une modélisation revue que d'un réglage de solveur, et le chapitre 3 a montré pourquoi.

Exercices type

Combien de clauses produit la mise en 3-SAT d'une clause de 8 littéraux ?

Par la construction en chaîne : $k - 2 = 6$ clauses, et $k - 3 = 5$ variables fraîches.

Sur une formule entière, la transformation est donc linéaire en la somme des tailles de clauses, c'est-à-dire en le nombre total de littéraux. Une formule de $10^6$ littéraux reste de l'ordre de $10^6$ clauses après réduction.

C'est ce qui rend la réduction utilisable en théorie et en pratique, contrairement à beaucoup de réductions de la NP-complétude qui sont polynomiales mais de degré prohibitif.

On sait réduire le problème de la clique à SAT. Qu'a-t-on démontré ?

On a démontré que la clique n'est pas plus difficile que SAT, et rien d'autre. En pratique, cela donne un moyen de résoudre la clique : traduire, puis lancer un solveur.

Ce que l'on n'a pas démontré, c'est que la clique est difficile. Pour cela il faudrait la réduction inverse, de SAT vers la clique, qui montrerait que la clique est au moins aussi difficile que SAT.

C'est exactement le piège du sens de lecture. La phrase « j'ai réduit mon problème à SAT, donc il est NP-difficile » est fausse : n'importe quel problème facile se réduit lui aussi à SAT.

Un solveur rend UNSAT sur une instance de 40 variables après une heure, et SAT sur une instance de 2 millions de variables en 5 secondes. Que peut-on en conclure sur les deux instances ?

Rien qui concerne leur taille. L'instance de 40 variables a probablement une structure hostile : aucune porte dérobée petite, beaucoup de symétries, ou une réfutation dont on sait qu'elle est exponentiellement longue, comme le principe des tiroirs.

L'instance de 2 millions décrit sans doute un système réel, où quelques dizaines de variables d'entrée déterminent tout le reste par propagation. Le solveur ne parie que sur ces quelques dizaines.

La bonne question à poser sur la petite instance n'est donc pas « comment accélérer le solveur » mais « d'où vient cette structure ». Les symétries se cassent, un encodage se change, et c'est de là que viennent les gains.

Pourquoi les meilleurs algorithmes pour 3-SAT visent-ils

1{,}31^n

plutôt que

2^{\sqrt{n}}

Parce que l'hypothèse du temps exponentiel affirme qu'aucun algorithme en $2^{o(n)}$ n'existe pour 3-SAT. Un algorithme en $2^{\sqrt{n}}$ en serait un, puisque $\sqrt{n}$ croît moins vite que $n$ .

Ce n'est pas un théorème, mais la conjecture est prise très au sérieux : de nombreux résultats de complexité fine s'en déduisent, et aucun indice ne la contredit.

Le travail se concentre donc sur la base de l'exponentielle. Passer de $2^n$ à $1{,}31^n$ change tout en pratique : pour $n = 100$ , le rapport est de l'ordre de $10^{18}$ . C'est une amélioration considérable qui laisse pourtant le problème exponentiel.

Une réponse « oui » à SAT se certifie facilement. Que serait un certificat pour « non » ?

Il faudrait convaincre qu'aucune des $2^n$ affectations ne convient, sans les parcourir.

La réponse pratique est une preuve de réfutation : une suite de déductions, chacune tirée des précédentes, aboutissant à une contradiction manifeste. Le chapitre 6 en donne le mécanisme, la résolution, et les solveurs modernes savent produire de telles preuves dans un format vérifiable par un programme indépendant.

La réponse théorique est ouverte. Savoir si toute instance insatisfiable admet une preuve de taille polynomiale équivaut à $NP = \text{co-}NP$ , un problème non résolu. Et l'on sait déjà que pour la résolution seule, la réponse est non : certaines familles exigent des preuves de taille exponentielle.

Vérification rapideon peut se reprendre

1.Réduire un problème A à SAT prouve que…

2.Une instance de 3 millions de variables se résout en 10 secondes, une autre de 200 variables résiste une heure. Est-ce contradictoire avec la NP-complétude ?

3.Le rapport clauses sur variables d'une instance 3-SAT aléatoire vaut 8. À quoi s'attendre ?

4.Un collègue affirme : « cette instance a un rapport m/n de 4,3, elle sera donc très difficile ». Que répondre ?

5.Vérifier qu'une affectation satisfait une formule d'un million de clauses coûte…

La méthode

Séparer vérifier et trouver avant toute discussion de difficulté : ce sont deux problèmes distincts.
Fixer le sens d'une réduction en écrivant laquelle des deux instances est traduite en l'autre.
Vérifier une réduction dans les deux sens, en particulier celui où la traduction pourrait inventer des solutions.
Ne pas conclure de la taille à la difficulté : chercher plutôt le petit ensemble de variables qui commande les autres.
Situer une instance aléatoire par son rapport $m/n$ , et se souvenir que ce critère ne vaut que pour l'aléatoire.
Poser une limite de temps à toute exécution, et traiter l'absence de réponse comme une information.
Revoir l'encodage avant de changer de solveur quand une instance résiste.

Synthèse

NP est la classe des problèmes dont une réponse « oui » se vérifie vite, pas se trouve vite.
Un certificat est la preuve qu'on donne à vérifier : pour SAT, une affectation, contrôlable en un parcours.
Une réponse non n'a pas de certificat évident : c'est la question de co-NP, et elle est ouverte.
Cook-Levin : SAT est NP-complet, tout problème de NP s'y ramène. Exécuter un programme, c'est satisfaire une formule.
SAT joue le rôle d'un langage d'assemblage pour les problèmes combinatoires.
Une réduction $A \leq_p B$ transporte la facilité vers le bas et la difficulté vers le haut : le sens compte.
$k$ -SAT est NP-complet dès $k = 3$  ; la réduction depuis SAT est linéaire.
L'hypothèse du temps exponentiel interdit tout algorithme en $2^{o(n)}$  : on grignote la base, pas l'exposant.
La transition de phase du 3-SAT aléatoire est en $\alpha \approx 4{,}26$ , et ne concerne que l'aléatoire.
Une porte dérobée est un petit ensemble de variables dont l'affectation laisse la propagation finir seule.
La NP-complétude porte sur le pire cas ; elle ne prédit rien sur une instance donnée.

Ce que « difficile » veut dire

Ce que ce chapitre apporte

Vérifier n'est pas trouver

Le théorème de Cook-Levin

Ce qu'est une réduction, et dans quel sens elle va

3-SAT

La transition de phase

La reproduire soi-même

Difficile en théorie, résolu en pratique

Ce que « structure » veut dire

Exercices type

La méthode

Synthèse

Ce que « difficile » veut dire

Ce que ce chapitre apporte

Vérifier n'est pas trouver

Le théorème de Cook-Levin

Ce qu'est une réduction, et dans quel sens elle va

3-SAT

La transition de phase

La reproduire soi-même

Difficile en théorie, résolu en pratique

Ce que « structure » veut dire

Exercices type

La méthode

Synthèse

Ce que « structure » veut dire