Principe de satisfiabilité booléenne

Le principe de satisfiabilité booléenne (parfois appelé problème de satisfiabilité propositionnelle et abrégé SATISFIABILITÉ ou problème 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 demande si les variables d'une formule booléenne donnée peuvent être remplacées de manière cohérente par les valeurs TRUE ou FALSE de manière à ce que la formule soit évaluée à VRAI. Si tel est le cas, la formule est appelée satisfiable. D'autre part, si aucune affectation de ce type n’existe, la fonction exprimée par la formule est FAUSSE pour toutes les affectations possibles variables et la formule est insatisfiable . Par exemple, la formule " a AND NOT b " est satisfiable car on peut trouver les valeurs a = TRUE et b = FALSE, ce qui donne (a AND NOT b) = TRUE. En revanche, " a AND NOT a " est insatisfiable.

SAT est le premier problème qui s'est avéré NP-complet. Cela signifie que tous les problèmes dans la classe de complexité NP, qui comprend un large éventail de décisions naturelles et des problèmes d’optimisation, sont au plus aussi difficile à résoudre que SAT. Il n'y a pas algorithme connu qui permette de résoudre efficacement chaque problème SAT, et il est généralement admis qu'aucun algorithme de ce type n'existe; pourtant cette croyance n’a pas été prouvée mathématiquement, et résoudre la question de savoir si SAT a un algorithme polynomial est équivalent au problème P versus NP, qui est un célèbre problème ouvert de la théorie de l’informatique.

Néanmoins, à partir de 2007, les algorithmes SAT heuristiques sont capables de résoudre des problèmes comportant des dizaines de milliers de variables et des formules comprenant des millions de symboles , ce qui suffit pour de nombreux problèmes pratiques de SAT, tels que l'intelligence artificielle, les circuits. conception et démonstration automatique de théorèmes .