Problème de satisfaction booléenne

En logique et en informatique , le problème de satisfiabilité booléenne (parfois appelé problème de satisfiabilité propositionnelle et abrégé en SATISFIABILITÉ , SAT ou B-SAT ) est le problème consistant à déterminer s'il existe une interprétation qui satisfait une formule booléenne donnée . En d'autres termes, il s'agit de savoir si les variables d'une formule booléenne donnée peuvent être remplacées de manière cohérente par les valeurs VRAI ou FAUX de telle sorte que la formule soit évaluée à VRAI. Si tel est le cas, la formule est dite satisfiable . En revanche, si aucune affectation de ce type n'existe, la fonction exprimée par la formule est FAUSSE pour toutes les affectations de variables possibles et la formule est insatisfiable . Par exemple, la formule « a AND NOT b » est satisfiable car on peut trouver les valeurs a = VRAI et b = FAUX, ce qui fait que ( a AND NOT b ) = VRAI. En revanche, « a AND NOT a » est insatisfiable.

SAT est le premier problème dont on a prouvé qu'il était NP-complet — c'est le théorème de Cook-Levin . Cela signifie que tous les problèmes de la classe de complexité NP , qui comprend un large éventail de problèmes de décision et d'optimisation naturels, sont au plus aussi difficiles à résoudre que SAT. Il n'existe aucun algorithme connu qui résolve efficacement chaque problème SAT, et on pense généralement qu'aucun algorithme de ce type n'existe, mais cette croyance n'a pas été prouvée mathématiquement, et résoudre la question de savoir si SAT possède un algorithme en temps polynomial équivaut au problème P versus NP , qui est un problème ouvert célèbre de la théorie de l'informatique.

Néanmoins, depuis 2007, les algorithmes SAT heuristiques sont capables de résoudre des cas de problèmes impliquant des dizaines de milliers de variables et des formules composées de millions de symboles, ce qui est suffisant pour de nombreux problèmes SAT pratiques, par exemple, l'intelligence artificielle , la conception de circuits , et la preuve automatique de théorèmes .

Une formule de logique propositionnelle , également appelée expression booléenne , est construite à partir de variables , d'opérateurs AND ( conjonction , également notée ∧), OR ( disjonction , ∨), NOT ( négation , ¬) et de parenthèses. Une formule est dite satisfaisable si elle peut être rendue VRAIE en attribuant des valeurs logiques appropriées (c'est-à-dire VRAI, FAUX) à ses variables. Le problème de satisfiabilité booléenne (SAT) consiste, étant donné une formule, à vérifier si elle est satisfaisable. Ce problème de décision est d'une importance capitale dans de nombreux domaines de l'informatique , notamment l'informatique théorique , la théorie de la complexité , l'algorithmique , la cryptographie et l'intelligence artificielle .

Un littéral est soit une variable (auquel cas il est appelé littéral positif ), soit la négation d'une variable (appelé littéral négatif ). Une clause est une disjonction de littéraux (ou un littéral unique). Une clause est appelée clause de Horn si elle contient au plus un littéral positif. Une formule est sous forme normale conjonctive (CNF) si elle est une conjonction de clauses (ou une clause unique).

Par exemple, x ₁ est un littéral positif, ¬ x ₂ est un littéral négatif et x ₁ ∨ ¬ x ₂ est une clause. La formule ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ est sous forme normale conjonctive ; ses première et troisième clauses sont des clauses de Horn, mais sa deuxième clause ne l'est pas. La formule est satisfaisable en choisissant arbitrairement x ₁ = FAUX, x ₂ = FAUX et x _{3 , puisque (FAUX ∨ ¬FAUX) ∧ (¬FAUX ∨ FAUX ∨} x ₃ ) ∧ ¬FAUX est évalué à (FAUX ∨ VRAI) ∧ (VRAI ∨ FAUX ∨ x ₃ ) ∧ VRAI, et à son tour à VRAI ∧ VRAI ∧ VRAI (c'est-à-dire à VRAI). En revanche, la formule CNF a ∧ ¬ a , composée de deux clauses d'un littéral, n'est pas satisfaisable, car pour a =VRAI ou a =FAUX elle est évaluée à VRAI ∧ ¬VRAI (c'est-à-dire FAUX) ou FAUX ∧ ¬FAUX (c'est-à-dire à nouveau FAUX), respectivement.

Pour certaines versions du problème SAT, il est utile de définir la notion de formule de forme normale conjonctive généralisée , à savoir comme une conjonction d'un nombre arbitraire de clauses généralisées , ces dernières étant de la forme R ( l ₁ ,..., l _n ) pour une fonction booléenne R et des littéraux (ordinaires) l _i . Différents ensembles de fonctions booléennes autorisées conduisent à différentes versions du problème. Par exemple, R (¬ x , a , b ) est une clause généralisée, et R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) est une forme normale conjonctive généralisée. Cette formule est utilisée ci-dessous, R étant l'opérateur ternaire qui est VRAI uniquement lorsque l'un de ses arguments l'est.

En utilisant les lois de l'algèbre booléenne , chaque formule de logique propositionnelle peut être transformée en une forme normale conjonctive équivalente, qui peut cependant être exponentiellement plus longue. Par exemple, la transformation de la formule ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) en forme normale conjonctive donne

( x ₁ ∨ x ₂ ∨ … ∨ x _n ) ∧

( y ₁ ∨ x ₂ ∨ … ∨ x _n ) ∧

( x ₁ ∨ y ₂ ∨ … ∨ x _n ) ∧

( y ₁ ∨ y ₂ ∨ … ∨ x _n ) ∧ ... ∧

( x ₁ ∨ x ₂ ∨ … ∨ y _n ) ∧

( oui ₁ ∨ X ₂ ∨ … ∨ oui _n ) ∧

( X ₁ ∨ y ₂ ∨ … ∨ y _n ) ∧

( oui ₁ ∨ oui ₂ ∨ … ∨ oui _n ) ;

tandis que la première est une disjonction de n conjonctions de 2 variables, la seconde est constituée de 2 ⁿ clauses de n variables.

Cependant, avec l'utilisation de la transformation de Tseytin , nous pouvons trouver une formule de forme normale conjonctive équisatisfaisable avec une longueur linéaire dans la taille de la formule logique propositionnelle originale.

SAT est le premier problème connu comme étant NP-complet , comme l'ont prouvé Stephen Cook à l' Université de Toronto en 1971 et indépendamment Leonid Levin à l' Académie des sciences de Russie en 1973. Jusqu'à cette époque, le concept de problème NP-complet n'existait même pas. La preuve montre comment chaque problème de décision dans la classe de complexité NP peut être réduit au problème SAT pour les formules CNF , parfois appelées CNFSAT . Une propriété utile de la réduction de Cook est qu'elle préserve le nombre de réponses acceptables. Par exemple, décider si un graphe donné a une 3-coloration est un autre problème de NP ; si un graphe a 17 3-colorations valides, alors la formule SAT produite par la réduction de Cook-Levin aura 17 affectations satisfaisantes.

La complétude NP ne concerne que le temps d'exécution des cas les plus défavorables. De nombreuses instances qui se produisent dans des applications pratiques peuvent être résolues beaucoup plus rapidement. Voir §Algorithmes de résolution de SAT ci-dessous.

Comme le problème de satisfiabilité pour des formules arbitraires, déterminer la satisfiabilité d'une formule sous forme normale conjonctive où chaque clause est limitée à trois littéraux au plus est également NP-complet ; ce problème est appelé 3-SAT , 3CNFSAT ou 3-satisfiabilité . Pour réduire le problème SAT non restreint à 3-SAT, transformez chaque clause l ₁ ∨ ⋯ ∨ l _n en une conjonction de n - 2 clauses

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n −3} ∨ l _{n −2} ∨ x _{n −2} ) ∧

(¬ x _{n −2} ∨ l _{n −1} ∨ l _n )

où x ₂ , ⋯ ,  x _{n −2} sont des variables fraîches qui n'apparaissent pas ailleurs. Bien que les deux formules ne soient pas logiquement équivalentes , elles sont équisatisfaisables . La formule résultant de la transformation de toutes les clauses est au plus 3 fois plus longue que son originale ; c'est-à-dire que la croissance de longueur est polynomiale.

Le 3-SAT est l'un des 21 problèmes NP-complets de Karp , et il est utilisé comme point de départ pour prouver que d'autres problèmes sont également NP-difficiles . Cela se fait par réduction en temps polynomial du 3-SAT à l'autre problème. Un exemple de problème où cette méthode a été utilisée est le problème de la clique : étant donnée une formule CNF composée de c clauses, le graphe correspondant est composé d'un sommet pour chaque littéral, et d'une arête entre chaque deux littéraux non contradictoires de clauses différentes ; voir l'image. Le graphe a une c -clique si et seulement si la formule est satisfiable.

Il existe un algorithme randomisé simple dû à Schöning (1999) qui s'exécute en temps (4/3) ⁿ où n est le nombre de variables dans la proposition 3-SAT, et qui réussit avec une forte probabilité à décider correctement 3-SAT.

L' hypothèse du temps exponentiel affirme qu'aucun algorithme ne peut résoudre 3-SAT (ou même k -SAT pour tout k > 2 ) en temps exp( o ( n )) (c'est-à-dire fondamentalement plus rapidement que l'exponentiel en n ).

Selman, Mitchell et Levesque (1996) fournissent des données empiriques sur la difficulté des formules 3-SAT générées aléatoirement, en fonction de leurs paramètres de taille. La difficulté est mesurée en nombre d'appels récursifs effectués par un algorithme DPLL . Ils ont identifié une région de transition de phase allant des formules presque certainement satisfaisables aux formules presque certainement insatisfaisables au rapport clauses/variables d'environ 4,26.

La 3-satisfiabilité peut être généralisée à la k-satisfiabilité ( k-SAT , également k-CNF-SAT ), lorsque les formules en CNF sont considérées avec chaque clause contenant jusqu'à k littéraux. Cependant, comme pour tout k ≥ 3, ce problème ne peut être ni plus facile que 3-SAT ni plus difficile que SAT, et les deux derniers sont NP-complets, donc doit être k-SAT.

Certains auteurs limitent k-SAT aux formules CNF avec exactement k littéraux . Cela ne conduit pas non plus à une classe de complexité différente, car chaque clause l ₁ ∨ ⋯ ∨ l _j avec j < k littéraux peut être complétée avec des variables muettes fixes à l ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ d _k . Après avoir complété toutes les clauses, 2 ^k –1 clauses supplémentaires doivent être ajoutées pour garantir que seules d ₁ = ⋯ = d _k = FAUX peuvent conduire à une affectation satisfaisante. Puisque k ne dépend pas de la longueur de la formule, les clauses supplémentaires conduisent à une augmentation constante de la longueur. Pour la même raison, il importe peu que les littéraux en double soient autorisés dans les clauses, comme dans ¬ x ∨ ¬ y ∨ ¬ y .

La forme normale conjonctive (en particulier avec 3 littéraux par clause) est souvent considérée comme la représentation canonique des formules SAT. Comme indiqué ci-dessus, le problème général SAT se réduit à 3-SAT, le problème de la détermination de la satisfiabilité des formules sous cette forme.

SAT est triviale si les formules sont restreintes à celles sous forme normale disjonctive , c'est-à-dire qu'elles sont une disjonction de conjonctions de littéraux. Une telle formule est en effet satisfiable si et seulement si au moins une de ses conjonctions est satisfiable, et une conjonction est satisfiable si et seulement si elle ne contient pas à la fois x et NOT x pour une variable x . Cela peut être vérifié en temps linéaire. De plus, si elles sont restreintes à être sous forme normale disjonctive complète , dans laquelle chaque variable apparaît exactement une fois dans chaque conjonction, elles peuvent être vérifiées en temps constant (chaque conjonction représente une affectation satisfaisante). Mais il peut falloir un temps et un espace exponentiels pour convertir un problème SAT général en forme normale disjonctive ; pour obtenir un exemple, remplacez « ∧ » et « ∨ » dans l'exemple d'explosion exponentielle ci-dessus par des formes normales conjonctives.

Une variante du problème de satisfiabilité 3 est le 3-SAT un sur trois (également connu sous les noms de 1-sur-3-SAT et exactement-1 3-SAT ). Étant donné une forme normale conjonctive avec trois littéraux par clause, le problème consiste à déterminer s'il existe une affectation de vérité aux variables de sorte que chaque clause ait exactement un littéral VRAI (et donc exactement deux littéraux FAUX). En revanche, le 3-SAT ordinaire exige que chaque clause ait au moins un littéral VRAI. Formellement, un problème 3-SAT un sur trois est donné comme une forme normale conjonctive généralisée avec toutes les clauses généralisées utilisant un opérateur ternaire R qui est VRAI juste si exactement un de ses arguments l'est. Lorsque tous les littéraux d'une formule 3-SAT un sur trois sont positifs, le problème de satisfiabilité est appelé 3-SAT positif un sur trois .

Le problème 3-SAT un sur trois, ainsi que son cas positif, est répertorié comme problème NP-complet « LO4 » dans la référence standard Computers and Intractability: A Guide to the Theory of NP-Completeness de Michael R. Garey et David S. Johnson . Le problème 3-SAT un sur trois a été prouvé comme étant NP-complet par Thomas Jerome Schaefer comme cas particulier du théorème de dichotomie de Schaefer , qui affirme que tout problème généralisant la satisfiabilité booléenne d'une certaine manière est soit dans la classe P, soit NP-complet.

Schaefer donne une construction permettant une réduction en temps polynomial facile de 3-SAT à 3-SAT un sur trois. Soit "( x ou y ou z )" une clause dans une formule 3CNF. Ajoutez six nouvelles variables booléennes a , b , c , d , e et f , à utiliser pour simuler cette clause et aucune autre. Alors la formule R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c ,FAUX) est satisfaisable par un réglage des nouvelles variables si et seulement si au moins une des x , y ou z est VRAIE, voir image (à gauche). Ainsi, toute instance 3-SAT avec m clauses et n variables peut être convertie en une instance 3-SAT un sur trois équisatisfaisable avec 5 m clauses et n + 6 m variables. Une autre réduction implique seulement quatre nouvelles variables et trois clauses : R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R( c , d ,¬ z ), voir l'image (à droite).

Une autre variante est le problème de satisfaction 3-non-égal (également appelé NAE3SAT ). Étant donnée une forme normale conjonctive avec trois littéraux par clause, le problème consiste à déterminer si une affectation aux variables existe telle que dans aucune clause les trois littéraux n'aient la même valeur de vérité. Ce problème est également NP-complet, même si aucun symbole de négation n'est admis, par le théorème de dichotomie de Schaefer.

Une formule 3-SAT est une formule SAT linéaire ( LSAT ) si chaque clause (considérée comme un ensemble de littéraux) croise au plus une autre clause et, de plus, si deux clauses se croisent, alors elles ont exactement un littéral en commun. Une formule LSAT peut être représentée comme un ensemble d'intervalles semi-fermés disjoints sur une ligne. Déterminer si une formule LSAT est satisfaisable est NP-complet.

Le problème SAT est plus simple si le nombre de littéraux dans une clause est limité à 2 au maximum, auquel cas le problème est appelé 2-SAT . Ce problème peut être résolu en temps polynomial et est en fait complet pour la classe de complexité NL . Si en plus toutes les opérations OR dans les littéraux sont transformées en opérations XOR , alors le résultat est appelé 2-satisfiabilité en mode OU exclusif , ce qui est un problème complet pour la classe de complexité SL = L.

Le problème de la détermination de la satisfiabilité d'une conjonction donnée de clauses de Horn est appelé Horn-satisfiabilité , ou HORN-SAT . Il peut être résolu en temps polynomial par une seule étape de l' algorithme de propagation unitaire , qui produit le modèle minimal unique de l'ensemble des clauses de Horn (par rapport à l'ensemble des littéraux assignés à TRUE). La satisfiabilité de Horn est P-complète . Elle peut être considérée comme la version de P du problème de satisfiabilité booléenne. De plus, la détermination de la vérité des formules de Horn quantifiées peut être effectuée en temps polynomial.

Les clauses de Horn sont intéressantes car elles permettent d'exprimer l'implication d'une variable à partir d'un ensemble d'autres variables. En effet, une telle clause ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y peut être réécrite comme x ₁ ∧ ... ∧ x _n → y ; c'est-à-dire que si x ₁ ,..., x _n sont toutes VRAIES, alors y doit être VRAIE également.

Une généralisation de la classe des formules de Horn est celle des formules de Horn renommables, qui sont l'ensemble des formules qui peuvent être placées sous forme de Horn en remplaçant certaines variables par leur négation respective. Par exemple, ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ n'est pas une formule de Horn, mais peut être renommée en formule de Horn ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ en introduisant y ₃ comme négation de x ₃ . En revanche, aucun changement de nom de ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ ne conduit à une formule de Horn. La vérification de l'existence d'un tel remplacement peut être effectuée en temps linéaire ; par conséquent, la satisfiabilité de telles formules est dans P car elle peut être résolue en effectuant d'abord ce remplacement puis en vérifiant la satisfiabilité de la formule de Horn résultante.

Un autre cas particulier est la classe de problèmes où chaque clause contient des opérateurs XOR (c'est-à-dire exclusif ou ) plutôt que des opérateurs OR (simple). C'est dans P , car une formule XOR-SAT peut aussi être vue comme un système d'équations linéaires mod 2, et peut être résolue en temps cubique par élimination gaussienne ; voir l'encadré pour un exemple. Cette reformulation est basée sur la parenté entre les algèbres booléennes et les anneaux booléens , et sur le fait que l'arithmétique modulo deux forme un corps fini . Puisque a XOR b XOR c est évalué à VRAI si et seulement si exactement 1 ou 3 membres de { a , b , c } sont VRAI, chaque solution du problème 1-en-3-SAT pour une formule CNF donnée est aussi une solution du problème XOR-3-SAT, et à son tour chaque solution de XOR-3-SAT est une solution de 3-SAT ; voir l'image. En conséquence, pour chaque formule CNF, il est possible de résoudre le problème XOR-3-SAT défini par la formule, et en fonction du résultat, de déduire soit que le problème 3-SAT est soluble, soit que le problème 1-en-3-SAT est insoluble.

À condition que les classes de complexité P et NP ne soient pas égales , ni la satisfaction 2, ni la satisfaction Horn, ni la satisfaction XOR ne sont NP-complètes, contrairement à SAT.

Les restrictions ci-dessus (CNF, 2CNF, 3CNF, Horn, XOR-SAT) lient les formules considérées à des conjonctions de sous-formules ; chaque restriction énonce une forme spécifique pour toutes les sous-formules : par exemple, seules les clauses binaires peuvent être des sous-formules dans 2CNF.

Le théorème de dichotomie de Schaefer stipule que, pour toute restriction aux fonctions booléennes pouvant être utilisées pour former ces sous-formules, le problème de satisfaction correspondant est dans P ou NP-complet. L'appartenance à P de la satisfaction des formules 2CNF, Horn et XOR-SAT sont des cas particuliers de ce théorème.

Le tableau suivant résume certaines variantes courantes du SAT.

Une extension qui a gagné en popularité depuis 2003 est la théorie de la satisfiabilité modulo ( SMT ) qui peut enrichir les formules CNF avec des contraintes linéaires, des tableaux, des contraintes toutes différentes, des fonctions non interprétées , etc. De telles extensions restent généralement NP-complètes, mais des solveurs très efficaces sont désormais disponibles et peuvent gérer de nombreux types de contraintes.

Le problème de satisfiabilité devient plus difficile si les quantificateurs « pour tout » ( ∀ ) et « il existe » ( ∃ ) sont autorisés à lier les variables booléennes. Un exemple d'une telle expression serait ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; elle est valide, car pour toutes les valeurs de x et y , une valeur appropriée de z peut être trouvée, à savoir z = VRAI si x et y sont tous deux FAUX, et z = FAUX sinon. SAT lui-même (tacitement) utilise uniquement des quantificateurs ∃ . Si seuls les quantificateurs ∀ sont autorisés, on obtient le problème dit de tautologie , qui est co-NP-complet . Si les deux quantificateurs sont autorisés, le problème est appelé problème de formule booléenne quantifiée ( QBF ), dont on peut démontrer qu'il est PSPACE-complet . Il est largement admis que les problèmes PSPACE-complets sont strictement plus difficiles que n'importe quel problème en NP, bien que cela n'ait pas encore été prouvé. En utilisant des systèmes P hautement parallèles , les problèmes QBF-SAT peuvent être résolus en temps linéaire.

Le SAT ordinaire demande s'il existe au moins une affectation de variable qui rend la formule vraie. Il existe plusieurs variantes concernant le nombre de ces affectations :

• MAJ-SAT demande si la majorité des affectations rendent la formule VRAIE. On sait qu'elle est complète pour PP , une classe probabiliste.
• #SAT , le problème de compter le nombre d'affectations de variables satisfaisant une formule, est un problème de comptage, pas un problème de décision, et est #P-complet .
• UNIQUE SAT est le problème de déterminer si une formule a exactement une affectation. Il est complet pour US, la classe de complexité décrivant les problèmes résolubles par une machine de Turing à temps polynomial non déterministe qui accepte lorsqu'il y a exactement un chemin acceptant non déterministe et rejette sinon.
• UNAMBIGUOUS-SAT est le nom donné au problème de satisfiabilité lorsque l'entrée est restreinte aux formules ayant au plus une affectation satisfaisante. Le problème est également appelé USAT . Un algorithme de résolution pour UNAMBIGUOUS-SAT est autorisé à présenter n'importe quel comportement, y compris une boucle sans fin, sur une formule ayant plusieurs affectations satisfaisantes. Bien que ce problème semble plus facile, Valiant et Vazirani ont montré que s'il existe un algorithme pratique (c'est-à-dire randomisé en temps polynomial ) pour le résoudre, alors tous les problèmes de NP peuvent être résolus tout aussi facilement.
• MAX-SAT , le problème de satisfaction maximale , est une généralisation FNP de SAT. Il demande le nombre maximal de clauses qui peuvent être satisfaites par n'importe quelle affectation. Il dispose d'algorithmes d'approximation efficaces , mais il est NP-difficile à résoudre exactement. Pire encore, il est APX -complet, ce qui signifie qu'il n'existe pas de schéma d'approximation en temps polynomial (PTAS) pour ce problème à moins que P=NP.
• WMSAT est le problème de recherche d'une affectation de poids minimum qui satisfasse une formule booléenne monotone (c'est-à-dire une formule sans aucune négation). Les poids des variables propositionnelles sont donnés en entrée du problème. Le poids d'une affectation est la somme des poids des variables vraies. Ce problème est NP-complet (voir Th. 1 de ).

D'autres généralisations incluent la satisfaction pour la logique du premier et du second ordre , les problèmes de satisfaction de contraintes et la programmation en nombres entiers 0-1 .

Bien que SAT soit un problème de décision , le problème de recherche d'une affectation satisfaisante se réduit à SAT. Autrement dit, chaque algorithme qui répond correctement à la question de savoir si une instance de SAT est résoluble peut être utilisé pour trouver une affectation satisfaisante. Tout d'abord, la question est posée sur la formule donnée Φ. Si la réponse est « non », la formule est insatisfaisable. Sinon, la question est posée sur la formule partiellement instanciée Φ { x ₁ =VRAI} , c'est-à-dire Φ avec la première variable x ₁ remplacée par VRAI, et simplifiée en conséquence. Si la réponse est « oui », alors x ₁ =VRAI, sinon x ₁ =FAUX. Les valeurs d'autres variables peuvent être trouvées ultérieurement de la même manière. Au total, n +1 exécutions de l'algorithme sont nécessaires, où n est le nombre de variables distinctes dans Φ.

Cette propriété est utilisée dans plusieurs théorèmes de la théorie de la complexité :

NP ⊆ P/poly ⇒ PH = Σ ₂ ( théorème de Karp–Lipton )

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Étant donné que le problème SAT est NP-complet, seuls des algorithmes avec une complexité exponentielle dans le pire des cas sont connus pour lui. Malgré cela, des algorithmes efficaces et évolutifs pour SAT ont été développés au cours des années 2000 et ont contribué à des avancées spectaculaires dans la capacité à résoudre automatiquement des instances de problèmes impliquant des dizaines de milliers de variables et des millions de contraintes (c'est-à-dire des clauses). Des exemples de tels problèmes dans l'automatisation de la conception électronique (EDA) incluent la vérification d'équivalence formelle , la vérification de modèle , la vérification formelle de microprocesseurs pipelined , la génération automatique de modèles de test , le routage de FPGA , les problèmes de planification et d'ordonnancement , etc. Un moteur de résolution SAT est également considéré comme un composant essentiel de la boîte à outils d'automatisation de la conception électronique .

Les principales techniques utilisées par les solveurs SAT modernes comprennent l' algorithme Davis-Putnam-Logemann-Loveland (ou DPLL), l'apprentissage des clauses pilotées par les conflits (CDCL) et les algorithmes de recherche locale stochastique tels que WalkSAT . Presque tous les solveurs SAT incluent des délais d'attente, de sorte qu'ils se termineront dans un délai raisonnable même s'ils ne peuvent pas trouver de solution. Différents solveurs SAT trouveront différentes instances faciles ou difficiles, et certains excellent à prouver l'insatisfaction, et d'autres à trouver des solutions. Des tentatives récentes ont été faites pour apprendre la satisfaction d'une instance en utilisant des techniques d'apprentissage profond.

Les solveurs SAT sont développés et comparés lors de concours de résolution SAT. Les solveurs SAT modernes ont également un impact significatif sur les domaines de la vérification de logiciels, de la résolution de contraintes en intelligence artificielle et de la recherche opérationnelle, entre autres.