Problème SAT

Un article de Wikipédia, l'encyclopédie libre.

Un problème SAT est un problème de décision visant à déterminer s'il existe une valuation d'un ensemble de variables booléennes telle qu'une formule propositionnelle donnée est alors logiquement vraie (En bref, c'est de savoir si une équation booléenne a une solution). Ce problème est très important en théorie de la complexité et a de nombreuses applications en planification classique, model checking, diagnostic, etc.

[modifier] Définition du problème SAT

Soit une formule logique sous forme normale conjonctive (ou CNF), c'est-à-dire une conjonction de disjonctions de littéraux, chaque littéral étant une variable booléenne ou sa négation. Ce CNF est satisfiable s'il est possible d'associer une valeur logique (booléenne) à chaque variable du CNF de telle manière que le CNF soit logiquement vrai. Déterminer si une formule est satisfiable est appelé problème de satisfiabilité ou problème SAT. Si la formule propositionnelle n'est pas sous forme CNF, il est nécessaire de la traduire pour que le problème soit qualifié de SAT. Généralement, la réponse à cette question fournit également un exemple d'assignement des variables tel que le CNF soit logiquement vrai.

Exemple : soit l'ensemble de variables $\{v_1,v_2,v_3\}\$ et $\phi = (v_1 \lor v_2) \land (\neg v_1 \lor v_3) \land (\neg v_2 \lor \neg v_1)$

$\phi\$ est satisfiable, puisque si on pose $v_1 = \mathit{vrai},\ v_2 = \mathit{faux},\ v_3 = \mathit{vrai}$ alors $\phi\$ est logiquement vrai.

En revanche, $\phi' = (v_1 \lor v_2) \land (\neg v_1 \lor v_3) \land (\neg v_2 \lor v_1) \land (\neg v_2 \lor v_3) \land (\neg v_1 \lor \neg v_3)$ n'est pas satisfiable !

[modifier] Complexité

SAT est un problème NP-complet d'après le théorème de Cook.

On obtient de même un problème NP-complet si on se restreint au problème 3SAT : étant donnée une formule logique de la forme $(a_1 \lor b_1 \lor c_1) \land \dots \land (a_m \lor b_m \lor c_m)$ , avec les $a i, b i, c i$ choisis dans un ensemble de $n$ variables et de leurs négations, déterminer si ce CNF est satisfiable est NP-complet.

Exemple : posons

n = 4

, les variables sont

{v 1, v 2, v 3, v 4}

Déterminer si l'expression $(v_1 \lor \neg v_2 \lor v_3) \land (\neg v_1 \lor v_3 \lor v_4)$ est satisfiable est un problème 3SAT.

Tout algorithme capable de résoudre un problème 3SAT (même le meilleur) peut dans certains cas devoir essayer un nombre de combinaisons d'assignements exponentiel en la valeur

n

[modifier] Algorithmes de SAT

La plus évidente des méthodes pour résoudre un problème SAT est de parcourir la table de vérité du problème, mais la complexité est alors exponentielle par rapport au nombre de variables.

[modifier] Méthode systématique

Pour prouver la satisfiabilité du CNF $\phi\$ , il suffit de choisir une variable $v$ et de prouver récursivement la satisfiabilité de $v \land \phi$ ou $\neg v \land \phi$ . La procédure est plus facile récursivement puisque $a \land \phi$ avec $a = v\$ ou $a = \neg v$ peut souvent se simplifier. L'appel récursif construit ainsi un arbre binaire de recherche.

Généralement, il existe à chaque nœud des clauses unitaires (le CNF est de la forme $\phi = a \land \phi'$ ), qui permettent de réduire fortement l'espace de recherche.

Exemple : considérons le CNF

$(v_1 \lor \neg v_2) \land \neg v_3 \land (v_3 \lor \neg v_1)$ .

La deuxième clause ( $\neg v_3$ ) est unitaire et permet d'obtenir immédiatement

v 3 = f a u x

. On peut remplacer les valeurs de

v 3

dans ce CNF, ce qui donne

$(v_1 \lor \neg v_2) \land \neg \textit{faux} \land (\textit{faux} \lor \neg v_1) = (v_1 \lor \neg v_2) \land \neg v_1$ .

À nouveau, on a une clause unitaire, et on obtient

v 1 = f a u x

. Puis, par propagation, on obtient

v 2 = f a u x

Dans cet exemple, on a trouvé les valeurs des trois variables sans même développer l'arbre de recherche. De manière générale, on peut réduire fortement l'espace de recherche. D'autre part, si une variable $v$ apparaît toujours positivement dans le CNF $\phi\$ , alors on peut poser $v = v r a i$ puisque $\phi\$ est satisfiable si et seulement si $\phi \land v$ est satisfiable (et de même si la variable apparaît négativement). Ainsi, dans l'exemple précédent, $v_2\$ n'apparaît que négativement et l'assignement $v 2 = f a u x$ peut être effectué. Remarquons que cet assignement permet d'accélérer la découverte d'une solution mais que des solutions pourraient exister en effectuant l'assignement contraire. L'algorithme DPLL (Davis, Putnam^[1], Davis, Logemann, Loveland^[2]) se base sur ces idées.

Le choix de la variable $v$ à développer est très important pour les performances des algorithmes SAT. On choisit généralement les variables qui apparaissent le plus souvent, si possible dans des clauses de taille 2.

[modifier] Apprentissage de clauses

Le principe de l'apprentissage de clauses est le suivant : lorsqu'un conflit apparaît lors de la recherche, c'est-à-dire lorsque un assignement partiel est démontré non cohérent avec l'ensemble des clauses, on peut isoler un sous-ensemble de ces assignements et un sous-ensemble de ces clauses, qui sont responsables du conflit (les assignements ne sont pas cohérents avec les clauses). À partir de ces assignements, il est possible de construire (d'apprendre) une clause qui est impliquée par les clauses. Cette nouvelle clause est ajoutée au CNF. Les assignements pertinents sont déterminés par un graphe de dépendance entre les clauses et les assignements. Les clauses apprises permettent de ne pas refaire plusieurs fois les mêmes erreurs dans l'arbre de recherche.

Exemple : Considérons que l'assignement

{v 1 = v r a i, v 2 = f a u x, v 3 = f a u x, v 4 = v r a i, v 5 = f a u x}

mène à un conflit. S'il est démontré que les variables

{v 1, v 4, v 5}

sont responsables de ce conflit, alors la clause $\neg v_1 \lor \neg v_4 \lor v_5$ est impliquée et il est possible de l'ajouter dans la liste des clauses. Si par la suite, la recherche conduit à l'assignement

{v 1 = v r a i, v 2 = v r a i, v 5 = f a u x, v 12 = f a u x}

, la variable

v 4

peut être immédiatement assignée à

v r a i

grâce à la clause apprise.

[modifier] Approches prospectives

L'approche prospective consiste à prospecter l'arbre de recherche pour découvrir des assignements certains. Ainsi, étant donné un CNF $\phi\$ , étant donnée une variable non instanciée $v\$ , on prospecte les CNFs $\phi \land v$ et $\phi \land \neg v$ . Si les deux CNFs conduisent à l'instanciation de la même variable $v'\$ avec la même valeur, alors l'instanciation peut se faire dès le CNF $\phi\$ .

Exemple : Considérons le CNF $\phi = (v_1 \lor v_2) \land (v_1 \lor \neg v_2 \lor v_3) \land (\neg v_1 \lor v_2 \lor v_4) \land (\neg v_3 \lor \neg v_4)$ . Nous nous intéressons ici à la variable $v_2\$ et prospectons la variable $v_1\$ .

Considérons l'assignement $v_1 = \textit{vrai}\$ , on obtient $(v_2 \lor v_4) \land (\neg v_3 \lor \neg v_4)$ et donc l'assignement $v_2 = \textit{vrai}\$ (puisque cette variable apparaît uniquement positivement).

Considérons l'assignement $v_1 = \textit{faux}\$ , on obtient $v_2 \land (\neg v_2 \lor v_3) \land (\neg v_3 \lor \neg v_4)$ et donc l'assignement $v_2 = \textit{vrai}\$ par clause unitaire.

Dans tous les cas, on obtient $v_2 = \textit{vrai}\$ et il est donc possible d'effectuer cet assignement dès le CNF $\phi\$ .

Rappelons que la complexité du problème SAT vient de la taille exponentielle de l'arbre de recherche par rapport au nombre de variables. La prospection permet de réduire fortement ce nombre de variables dès la racine (ou à n'importe quel nœud de l'arbre) avec une complexité supplémentaire relativement faible eu égard à la diminution de l'arbre de recherche.

[modifier] Recherche locale

Partant d'un assignement de toutes les variables, on cherche à modifier certaines valuations de façon à réduire le nombre de clauses non satisfaites. Cet algorithme souffre de plusieurs défauts : il peut tomber dans des minima locaux et il est incapable de prouver la non satisfiabilité, mais il s'avère très efficace dans les problèmes non structurés (c'est-à-dire souvent les problèmes générés aléatoirement). En cas d'échec après un temps long, il est possible de choisir un nouvel assignement aléatoire pour éviter les minima locaux.

[modifier] Principales implémentations

zChaff (Moskewicz, Madigan, Zhao, Zhang 2001)
Siege (Ryan 2003)
MiniSAT (Eén et Sörensson)

[modifier] Applications

Il est possible de traduire certains problèmes d'intelligence artificielle et d'utiliser les algorithmes SAT pour résoudre efficacement ces problèmes.

[modifier] Diagnostic

Le diagnostic de systèmes statiques consiste à déterminer si un système a un comportement défectueux étant donnée l'observation des entrées et sorties du système. Le modèle du système peut être traduit en un ensemble de contraintes (disjonctions) : pour chaque composant $c$ du système, une variable $A b (c)$ est créée qui est évaluée à vraie si le composant a un comportement anormal (Abnormal). Les observations peuvent être également traduites par un ensemble de disjonctions. L'assignement trouvé par l'algorithme de satisfiabilité est un diagnostic.

[modifier] Planification classique

Le problème de planification classique consiste à trouver une séquence d'actions menant d'un état du système à un ensemble d'états. Étant donnée une longueur maximale du plan $n$ et un ensemble $V$ de variables d'état booléennes permettant de décrire l'état du système, on crée les variables propositionelles $v i$ pour tout $i \in \{0,\dots,n\}$ et toute variable $v \in V$ . La variable $v i$ est vraie si la variable d'état est vraie après l'action numéro $i$ . On crée également les variables $a i$ pour tout $i \in \{1,\dots,n\}$ et toute action $a$ . La variable $a i$ est vraie si l'action numéro $i$ est $a$ . Il est alors possible de transformer le modèle du système en un ensemble de clauses. Par exemple, si l'action $a$ fait passer la variable $v 1$ à vrai lorsque celle-ci est fausse, alors le CNF contiendra une clause $(\neg v^0) \Rightarrow a^1 \Rightarrow v^1$ (ce qui est traduit par la clause $v^0 \lor \neg a_1 \lor v^1$ ). L'assignement trouvé par l'algorithme de satisfiabilité peut être immédiatement traduit en plan.

La planification classique par SAT est très efficace si on connaît la longueur $n$ du plan. Si cette valeur n'est pas connue, on peut chercher des plans pour une valeur incrémentale, ce qui est parfois coûteux (notamment parce que le CNF est non satisfiable jusqu'à $n - 1$ ).

[modifier] Model checking

Une approche semblable a été utilisée pour le model checking (vérification de propriétés d'un modèle). La principale différence est que le model checking s'applique à des trajectoires de longueur infinie contrairement à la planification. Cependant, si l'espace d'états du système est fini, toute trajectoire infinie boucle à un certain point et on peut borner la taille des trajectoires qu'il est nécessaire de vérifier. Le bounded model checking tire parti de cette propriété pour transformer le problème de model checking en un certain nombre de problèmes de satisfiabilité.

[modifier] Notes

↑ (en) Martin Davis et Hillary Putnam, « A Computing Procedure for Quantification Theory » , dans Communications of the ACM, 7, p. 201-215 (1960) [lire en ligne]
↑ (en) Martin Davis, George Logemann et Donald Loveland, « A machine Program for Theorem Proving », dans Communications of the ACM, 5, p. 394-397 (1962), [lire en ligne]

Récupérée de « http://fr.wikipedia.org../../../p/r/o/Probl%C3%A8me_SAT_5539.html »

Catégories : Algorithmique • Intelligence artificielle • Problème NP-complet