L'informatique et les mathématiques appliqués à la logique et au langage.
Dans tout l'article je tente de vulgariser le sujet traité. Je dois alors trouver un compromis entre pédagogie et rigueur, qui permette à la fois de vulgariser le sujet et à la fois de conserver son essence. N'hésitez pas à me contacter si vous penser trouver une coquille, ou si vous n'adhérez pas à ma méthode.
Le problème SAT (pour SATisfiabilité) est un problème du calcul propositionnel. On peut le résumer ainsi : étant donné une formule du calcul propositionnel existe-t-il une façon d'associer des valeurs de vérité aux variables de la formule pour que celle-ci soit évaluée comme vraie.
Conceptuellement, le problème SAT représente un problème de vérification des propriétés d'un modèle (dans le sens informel et abstrait) en fonction de contraintes qu'on lui impose. Par exemple, si l'on souhaite trouver une façon d'organiser chronologiquement les passages en entretient de nombreux candidats pour un poste, en ne disposant que d'un nombre réduit d'examinateurs, on peut se ramener à la résolution d'un problème SAT associé.
En fait, on pourra s'intéresser à la coloration de graphes pour résoudre ce problème.
Dans les exemples, on note $V$ la valeur booléenne vraie et $F$ la valeur
booléenne fausse.
On appelle valuation une fonction $\sigma$ qui a un ensemble de variables
propositionnelles associe ou bien $V$, ou bien $F$. Pour toute formule $P$
du calcul propositionnel, on note alors $[\![P]\!]_{\sigma}$ l'évaluation
de $P$ en fonction de la valuation $\sigma$ : c'est la valeur booléenne associée
à une formule en fonction d'une valuation donnée.
Enfin, on note $\lor$ le symbole correspondant au ou logique et $\land$
celui correspondant au et logique.
Considérons la formule suivante : $P = (a \lor \neg b \lor c) \land (\neg a \lor \neg c)$. Pour chaque variable présente dans la formule donnée, déterminons la valeur booléenne à lui associer pour que la $P$ soit évaluée comme vraie. On remarque que lorsque l'on choisit $a := V$, $b := V$ et $c := F$ on a bien $P$ évaluée en $V$. On peut donc définir la valuation $\sigma$ qui satisfait $F$ par : \[ \sigma(a) = V, \quad \sigma(b) = V, \quad \sigma(c) = F \] et on obtient alors $[\![P]\!]_{\sigma} = V$.
On peut montrer avec un contre exemple que la valuation trouvée n'est pas toujours unique. En effet, la plupart du temps, on peut en déterminer plusieurs qui satisfont la formule donnée.
Dans l'exemple donné, la formule $P$ est sous forme normale conjonctive. Cela signifie qu'elle est sous forme de conjonctions de disjonctions. Autrement dit, c'est une suite de et logique sur des sous-formules qui sont des suites de ou logiques entre des variables, ou leur négation : \[ (l_1 \lor l_2 \lor ... \lor l_n) \land (l_1 \lor l_2 \lor ... \lor l_p) \land (l_1 \lor l_2 \lor ... \lor l_m) \] Dans cet article, on s'intéresse à la résolution du problème SAT pour les formules de cette forme. À priori, nous pourrions penser que cette contrainte sur la forme d'une formule réduit le champs d'action de l'algorithme, mais en réalité, nous pouvons démontrer toute formule du calcul propositionnel peut être écrite sous forme normale conjonctive.
Dans une formule sous FNC, on peut déterminer le nombre maximal de variables utilisées dans ses sous-formules. En notant ce nombre $p$, on dit alors que l'on résout un problème p-SAT.
Lorsque $p = 1$, pour déterminer $\sigma$, on associe à chaque variable (ou sa négation) une valeur booléenne qui la rend vraie. Le temps de résolution du problème (la complexité temporelle) avec cette méthode est de l'ordre du nombre de variables dans la formule.
Lorsque $p = 2$, les choses se compliquent un peu lorsque l'on souhaite obtenir encore une fois une complexité temporelle en temps linéaire au nombre de variables, car cela implique l'utilisation de théories qui n'ont à priori pas de rapport avec le problème (la théorie des graphes). Sans entrer dans les détails, pour déterminer $\sigma$, on construit un graphe d'implication puis on le manipule en s'intéressant à ses composantes fortement connexes. Plus précisément, on se ramène à la résolution d'un problème de théorie des graphes pour résoudre le problème 2-SAT.
De manière formelle, on dit que le problème 2-SAT peut être réduit calculatoirement au problème de recherche de composantes fortement connexes dans un graphe orienté.
Lorsque $p = 3$, on se ramène là aussi à un problème de théorie des graphes, mais cette fois-ci, au lieu d'essayer de déterminer les composantes fortement connexes d'un graphe d'implication et d'en déduire une valuation qui satasfait une formelle donnée, on tente de colorier un graphe avec trois couleurs différentes en respectant certaines contraintes. L'analogie entre la formule et le graphe se fait au travers d'un outil qui modélise le ou logique par un graphe avec des couleurs, on l'appelle gadget.
De manière formelle, on dit que le problème 3-SAT peut être réduit calculatoirement au problème 3-COLOR.
L'algorithme de Quine-McCluskey permet de résoudre le problème k-SAT en se basant sur le principe de retour sur trace En voici le principe général.
En considérant une formule $P$ sous FNC et une valuation partielle $\sigma$, pour chaque variable $x$ dans la formule, tant que l'évaluation de $P$ avec $\sigma$ n'est pas $V$
En fait, cette méthode revient à tester chaque valuation possible au fur et à mesure de l'exécution, jusqu'à tomber sur celle qui satisfait $P$. Dans l'idée, on pourrait donc construire l'arbre représentant l'ensemble des valuations testées pour le comparer à l'arbre de l'ensemble des valuations possibles, et on remarquerait que le premier correspond au parcours en profondeur partiel du second.
Dans la présentation du principe général, je fais mention de deux étapes fondamentales
dans la résolution de l'algorithme : la substitution et la simplification.
La substitution de $x$ avec une valeur booléenne $b$ signifie que l'on remplace
dans la formule $P$ chaque occurence de $x$ par $P$. La simplification consiste
à évaluer la formule issue de la substitution puis à la transformer (réduire sa taille) en fonction
de $b$.
Considérons par exemple la formule sous FNC suivante : $P = (a \lor \neg b) \land (\neg a \lor \neg b)$. Substituons $a$ par $V$. On a alors $P = (V \lor \neg b) \land (F \lor \neg b)$. On peut alors simplifier (ie. transformer) $P$ de la manière suivante, en utilisant les règles de la logique : \begin{align} P & = (V \lor \neg b) \land (F \lor \neg b) \\ & = V \land \neg b \\ & = \neg b \end{align}
Lorsque l'on substitue une variable $x$ quelconque de $P$ par une valeur $b$, on peut simplifier $P$ en suivant les règles suivantes, en se basant sur les propriétés du ou logique :
Dans le pire des cas, il n'existe aucune valuation qui satisfait la formule
$P$. On dit que $P$ est une antilogie.
On remarque alors que cette fois ci, l'arbre issu de la recherche d'une valuation
correspond exactement à l'arbre de l'ensemble des valuations possibles.
Pour construire cet arbre, il a fallu tester $2^p - 1$ valuations (c'est le nombre de noeuds dans l'arbre), avec $p$
qui désigne le nombre de variables dans $P$. On en déduit que le temps d'exécution de l'algorithme
est exponentiel et pour une formule contenant plusieurs dizaines de
variables distinctes, il est probable que son exécution sur un ordinateur
classique dure plusieurs centaines d'années...
Cette liste de références n'est malheureusement pas exhaustive, si vous vous intéressez au sujet traité, je vous conseille fortement de vous renseigner via d'autres ressources et de vérifier la validité du contenu utilisé.
L'algorithme de Quine-McCluskey