Formalisation de calcul de logique avec Isabelle/HOL

I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach.I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop.Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.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