Résumé
En matière de calcul Booléen, il y a trois problèmes principaux : le codage de fonctions Booléennes, la satisfiabilité d’une formule pour au moins un jeu de valeurs des variables, appelée le problème SAT, et sa validité pour toutes les valeurs des variables, équivalente à la non-satisfiabilité de sa négation. Si les BDDs présentés au cours précédents sont devenus le standard pour la représentation de fonctions, ils sont moins efficaces pour la satisfiabilité car ils calculent trop d’information : un BDD encode en fait tous les vecteurs de valeurs des variables qui rendent une formule vraie, alors qu’il suffit d’en trouver un seul pour garantir la satisfiabilité. Les premiers algorithmes SAT, nés dans les années 1960, étaient fondés soit sur l’élimination de variables par suite de résolution logique d’une variable contre ses opposés, soit par l’exploration systématique des valeurs des variables. Ces algorithmes sont fondamentalement exponentiels dans les pire cas, et le sont souvent en pratique. En 1972, Cook a caractérisé la classe de complexité NP et montré que SAT est le prototype du problème NP-complet, ce qui explique que sa solution a été longtemps jugée impossible en pratique.
Cependant, depuis les années 2000, une barrière a sauté : de nouveaux algorithmes sont apparus, améliorant considérablement la recherche de solution et mêlant recherche systématique et résolution. Même si leurs pires cas restent exponentiels, ces algorithmes constamment perfectionnés permettent désormais de résoudre des problèmes SAT sur des formules issues d’exemples concrets et comportant des centaines de milliers voire des millions de variables, ce qui était tout à fait impensable il y a seulement 15 ans. Ils sont maintenant utilisés très largement dans l’industrie, tout particulièrement en vérification de modèles et en génération de tests pour les circuits et les programmes embarqués, avec un rôle essentiel pour la preuve de conformité des transformations conduisant d’une spécification de haut niveau d’un circuit en composants électroniques intégrés. Une compétition mondiale régulière a joué un rôle essentiel dans l’élaboration et le réglage de ces algorithmes, qui restent largement empiriques car on ne sait pas encore vraiment pourquoi ils marchent si bien en pratique.
