J'ai développé un framework pour le problème de satisfaisabilité booléenne avec la procédure CDCL (conflict-driven clause learning) avec l'assistant de preuve Isabelle/HOL. Le framework offre un moyen pratique de prouver des meta-théorèmes and expérimenter avec des variantes, y compris la procédure DPLL (Davis-Putnam-Logemann-Loveland). L'un des impacts les plus importants de mon travail est l'inclusion des règle pour oublier et rédemarrer, et l'approche par raffinement. J'ai utilisé ma formalisation pour développer trois extension: d'abord une extension incrémental de CDCL; ensuite, une variante optimisante de CDCL (OCDCL), qui à partir d'une fonction de coût sur les littéraux, OCDCL trouve un modèle do coût optimal; et j'ai également travaillé sur du model covering. Grâce au framework que j'ai pu réutiliser, ces extensions étaient simples à développer. Par une chaîne de raffinement, je connecte le calcul abstrait de CDCL, d'abord pour un calcul plus concret, puis vers un SAT solveur exprimé dans un langage de programmation fonctionnelle, et finalement vers un SAT solveur dans un langaqe de programmation impératif avec une garantie de correction totale. La version impérative utilise la structure de donnée «two-watched literals» et d'autres optimisations que l'on trouve dans les SAT solveurs modernes. J'utilise le «Isabelle Refinement Framework» pour automatiser les pas de raffinement. Ensuite, j'étends ce travail avec des optimisations comme les «blocking literals» et l'usage d'entiers natifs le plus longtemps possible, avant d'utiliser des entiers non-bornés afin de garantir la complétude.