vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie.

Ce problème est important en théorie de la complexité. Il a été mis en lumière par le théorème de Cook-Levin, qui est à la base de la théorie de la NP-complétude et du problème P = NP. Le problème SAT a aussi de nombreuses applications notamment en satisfaction de contraintes, planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation : on se ramène à des formules propositionnelles et on utilise un solveur SAT.

Terminologie

Formules de la logique propositionnelle Les formules de la logique propositionnelle sont construites à partir de variables propositionnelles et des connecteurs booléens "et" (), "ou" (), "non" (). Une formule est satisfaisable. (on dit aussi satisfiable.) s'il existe une assignation des variables propositionnelles qui rend la formule logiquement vraie. Par exemple :

La formule est satisfaisable car si prend la valeur faux, la formule est évaluée à vrai. La formule n'est pas satisfaisable car aucune valeur de p ne peut rendre la formule vraie.

Clauses et forme normale conjonctives

Un littéral est une variable propositionnelle (littéral positif) ou la négation d'une variable propositionnelle (littéral négatif). Une clause est une disjonction de la forme où les sont des littéraux.

Une formule du calcul propositionnel est en forme normale conjonctive (ou forme clausale ou CNF sigle de l'anglais ) si elle est une conjonction de clauses.

Exemple Soit l'ensemble de variables et la formule . , et sont des clauses avec deux littéraux par clause. Leur conjonction est une forme normale conjonctive.

Si la formule propositionnelle n'est pas sous forme normale conjonctive, on peut la transformer en une forme normale conjonctive équivalente de taille au plus exponentielle en la formule initiale. On peut aussi la transformer en une forme normale conjonctive équisatisfiable de taille linéaire en la formule initiale.

Restrictions du problème SAT On considère des restrictions syntaxiques du problème SAT. Le problème FNC-SAT est la restriction du problème SAT aux formes normales conjonctives. Le problème 2-SAT est la restriction du problème SAT aux formes normales conjonctives avec au plus 2 littéraux par clause. Le problème 3-SAT est la restriction du problème SAT aux formes normales conjonctives avec au plus 3 littéraux par clause. Exemple d'instance : . Le problème HORN-SAT est la restriction du problème SAT aux formes normales conjonctives où les clauses sont des clauses de Horn.

Complexité et restrictions

FNC-SAT Le problème SAT est un problème NP–complet d'après le théorème de Cook. Par la transformée de tseitin, toute formule peut se transformer en une forme normale conjonctive équisatisfiable de taille linéaire en la formule initiale, le problème FNC-SAT est alors aussi NP-difficile, étant dans NP pour les mêmes raisons que SAT, il est alors NP-Complet.

3-SAT Le problème 3–SAT est lui aussi NP–complet. Pour démontrer la NP-difficulté de 3-SAT, il suffit de prouver que le problème FNC-SAT est polynomialement réductible à 3–SAT. La réduction transforme chaque clause avec en .

2-SAT Le problème 2-SAT est la restriction du problème SAT aux formes normales conjonctives avec au plus 2 littéraux par clause. Ce problème est dans la classe P. Sous l'hypothèse , il n'est pas NP-complet. Il existe plusieurs algorithmes polynomiaux déterministes pour résoudre le problème 2-SAT.

Algorithme de Aspvall, Plass et Tarjan Bengt Aspvall, Michael F. Plass, et Robert E. Tarjan, « », , 8, p. 121-123 (1979), . L'algorithme prend une formule en forme normale conjonctive avec au plus 2 littéraux par clause. Une clause d'ordre deux est équivalente aux implications et . Pour résoudre 2-SAT, on construit un graphe orienté dual (appelé graphe 2-SAT) selon les deux règles suivantes : les sommets sont les variables propositionnelles apparaissant dans la formule et les négations des variables propositionnelles apparaissant dans la formule ; on ajoute les arcs et pour chaque clause . La formule est satisfaisable si et seulement si pour toute variable propositionnelle de , et sont dans deux composantes fortement connexes distinctes dans le graphe 2-SAT. On utilise alors l'algorithme de Tarjan (ou l'algorithme de Kosaraju) pour calculer les composantes fortement connexes du graphe 2-SAT.

Christos Papadimitriou a montré, en 1994, que le problème 2-SAT est NL-complet.

HORN-SAT Le problème de satisfiabilité d'un ensemble de clauses de Horn propositionnelles (c'est-à-dire avec au plus un littéral positif par clause) est dans la classe P. Plus précisément, il existe un algorithme linéaire en la taille des clauses qui résout le problème de satisfiabilité. Il est P-complet (pour la réduction en espace logarithmique).

Théorème de dichotomie de Schaefer Le théorème de Schaefer donne des conditions nécessaires et suffisantes pour qu'une variante du problème SAT soit dans la classe P ou NP–complet. On retrouve les résultats de complexité concernant 3-SAT (NP-complet), 2-SAT (dans P), HORN-SAT (dans P) comme des applications de ce théorème.

Algorithmes pour 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.

Méthode systématique Pour prouver la satisfaisabilité du CNF , il suffit de choisir une variable et de prouver récursivement la satisfaisabilité de ou . La procédure est plus facile récursivement puisque avec ou 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 (la CNF est de la forme ), qui permettent de réduire fortement l'espace de recherche.

Exemple Considérons la CNF : . La deuxième clause () est unitaire et permet d'obtenir immédiatement . On peut remplacer les valeurs de dans ce CNF. Cela donne : . À nouveau, on a une clause unitaire, et on obtient . Puis, par propagation, on obtient .

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 apparaît toujours positivement dans la CNF , alors on peut poser puisque est satisfaisable si et seulement si est satisfaisable (et de même si la variable apparaît négativement). Ainsi, dans l'exemple précédent, n'apparaît que négativement et l'assignation peut être effectuée. Remarquons que cette affectation permet d'accélérer la découverte d'une solution mais que des solutions pourraient exister en effectuant l'assignation contraire. L'algorithme DPLL (Davis, Putnam Martin Davis et Hillary Putnam, « A Computing Procedure for Quantification Theory », Communications of the ACM, 7, p. 201-215 (1960) , Logemann, Loveland Martin Davis, George Logemann et Donald Loveland, « A machine Program for Theorem Proving », Communications of the ACM, 5, p. 394-397 (1962), ) se base sur ces idées.

Le choix de la variable à 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.

Apprentissage de clauses par conflits

Le principe des solveurs de type CDCL (Conflict-Driven Clause Learning) est d'utiliser un mécanisme pour apprendre de nouvelles clauses en cours de recherche, puis d'utiliser au maximum les informations apprises dans l'espoir d'améliorer le temps de recherche. D'un point de vue pratique, cette méthodologie est très efficace pour résoudre des problèmes concretsClassement des solveurs lors du SAT Challenge 2012, catégorie Application | Sat Challenge 2012. L'apprentissage de clauses est le suivant : lorsqu'un conflit apparaît lors de la recherche, c'est-à-dire lorsqu'une assignation partielle est démontrée non cohérente avec l'ensemble des clauses, on peut isoler un sous-ensemble de ces assignations et un sous-ensemble de ces clauses, qui sont responsables du conflit (les assignations ne sont pas cohérentes avec les clauses). L'apprentissage de clause permet deux choses. Premièrement, il permet d'éviter de refaire plusieurs fois les mêmes erreurs dans l'arbre de recherche. Deuxièmement, la clause apprise sera en contradiction avec l'état de l'arbre de recherche. De ce fait, il sera nécessaire de réaliser un retour en arrière (backtracking) pour s'assurer qu'au moins un de ces littéraux soit vrai.

Il existe différentes méthodes pour générer de nouvelles clauses à partir d'une inconsistance locale.

Méthode naïve

Soit l'instance à résoudre la formule suivante :

et l'interprétation partielle définie par: . Cette interprétation mène à un conflit car implique que , tandis que implique que . Pour générer une clause représentant ce conflit, il est possible de prendre la négation de l'interprétation : . Cependant, cette méthode possède un inconvénient majeur: la taille de la clause est entièrement déterminée par toute l'interprétation. Or, certaines parties de l'interprétation peuvent être complètement indépendantes du conflit que l'on souhaite représenter. En effet, ajoutons à l'instance les formules: et soit l'interprétation courante . Le conflit provient des deux premières clauses et donc, des valeurs de et . Or, la clause générée par la négation de l'interprétation prendra en compte toutes les variables à l'exception de . De ce fait, la clause sera inutilement longue.

Analyse des conflits Lorsque cette méthode est utilisée, un graphe est créé permettant de représenter l'origine de la propagation, appelé graphe d'implication. Les nœuds représentent les littéraux vrais. Il existe deux types de nœuds : les nœuds carrés dont la valeur du littéral provient d'un choix arbitraire et les nœuds ronds dont la valeur provient d'une propagation. À chaque nœud est également associée une information : le niveau du nœud en question. Ce niveau est défini par le nombre de littéraux choisis avant de réaliser la propagation s'il y a eu propagation. Sinon, le niveau est défini par le nombre de littéraux choisis, littéral courant compris. Les arcs relient entre eux les littéraux faisant partie d'une clause servant à la propagation. La destination d'un arc est le littéral propagé, la/les source(s) étant les autres littéraux de la clause. Soit l'instance à résoudre la formule suivante :

accompagné de l'interprétation à laquelle les niveaux des différents littéraux ont été spécifiés ainsi que le littéral menant à l’inconsistance : . Alors, il est possible d'en tirer le graphe suivant.

Grâce à ce graphe, il est possible de créer une clause représentant la cause du conflit. La méthode employée est la suivante : on commence par créer la résolvante des clauses menant à un conflit. Puis tant qu'il reste plus d'un littéral du niveau courant, une nouvelle résolvante est créée entre la résolvante courante et la cause d'un des littéraux du niveau courant. Sur notre exemple, cela donnera (où représente la résolution entre la clause et la clause )

Retour en arrière non chronologique Une fois la clause apprise, celle-ci sera utilisée pour le retour en arrière. L'idée derrière le retour en arrière non chronologique est qu'un retour en arrière sera effectué de manière que l'état des assignations soit tel qu'il ne reste qu'un seul littéral non assigné. Ainsi, grâce à la clause apprise, il sera possible de continuer les différentes propagations alors que cela n'était plus possible sans elle.