Satisfiability Modulo Theories (SMT)

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

La Satisfaisabilité 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 sont la théorie des nombres réels, la théorie de entiers linéaires, et des théories de diverses structures de données comme les listes, les tableaux, les vecteurs de bits, etc., ainsi que des combinaisons de celles-ci.

Terminologie[modifier | modifier le code]

Formellement, une instance SMT est une formule du premier ordre sans quantificateurs. Le problème SMT est de déterminer si une telle formule est satisfaisable. 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 coeurs principaux : un solveur SAT et une (ou plusieurs) procédures de décisions de la théorie modulo. Une instance SMT, dans laquelle les prédicats sont remplacés par des variables booléennes et dont la nouvelle formule obtenue est SAT, n'est pas forcément SAT 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 à une certaine instance SMT F donnée:

  1. Remplacement des prédicats et contraintes de F par des variables booléennes
  2. Demander au solveur SAT un modèle M de satisfaisabilité
    1. Si il n'existe pas de modèle SAT, la formule F est ni SAT, ni SAT modulo théorie
    2. Sinon, remplacer dans M les variables par les prédicats de l'étape 1
  3. Vérifier la cohérence du modèle par la procédure de décision de la théorie
    1. Si le modèle est cohérent, la formule F est dont satisfaisable modulo théorie et le modèle est explicité.
    2. Sinon, recommencer à l'étape 1 avec la formule F ∧ ¬M

Solveurs SMT[modifier | modifier le code]

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.

Liens externes[modifier | modifier le code]