Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter
Support de cours · chapitre 4
Modéliser et résoudre : SAT et énigmes
Traduire un problème en formules, se demander si elles sont cohérentes et ce qu'elles impliquent, et laisser un algorithme chercher la réponse.
Modéliser
La démarche
Modéliser, c'est traduire un énoncé en français en un ensemble de formules $\Sigma$, puis poser les questions du chapitre 2 :
- les faits sont-ils cohérents ? C'est demander si $\Sigma$ est satisfiable ;
- une affirmation $A$ découle-t-elle des faits ? C'est demander si $\Sigma \vDash A$, c'est-à-dire si $\Sigma \cup \{\lnot A\}$ est insatisfiable ;
- que sait-on exactement ? Ce sont les modèles de $\Sigma$.
La première étape est de choisir les variables : une par fait élémentaire, qui peut être vrai ou faux indépendamment des autres. « Alice vient » est une variable $a$. « Alice et Bob viennent » n'en est pas une : c'est $a \land b$.
Traduire le français
Le français est plus riche, et plus ambigu, que la logique. Les tournures courantes :
| En français | En formule |
|---|---|
| $p$ et $q$ ; $p$ mais $q$ ; $p$, pourtant $q$ | $p \land q$ |
| $p$ ou $q$ (l'un, l'autre ou les deux) | $p \lor q$ |
| soit $p$, soit $q$ (pas les deux) | $p \oplus q$ |
| ni $p$ ni $q$ | $\lnot p \land \lnot q$ |
| si $p$ alors $q$ ; $q$ si $p$ ; $p$ suffit pour $q$ | $p \to q$ |
| $p$ seulement si $q$ ; $q$ est nécessaire pour $p$ | $p \to q$ |
| $p$ si et seulement si $q$ | $p \leftrightarrow q$ |
| $p$, sauf si $q$ ; $p$, à moins que $q$ | $\lnot q \to p$, soit $p \lor q$ |
Un exemple complet
On organise une soirée. Trois invités, Alice, Bob et Chloé, et trois contraintes :
- si Alice vient, Bob vient aussi ;
- Bob et Chloé ne viennent pas ensemble ;
- Chloé vient, à moins qu'Alice ne vienne.
Variables $a$, $b$, $c$ : « Alice (Bob, Chloé) vient ». Les faits :
Cohérence. On raisonne par cas sur $a$.
- $a = 1$ : la contrainte 1 impose $b = 1$, la 2 impose alors $c = 0$, et la 3 est satisfaite par $a$. Modèle : $a = 1, b = 1, c = 0$.
- $a = 0$ : la 3 impose $c = 1$, la 2 impose alors $b = 0$, et la 1 est satisfaite (antécédent faux). Modèle : $a = 0, b = 0, c = 1$.
$\Sigma$ est satisfiable, avec deux modèles : les faits sont cohérents, mais ils ne disent pas qui vient.
Conséquences. Une affirmation est conséquence de $\Sigma$ si elle est vraie dans les deux modèles. « Bob et Chloé ne viennent pas tous les deux » : oui, c'était une hypothèse. « Bob vient ou Chloé vient », $b \lor c$ : vrai dans les deux, donc $\Sigma \vDash b \lor c$. « Bob vient » : faux dans le second modèle, donc $\Sigma \not\vDash b$.
Faire résoudre par une machine
Le problème SAT
Décider si une formule en FNC est satisfiable s'appelle le problème SAT. C'est le premier problème dont on a montré qu'il est NP-complet (Cook, 1971) : on ne connaît pas d'algorithme qui le résolve toujours en temps polynomial, et en trouver un résoudrait d'un coup des milliers d'autres problèmes.
En pratique pourtant, les solveurs SAT traitent des formules de millions de variables. Ils servent à vérifier des circuits, planifier, ordonnancer, résoudre des sudokus, et choisir les versions compatibles des paquets d'une distribution logicielle. La démarche est toujours celle de ce chapitre : modéliser en FNC, puis donner la formule au solveur.
L'algorithme DPLL
Les solveurs modernes descendent tous d'un algorithme de 1962, DPLL (Davis, Putnam, Logemann, Loveland). Il travaille sur une FNC et alterne deux gestes.
- Propagation unitaire. Une clause réduite à un seul littéral force sa valeur. Si $\lnot s$ est une clause, $s$ doit valoir 0. On simplifie alors toutes les clauses : celles qui contiennent $\lnot s$ sont satisfaites et disparaissent ; dans les autres, le littéral $s$ est faux et disparaît. De nouvelles clauses unitaires peuvent apparaître : on recommence.
- Choix. Quand plus rien n'est forcé, on choisit une variable, on essaie une valeur, et l'on revient en arrière si l'on aboutit à une contradiction.
Si une clause devient vide (tous ses littéraux sont faux), la branche échoue. Si toutes les clauses sont satisfaites, on a trouvé un modèle.
Les énigmes des Purs et des Pires
Le logicien Raymond Smullyan a inventé une île où vivent deux sortes d'habitants : les Purs disent toujours la vérité, les Pires mentent toujours. On rencontre des habitants, ils parlent, on déduit qui est qui.
La modélisation tient en une règle. Soit $x$ la variable « $X$ est un Pur ». Si $X$ affirme $S$ :
- s'il est Pur, $S$ est vraie ;
- s'il est Pire, $S$ est fausse.
Dans les deux cas : $x \leftrightarrow S$.