Ce module présente un certain nombre d'applications de la satisfiabilité modulo la théorie des inégalités linéaires (SMT)

Ce module décrit comment une règle appelée Résolution permet de déterminer si une formule propositionnelle en forme normale conjonctive (CNF) est insatisfaisante. Il est montré comment une approche appelée DPLL fait le même travail, et comment elle est liée à la résolution. Enfin, nous montrons comment les solveurs SAT actuels implémentent et optimisent essentiellement la DPLL.

Ce module se compose de deux parties. La première partie concerne la transformation de formules propositionnelles arbitraires en CNF, conduisant à la transformation de Tseitin qui effectue ce travail de telle sorte que la taille de la formule transformée est linéaire par rapport à la taille de la formule originale. La deuxième partie concerne l'extension de SAT à SMT, en particulier pour traiter les inégalités linéaires. Il est montré comment la méthode du Simplex pour l'optimisation linéaire sert à cette fin ; la méthode du Simplex elle-même est expliquée en détail.