Problème SAT

Eninformatique théorique, leproblème SATouproblème desatisfaisabilitébooléenneest leproblème de décision, qui, étant donné uneformule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie.
Ce problème est important enthéorie de la complexité. Il a été mis en lumière par lethéorème de Cook-Levin, qui est à la base de la théorie de laNP-complétudeet duproblème P = NP. Le problème SAT a aussi de nombreuses applications notamment ensatisfaction de contraintes,planificationclassique,model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation: on se ramène à desformules propositionnelleset on utilise unsolveur SAT.
Les formules de la logique propositionnelle sont construites à partir de variables propositionnelles et des connecteurs booléens "et" (∧{\displaystyle \land }), "ou" (∨{\displaystyle \lor }), "non" (¬{\displaystyle \lnot }). Une formule estsatisfaisable(on dit aussisatisfiable) s'il existe une assignation des variables propositionnelles qui rend la formulelogiquementvraie. Par exemple :
Unlittéralℓ{\displaystyle \ell }est une variable propositionnellevj{\displaystyle v_{j}}(littéral positif) ou la négation d'une variable propositionnelle¬vj{\displaystyle \lnot v_{j}}(littéral négatif). Uneclauseest unedisjonctionde la forme⋁i=1nℓi=(ℓ1∨ℓ2∨…∨ℓn){\displaystyle {\overset {n}{\underset {i=1}{\bigvee }}}\ell _{i}=(\ell _{1}\lor \ell _{2}\lor \ldots \lor \ell _{n})}où lesℓi{\displaystyle \ell _{i}}sont deslittéraux.
Une formule ducalcul propositionnelest enforme normale conjonctive(ou forme clausale ouCNFsigle de l'anglaisConjunctive Normal Form)si elle est une conjonction de clauses.
Si laformule propositionnellen'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.
On considère des restrictions syntaxiques du problème SAT.
Le problème SAT est unproblème NP–completd'après lethéorème de Cook. En particulier, on ne connaît aucunalgorithme déterministepolynomial pour le résoudre. De même, comme toute formule peut se transformer en une forme normale conjonctive équisatisfiable de taille linéaire en la formule initiale, le problème CNF-SAT est aussiNP-complet.
Le problème3–SATest lui aussi NP–complet. Pour démontrer laNP-difficultéde 3-SAT, il suffit de prouver que le problème CNF-SAT estpolynomialement réductibleà 3–SAT. La réduction transforme chaque clauseℓ1∨ℓ2∨…∨ℓn{\displaystyle \ell _{1}\lor \ell _{2}\lor \ldots \lor \ell _{n}}avecn≥3{\displaystyle n\geq 3}en(ℓ1∨ℓ2∨u1)∧(ℓ3∨¬u1∨u2)∧…∧(ℓn−2∨¬un−4∨un−3)∧(ℓn−1∨ℓn∨¬un−3){\displaystyle (\ell _{1}\lor \ell _{2}\lor u_{1})\land (\ell _{3}\lor \lnot u_{1}\lor u_{2})\land \ldots \land (\ell _{n-2}\lor \lnot u_{n-4}\lor u_{n-3})\land (\ell _{n-1}\lor \ell _{n}\lor \lnot u_{n-3})}.
Le problème2-SATest la restriction du problème SAT aux formes normales conjonctives avec au plus 2 littéraux par clause. Ce problème est dans laclasse P. Sous l'hypothèseP≠NP{\displaystyle P\neq NP}, il n'est pas NP-complet. Il existe plusieurs algorithmes polynomiaux déterministes pour résoudre le problème 2-SAT.
Christos Papadimitrioua montré, en 1994, que le problème 2-SAT estNL-complet.
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 laclasse P. Plus précisément, il existe un algorithme linéaireen la taille des clauses qui résout le problème de satisfiabilité. Il estP-complet(pour laréduction en espace logarithmique).
Le théorème de Schaeferdonne des conditions nécessaires et suffisantes pour qu'une variante du problème SAT soit dans laclasse PouNP–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.
La plus évidente des méthodes pour résoudre un problème SAT est de parcourir latable de véritédu problème, mais la complexité est alors exponentielle par rapport au nombre de variables.
Pour prouver la satisfaisabilité du CNFϕ{\displaystyle \phi \ }, il suffit de choisir une variablev{\displaystyle v~}et de prouver récursivement la satisfaisabilité dev∧ϕ{\displaystyle v\land \phi }ou¬v∧ϕ{\displaystyle \neg v\land \phi }. La procédure est plus facile récursivement puisquea∧ϕ{\displaystyle a\land \phi }aveca=v{\displaystyle a=v\ }oua=¬v{\displaystyle a=\neg v}peut souvent se simplifier. L'appel récursif construit ainsi unarbre binairederecherche.
Généralement, il existe à chaque nœud des clauses unitaires (la CNF est de la formeϕ=a∧ϕ′{\displaystyle \phi =a\land \phi '}), qui permettent de réduire fortement l'espace de recherche.
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 variablev{\displaystyle v\ }apparaît toujours positivement dans la CNFϕ{\displaystyle \phi \ }, alors on peut poserv=vrai{\displaystyle v={\textit {vrai}}\ }puisqueϕ{\displaystyle \phi \ }est satisfaisable si et seulement siϕ∧v{\displaystyle \phi \land v}est satisfaisable (et de même si la variable apparaît négativement). Ainsi, dans l'exemple précédent,v2{\displaystyle v_{2}\ }n'apparaît que négativement et l'assignationv2=faux{\displaystyle v_{2}=faux\ }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, Davis, Logemann, Loveland) se base sur ces idées.
Le choix de la variablev{\displaystyle 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.
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 concrets. 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.
Soit l'instance à résoudre la formuleϕ1{\displaystyle \phi _{1}}suivante :
et l'interprétation partielleI{\displaystyle {\mathcal {I}}}définie par:x2=faux,x3=faux{\displaystyle x_{2}={\textit {faux}},x_{3}={\textit {faux}}}. Cette interprétation mène à un conflit carx2{\displaystyle x_{2}}implique quex1=vrai{\displaystyle x_{1}=vrai}, tandis quex3{\displaystyle x_{3}}implique quex1=faux{\displaystyle x_{1}=faux}. Pour générer une clause représentant ce conflit, il est possible de prendre la négation de l'interprétationI{\displaystyle {\mathcal {I}}}:¬I=¬(¬x2∧¬x3)=x2∨x3{\displaystyle \neg {\mathcal {I}}=\neg (\neg x_{2}\land \neg x_{3})=x_{2}\lor x_{3}}. 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ϕ1{\displaystyle \phi _{1}}les formules:Ci=xi∨xi+1,4≤i≤N{\displaystyle C_{i}=x_{i}\lor x_{i+1},4\leq i\leq N}et soit l'interprétation couranteI={x2=faux,x3=faux,x4≤i≤N=faux}{\displaystyle {\mathcal {I}}=\{x_{2}=faux,x_{3}=faux,x_{4\leq i\leq N}=faux\}}. Le conflit provient des deux premières clauses et donc, des valeurs dex2{\displaystyle x_{2}}etx3{\displaystyle x_{3}}. Or, la clause générée par la négation de l'interprétation prendra en compte toutes les variables à l'exception dex1{\displaystyle x_{1}}. De ce fait, la clause sera inutilement longue.
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ϕ2{\displaystyle \phi _{2}}suivante :
accompagné de l'interprétation à laquelle les niveaux des différents littéraux ont été spécifiésI={d|1,f|1,e|2,g|2,h|3,i|3,j|3,a|3,b|3,c|3}{\displaystyle {\mathcal {I}}=\{d|_{1},f|_{1},e|_{2},g|_{2},h|_{3},i|_{3},j|_{3},a|_{3},b|_{3},c|_{3}\}}ainsi que le littéral menant à l’inconsistance :¬c{\displaystyle \neg c}. 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ésolvanteR1{\displaystyle {\mathcal {R}}_{1}}des clauses menant à un conflit. Puis tant qu'il reste plus d'un littéral du niveau courant, une nouvelle résolvanteRi+1{\displaystyle {\mathcal {R}}_{i+1}}est créée entre la résolvante couranteRi{\displaystyle {\mathcal {R}}_{i}}et la cause d'un des littéraux du niveau courant. Sur notre exemple, cela donnera (oùCi⊢RCj{\displaystyle C_{i}\vdash _{\mathcal {R}}C_{j}}représente la résolution entre la clauseCi{\displaystyle C_{i}}et la clauseCj{\displaystyle C_{j}})
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.
Si l'on reprend l'exempleϕ2{\displaystyle \phi _{2}}présenté dans la section analyse de conflit, la clause appriseR4=¬h∨¬g{\displaystyle {\mathcal {R}}_{4}=\neg h\lor \neg g}nous procure deux littéraux. Les niveaux des variables correspondantes sont: variableh{\displaystyle h}= 3, variableg{\displaystyle g}= 2. Pour savoir à quel niveau il est nécessaire de revenir en arrière, il faut regarder le niveau le plus profond (le niveaui+1{\displaystyle i+1}est plus profond que le niveaui{\displaystyle i}) des variables d'un niveau plus haut que le niveau actuel. Étant donné que la clause apprise ne contient que deux littéraux, il n'existe qu'un seul niveau différent du niveau actuel: le niveau 2. Un retour en arrière est donc effectué jusqu'à ce niveau et laisse donc comme interprétationI={d|1,f|1,e|2,g|2}{\displaystyle {\mathcal {I}}=\{d|_{1},f|_{1},e|_{2},g|_{2}\}}. Or, avec une telle interprétation, la clause apprise ne contient bien qu'une seule variable non affectée :h{\displaystyle h}tandis que l'autre est affectée de telle manière à ce que le littéral¬g{\displaystyle \neg g}soit faux. Cela implique la nécessité d'une propagation de la variableh{\displaystyle h}à la valeur faux.
Bien que dans cet exemple le retour en arrière ne s'effectue que sur un seul niveau, il est possible que celui-ci monte de plusieurs niveaux d'un coup. En effet, imaginons que nous puissions ajouter N niveaux entre le niveau 2 et le niveau 3 où toutes les variables qui y apparaissent soient de nouvelles variables. Puisque ces niveaux n'auraient pas d'impact sur l'ancien niveau 3, le retour en arrière remonterait d'un coup ces N+1 niveaux.
L'approche prospective consiste àprospecterl'arbre de recherche pour découvrir des assignations certaines. Ainsi, étant donné un CNFϕ{\displaystyle \phi \ }, étant donné une variable non instanciéev{\displaystyle v\ }, on prospecte les CNFsϕ∧v{\displaystyle \phi \land v}etϕ∧¬v{\displaystyle \phi \land \neg v}. Si les deux CNFs conduisent à l'instanciation de la même variablev′{\displaystyle v'\ }avec la même valeur, alors l'instanciation peut se faire dès la CNFϕ{\displaystyle \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.
Samer et Szeider ont proposé un algorithme deprogrammation dynamiquequi est polynomial en la taille de la formule à tester quand lalargeur arborescentedu graphe associé à cette formule est un paramètre fixé (voirComplexité_paramétrée). L'avantage de cette algorithme est qu'il peut aussi faire du comptage de valuationset donc résoudre le problème #SAT. Il peut aussi être parallélisé. Il est implémenté dans l'outil gpuSAT(la parallélisation est implémentée via le GPU).
Partant d'une assignation 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-satisfaisabilité, 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 une nouvelle assignation aléatoire pour éviter les minima locaux.
Il est possible deréduire(traduire) certains problèmes d'intelligence artificielleau problème SAT afin de résoudre efficacement ces problèmes.
Lediagnosticde 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 composantc{\displaystyle c}du système, une variableAb(c){\displaystyle Ab(c)}est créée qui est évaluée àvraiesi le composant a un comportement anormal (Abnormal). Les observations peuvent être également traduites par un ensemble de disjonctions. L'assignation trouvée par l'algorithme de satisfaisabilité est un diagnostic.
Le problème deplanification classiqueconsiste à trouver une séquence d'actions menant d'un état du système à un ensemble d'états. Étant donnée une longueur maximale du plann{\displaystyle n}et un ensembleV{\displaystyle V}de variables d'état booléennes permettant de décrire l'état du système, on crée les variables propositionellesvi{\displaystyle v^{i}}pour touti∈{0,…,n}{\displaystyle i\in \{0,\dots ,n\}}et toute variablev∈V{\displaystyle v\in V}. La variablevi{\displaystyle v_{i}}estvraiesi la variable d'état estvraieaprès l'action numéroi{\displaystyle i}. On crée également les variablesai{\displaystyle a^{i}}pour touti∈{1,…,n}{\displaystyle i\in \{1,\dots ,n\}}et toute actiona{\displaystyle a}. La variableai{\displaystyle a^{i}}estvraiesi l'action numéroi{\displaystyle i}esta{\displaystyle a}. Il est alors possible de transformer le modèle du système en un ensemble de clauses. Par exemple, si l'actiona{\displaystyle a}fait passer la variablev1{\displaystyle v_{1}}àvrailorsque celle-ci estfausse, alors la CNF contiendra une clause(¬v0)⇒a1⇒v1{\displaystyle (\neg v^{0})\Rightarrow a^{1}\Rightarrow v^{1}}(ce qui est traduit par la clausev0∨¬a1∨v1{\displaystyle v^{0}\lor \neg a^{1}\lor v^{1}}). L'assignation trouvée par l'algorithme de satisfaisabilité peut être immédiatement traduite en plan.
La planification classique par SAT est très efficace si on connaît la longueurndu 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 la CNF est non satisfaisable jusqu'àn– 1).
Une approche semblable a été utilisée pour lemodel checking(vérification de propriétés d'un modèle). La principale différence est que lemodel checkings'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. Lebounded model checkingtire parti de cette propriété pour transformer le problème demodel checkingen un certain nombre de problèmes de satisfaisabilité.
La complexité du problème SAT est une composante essentielle de la sécurité de tout système decryptographie.
Par exemple, unefonction de hachagesécurisée constitue une boîte noire pouvant être formulée en un temps et un espace fini sous la forme d'une conjonction de clauses normales, dont les variables booléennes correspondent directement aux valeurs possibles des données d’entrée de la fonction de hachage, et chacun des bits de résultat devra répondre à un test booléen d'égalité avec les bits de données d’un bloc de données d’entrées quelconque. Les fonctions de hachages sécurisées servent notamment dans des systèmes d'authentification (connaissance de données secrètes d’entrée ayant servi à produire la valeur de hachage) et de signature (contre toute altération ou falsification « facile » des données d’entrée, qui sont connues en même temps que la fonction de hachage elle-même et de son résultat).
La sécurité de la fonction de hachage dépend de la possibilité de retrouver un bloc de données d'entrée arbitraire (éventuellement différent du bloc secret de données pour lequel une valeur de hachage donnée a été obtenue) permettant d'égaliser la valeur binaire retournée par la fonction de hachage. Une méthode d'exploration systématique de toutes les valeurs possibles des données d'entrée et pour lesquelles on applique la fonction de hachage comme un oracle, permet effectivement de satisfaire à la question de une valeur de hachage égale à celle cherchée, mais sa complexité algorithmique sera exponentielle (en fonction de la taille maximale en bits des données d’entrée de la fonction de hachage).
Chercher à égaliser une valeur de hachage avec des variables d'entrée de valeur inconnue constitue un problème SAT (et comme en pratique les données d’entrée de la fonction de hachage sont constituées de nombreux bits, ce sera un problèmen-SAT avecnassez élevé (et en tout cas supérieur ou égal à 3). On sait alors que ce problème est réductible en temps polynomial à un problème 3–SAT, qui est NP-complet.
La sécurité de la fonction de hachage sera fortement liée au fait de l'impossibilité de la réduire plus simplement (que par un algorithme NP-complet de complexité suffisante) en réduisant la forme conjonctive des clauses qui la définissent simplement, pour y isoler des sous-ensembles de variables d’entrées de taille plus restreinte, mais suffisante pour déterminer une partie du résultat de la fonction de hachage dont l’ordrensera alors très inférieur, et pour ne plus avoir à explorer que les valeurs possibles de ces seuls sous-ensembles de variables pour satisfaire la condition d'égalité du résultat, sans avoir à tester toutes les autres variables dont la valeur peut être fixée arbitrairement à certaines valeurs déterminées par un algorithme plus simple (apprentissage de clauses, approches prospectives ci-dessus).
Le problème SAT peut être utilisé comme sous-routine pour résoudre le problème de satisfiabilité de la logique modale.
Il existe des extensions au problème SAT.
Martin DavisetHilary Putnamproposentleur algorithmepour le problème SAT en 1960, ensuite amélioré par George Logemann etDonald Loveland(en)(Algorithme de Davis-Putnam-Logemann-Loveland). Une impulsion a été donnée quandStephen Cookl'a utilisé comme paradigme desproblèmes NP-complets.  Une autre impulsion a été donnée en 2002 quand a commencé la compétition SATentre logiciels de résolution de problèmes SAT.