Sur l'île au trésor, il y a trois habitants :Alice, Bob et Carole. En bon chasseur de trésor, vous essayez de savoir où creuser. Mais vous n'avez pas le temps de mener un long interrogatoire sur chacun des habitants et vous avez besoin de savoir qui sait où est le trésor. Vous savez pour l'instant que :
En notant les propositions suivantes
| Texte français | Formule propositionnelle |
|---|---|
| Alice connaît l'emplacement du trésor | a |
| Bob connaît l'emplacement du trésor | b |
| Carole connaît l'emplacement du trésor | c |
| Alice ignore l'emplacement du trésor | ¬a |
| Bob ignore l'emplacement du trésor | ¬b |
| Carole ignore l'emplacement du trésor | ¬c |
Alors les quatre propositions de l'énoncé s'écrivent
a ∨ b, ¬b ∨ ¬c,
¬a ∨ c et a ∨ c.
Comme chacune d'entre elles ne fait intervenir que
deux variables propositionnelles, résoudre ce problème
fait partie de la classe 2-SAT.
Il s'agit d'un problème de satisfiabilité car on
veut savoir s'il existe une valuation des variables
propositionnelles a, b et c qui satisfasse la formule
(a ∨ b) ∧ (¬b ∨ ¬c) ∧ (¬a ∨ c) ∧ (a ∨ c).
Autrement dit, cette formule a-t-elle un modèle ?
En 1921, Emil Post propose un algorithme pour résoudre les problèmes SAT : on met dans un tableau les valuations possibles ⊥ et ⊤ des variables a, b et c et on calcule les valeurs de la formule φ pour chacune de ces valuations. Avec 3 variables cela fait 23=8 lignes dans le tableau de Post
| a | b | c | ¬a | ¬b | ¬c | a ∨ b | ¬b ∨ ¬c | ¬a ∨ c | a ∨ c | φ |
|---|---|---|---|---|---|---|---|---|---|---|
| ⊥ | ⊥ | ⊥ | ⊤ | ⊤ | ⊤ | ⊥ | ⊤ | ⊤ | ⊥ | ⊥ |
| ⊥ | ⊥ | ⊤ | ⊤ | ⊤ | ⊥ | ⊥ | ⊤ | ⊤ | ⊤ | ⊥ |
| ⊥ | ⊤ | ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊤ | ⊤ | ⊥ | ⊥ |
| ⊥ | ⊤ | ⊤ | ⊤ | ⊥ | ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊥ |
| ⊤ | ⊥ | ⊥ | ⊥ | ⊤ | ⊤ | ⊤ | ⊤ | ⊥ | ⊤ | ⊥ |
| ⊤ | ⊥ | ⊤ | ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊤ | ⊤ | ⊤ |
| ⊤ | ⊤ | ⊥ | ⊥ | ⊥ | ⊤ | ⊤ | ⊤ | ⊥ | ⊤ | ⊥ |
| ⊤ | ⊤ | ⊤ | ⊥ | ⊥ | ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊥ |
Il n'y a qu'une seule ligne (en gras) où la colonne de φ comporte ⊤, mais il y en a une : si φ n'est pas valide, elle est tout de même satisfaite par la valuation (⊤,⊥,⊤). On note
ou
Comme pour n variables propositionnelles, il y a 2n lignes dans le tableau, l'algorithme de Post est de complexité exponentielle.
L'algorithme de Quine-McCluskey consiste à construire un arbre de déduction, avec un embranchement pour chaque variable (qui peut prendre les valeurs ⊥ et ⊤ ce qui fait que l'arbre est binaire). Par exemple,
En convenant d'aller vers la gauche si a=⊥ et vers la droite si a=⊤, on obtient l'arbre suivant, dans lequel on a des expressions plus faciles à évaluer :
À gauche on a ⊥ indépendamment des valeurs de vérité de b et c, donc on n'a aucune chance de trouver un modèle de φ à gauche. Mais à droite on crée une nouvelle bifurcation selon que b=⊥ (à gauche) ou b=⊤ (à droite).
Pour compléter l'arbre binaire, il reste à faire la même chose pour c : bifurquer selon que c=⊥ (à gauche) ou c=⊤ (à droite) :
Une fois cet arbre calculé, on peut savoir si φ est valide (pour cela il faut et il suffit que toutes les feuilles soient ⊤, ce qui n'est pas le cas ici) et on peut savoir aussi si φ est satisfiable : pour cela il suffit qu'une des feuilles soit ⊤. C'est le cas ici :
On voit ici non seulement que φ est satisfiable (la feuille verte) mais aussi pour quelle valuation. Pour aller à la feuille, on va successivement
La déduction naturelle sert à prouver non seulement la satisfiabilité d'une formule, mais sa validité. On a vu dans le (2) que la formule φ n'est pas valide (par exemple elle est invalidée si Alice, Bob et Carole connaissent tous les trois l'emplacement du trésor). Mais montrer qu'une formule est satisfiable, c'est montrer que sa négation est invalide.
Aller sur ce site et y coller le texte suivant :
((a or b) and (a or c) and ((not a) or c) and ((not b) or (not c)))
puis cliquer sur « check for satifiability » pour voir le résultat.
Les termes de φ sont des disjonctions. On peut les transformer en implications :
| Disjonction | Implication | Contraposée |
|---|---|---|
a ∨ b | ¬a → b | ¬b → a |
¬b ∨ ¬c | b → ¬c | c → ¬b |
¬a ∨ c | a → c | ¬c → ¬a |
a ∨ c | ¬a → c | ¬c → a |
Cette relation d'ordre partiel peut être représentée par un graphe orienté appelé graphe d'implication :
Ce graphe a deux composantes fortement connexes :
On constate que
Or un problème 2-SAT admet une solution si et seulement si le graphe d'implication est tel qu'aucune variable n'est dans la même composante connexe que sa négation.
Cela prouve que le problème ci-dessus a une solution.
On aimerait savoir s'il est possible de colorier ce graphe avec seulement deux couleurs, de manière que deux sommets adjacents ne soient jamais de la même couleur :
Pour dire que le sommet a est rouge, on note r(a). Pour dire que le sommet a est bleu, on note ¬r(a). Comme il n'y a que deux couleurs, on n'a besoin que du prédicat r (signifiant rouge).
Si a est rouge alors ni b ni c ne le sont, puisqu'ils sont adjacents à a. Et si a n'est pas rouge alors c'est qu'il est bleu et dans ce cas b et c sont rouges. Ce qui donne ce graphe d'implication :
Comme ce graphe est fortement connexe, on en déduit que le problème 2-SAT de la bicoloration du graphe à 3 sommets n'a pas de solution.
En fait il y a un algorithme encore plus rapide pour savoir si un graphe est bipartite (c'est-à-dire colorable en deux couleurs seulement) : il suffit d'effectuer un parcours en profondeur, à partir de a par exemple, et de colorier alternativement les sommets rencontrés en rouge et en bleu :
Une fois le graphe parcouru
Ce qui prouve que le graphe ne peut être bicolorié.
Par contre, le graphe cycle d'ordre 4 est bipartite :
On s'en rend compte aisément en parcourant le graphe en profondeur, mais aussi avec le graphe d'implication :
Le graphe a deux composantes fortement connexes (correspondant à deux manières de colorier, l'une avec a et c en rouge, l'autre avec b et d en rouge). Aucune de ces composantes fortement connexe ne comportant une proposition et sa négation, le graphe est bicoloriable.
En allant sur cette page, et en choisissant la conversion d'une 3-coloration d'un graphe vers 3-SAT, le graphe précédent, codé
({vertices: [1, 2, 3],
edges: [[1, 2], [1, 3], [2, 3]]})
et le problème 3-SAT obtenu est
((1 in red) or (1 in blue) or (1 in yellow)) ((2 in red) or (2 in blue) or (2 in yellow)) ((3 in red) or (3 in blue) or (3 in yellow)) ((not (1 in red)) or (not (1 in blue))) ((not (1 in red)) or (not (1 in yellow))) ((not (1 in blue)) or (not (1 in red))) ((not (1 in blue)) or (not (1 in yellow))) ((not (1 in yellow)) or (not (1 in red))) ((not (1 in yellow)) or (not (1 in blue))) ((not (2 in red)) or (not (2 in blue))) ((not (2 in red)) or (not (2 in yellow))) ((not (2 in blue)) or (not (2 in red))) ((not (2 in blue)) or (not (2 in yellow))) ((not (2 in yellow)) or (not (2 in red))) ((not (2 in yellow)) or (not (2 in blue))) ((not (3 in red)) or (not (3 in blue))) ((not (3 in red)) or (not (3 in yellow))) ((not (3 in blue)) or (not (3 in red))) ((not (3 in blue)) or (not (3 in yellow))) ((not (3 in yellow)) or (not (3 in red))) ((not (3 in yellow)) or (not (3 in blue))) ((not (1 in red)) or (not (2 in red))) ((not (1 in red)) or (not (3 in red))) ((not (2 in red)) or (not (3 in red))) ((not (1 in blue)) or (not (2 in blue))) ((not (1 in blue)) or (not (3 in blue))) ((not (2 in blue)) or (not (3 in blue))) ((not (1 in yellow)) or (not (2 in yellow))) ((not (1 in yellow)) or (not (3 in yellow))) ((not (2 in yellow)) or (not (3 in yellow)))
En soumettant ce problème 3-SAT à cette autre page et en cliquant sur « check for satisfiability » on obtient la confirmation que le problème a bien une solution :
(1 in blue) (2 in yellow) (3 in red)