Satisfiability Modulo Theories (SMT)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La Satisfiabilité Modulo Théories (SMT) est un problème de décision pour des formules logiques, par rapport à des théories sous-jacentes exprimées dans la logique classique du premier ordre avec égalité. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les vecteurs de bits, ainsi que des combinaisons de celles-ci.

Terminologie[modifier | modifier le code]

Formellement, une instance de SMT est une formule du premier ordre sans quantificateur. Le problème SMT est 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.

Fonctionnement de base[modifier | modifier le code]

Les solveurs SMT fonctionnent autour de deux cœurs principaux : un solveur SAT et une ou plusieurs procédures de décision de la théorie. Une instance de SMT, même si elle est satisfiable lorsqu’elle est vue comme une instance de SAT (obtenue en remplaçant les prédicats par des variables booléennes), n'est pas forcément satisfiable modulo une certaine théorie. Il s'agit alors de demander des modèles SAT au solveur SAT puis de vérifier leur cohérence par les procédures de décision de la théorie. Le fonctionnement général d'un solveur SMT est décrit de la manière suivante pour une instance de SMT F donnée.

  1. Remplacer les prédicats et contraintes de F par des variables booléennes.
  2. Demander au solveur SAT un modèle de satisfiabilité M.
    • S’il n'existe pas de modèle SAT, alors la formule F n’est pas satisfiable, donc pas satisfiable modulo la théorie.
    • Sinon,
      1. Remplacer dans M les variables par les prédicats de l'étape 1.
      2. Vérifier la cohérence du modèle par la procédure de décision de la théorie.
        • Si le modèle est cohérent, alors la formule F est satisfiable modulo la théorie et le modèle est explicité.
        • Sinon, recommencer à l'étape 1 avec la formule F ∧ ¬M.

L'architecture des solveurs SMT est donc divisée comme suit : le solveur SAT basé sur l'algorithme DPLL résout la partie booléenne du problème et interagit avec le solveur de la théorie pour propager ses solutions. Ce dernier vérifie la satisfiabilité des conjonctions de prédicats de la théorie. Pour des raisons d'efficacité, on souhaite généralement que le solveur de la théorie participe à la propagation et à l'analyse des conflits.

Solveurs SMT[modifier | modifier le code]

Voici des exemples de solveurs SMT :

Liens externes[modifier | modifier le code]