Description
Le problème NP-complet classique de la satisfiabilité d'une formule Booléenne mise sous forme normale conjonctive a connu un intérêt croissant non seulement dans la communauté d'informatique théorique, mais aussi dans des domaines d'applications divers ou une solution pratique à ce problème permet des avancées significatives. Depuis les premiers développements de la procédure de base proposée par Davis, Putnam, Logemann et Loveland (DPLL), il y a plus d'une quarantaine d'années, ce domaine a connu un effort de recherche croissant ayant abouti aux solveurs SAT modernes d'aujourd'hui, capable de résoudre des instances de plusieurs centaines de milliers et même de millions de variables. Dans cet exposé, nous examinerons les idées principales ayant permis ce passage à l'échelle et nous évoquerons quelques directions possibles pour des recherches futures.