Résumé
Le problème SAT est celui du test de satisfiabilité, d’une formule Booléenne. Il peut se décrire comme le plus simple des problèmes difficiles à résoudre (techniquement, des problèmes NP-complets). Cette difficulté tranche avec l'apparente simplicité de la logique propositionnelle sur laquelle SAT se définit : on n’y manipule que des littéraux, c’est-à-dire des variables à valeurs dans {vrai, faux} ou leurs négations, et on cherche à vérifier des conjonctions de disjonctions de littéraux appelées clauses. Savoir s’il existe un tel algorithme efficace (polynomial) pour résoudre SAT est l'un des plus importants problèmes de l'informatique théorique.
SAT jalonne la frontière des problèmes pour lesquels aucun algorithme efficace dans tous les cas n’est connu : une traduction en SAT est systématiquement utilisée pour montrer l'impossibilité théorique de résoudre en pratique des problèmes de complexité comparable dans un large spectre de domaines. Pourtant, depuis plusieurs dizaines d'années, la communauté scientifique a remporté d'importantes victoires : de nombreux problèmes difficiles et parfois de très grande taille dans des domaines variés peuvent être résolus en pratique une fois transposés en un problème SAT équivalent. Les approches SAT se trouvent ainsi aujourd'hui au cœur de bien des avancées dans le monde des applications, et en particulier dans celui de la vérification formelle de circuits et programmes.
