Satisfiability Modulo Theories (SMT)
Un article de Wikipédia, l'encyclopédie libre.
Problème SMT (Satisfiability Modulo Theories) est un problème de la décision pour les formules logiques dans le respect d'une théorie exprimée dans la logique du premier ordre contenant l'égalité. Des exemples de théories sont la théorie des nombres réels, la théorie de entiers linéaires, et des théories d'une variété de structures de données comme les listes, les tableaux, les vecteurs de bits, etc.
[modifier] Terminologie
Formellement, une instance SMT est une formule du premier ordre libre de quantificateur. Le problème SMT est de problème de déterminer si une telle formule est satisfiable. En d'autres mots, imaginons une instance de SAT dans laquelle les variables booléennes sont remplacées par des prédicats. Ces prédicats étant classés selon la théorie à laquelle ils appartiennent.
[modifier] Solveurs SMT
Les solveurs SMT permettent de résoudre les problèmes SMT. L'architecture des solveurs SMT est divisée comme suit : le solveur SAT basé sur l'algorithme DPLL (solveur SAT) résout la partie booléenne du problème et interagit avec le solveur T pour propager ses solutions. Le solveur T vérifie la satisfiabilité des conjonctions de prédicats de théorie T. Pour des raisons d'efficacité, on souhaite généralement que le solveur de théorie participe à la propagation et à l'analyse de conflits.
