Le solveur Z3, développé par Microsoft Research, constitue l’un des outils de référence
pour la satisfiabilité modulo théories (SMT). Son interface Python permet de modéliser des
problèmes combinatoires, arithmétiques et logiques au moyen de contraintes déclaratives,
puis d’en déduire automatiquement une solution, une preuve d’insatisfiabilité ou un contre-
exemple. Cet article présente les fondements logiques de Z3, les principales constructions
du module Python, ainsi que plusieurs schémas de modélisation utiles en recherche et en
ingénierie logicielle.