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.
Dans ce séminaire, nous suivrons l'aventure scientifique qui a conduit ces progrès. Nous présenterons d’abord les ingrédients essentiels des démonstrateurs SAT actuels, dont beaucoup ont été développés au fil des compétitions du domaine et en fonction des applications rencontrées. Nous montrerons ensuite que certains de ces ingrédients, pourtant essentiels, ne sont pas encore bien compris : même si l'on sait écrire des algorithmes efficaces pour résoudre des problèmes de taille industrielle, comprendre plus profondément pourquoi ceux-ci fonctionnent si bien en pratique reste un mystère. Par exemple, plutôt que de passer du temps à chercher intelligemment une solution, les méthodes actuelles préfèrent aller le plus rapidement possible vers l'échec pour prendre ensuite le temps de l'analyser. Partant d'une approche de parcours systématique de l'espace des solutions, assez simple à appréhender, elles s’enrichissent de techniques d'apprentissages fondées sur les échecs passés, de politiques de redémarrages de nouvelle recherches extrêmement fréquentes, et de méthodes d'oubli de l'information apprise de plus en plus agressives. Ce faisant, les démonstrateurs SAT sont devenus des systèmes de science expérimentale quasiment impossible à comprendre par une analyse algorithmique classique. Pour finir, nous montrerons à quel point les solutions actuelles, bien que redoutablement efficaces, butent encore sur une question épineuse : comment utiliser au mieux les architectures parallèles pour mieux résoudre SAT.