Satisfiability modulo theories

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Ce modèle est-il pertinent ? Cliquez pour en voir d'autres.
Cet article ne cite pas suffisamment ses sources (septembre 2014).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références » (modifier l'article, comment ajouter mes sources ?).

La satisfiabilité modulo théories (SMT) est un problème de décision pour des formules logiques du premier ordre sans quantificateurs, par rapport à une théorie sous-jacente exprimée 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.

Instance d'un problème SMT[modifier | modifier le code]

Formellement, une instance de SMT est une formule du premier ordre sans quantificateur. Par exemple ː

est une formule du premier ordre sans quantificateur.

Le problème SMT est de déterminer si une telle formule est satisfiable par rapport à une théorie sous-jacente. Par exemple, on peut se demander si la formule ci-dessus est satisfiable par rapport à la théorie des nombres réels. Autrement dit, il s'agit de savoir si l'on peut trouver des nombres réels pour les variables x et y qui rendent la formule ci-dessus vraie.

On peut voir une instance d'un problème SMT comme une instance du problème de satisfiabilité de la logique propositionnelle dans laquelle les variables booléennes sont remplacées par des formules atomiques. Par exemple, la formule ci-dessus est la formule propositionnelle dans laquelle on a remplacé les variables booléennes p, q, r, s par des formules atomiques.

Fonctionnement de base d'un solveur SMT[modifier | modifier le code]

Un solveur SMT fonctionne autour de deux cœurs principaux : un solveur SAT et une ou plusieurs procédures de décision de la théorie. L'idée est de tester si la formule propositionnelle correspondante (obtenue en remplaçant les prédicats par des variables booléennes) est satisfiable via un solveur SAT. Mais une instance de SMT, même si elle est satisfiable lorsqu’elle est vue comme une instance de SAT, n'est pas forcément satisfiable modulo une certaine théorie. Par exemple, n'est pas satisfiable par rapport à la théorie des réels, pourtant l'instance de SAT correspondante, p, est satisfiable. C'est pourquoi on vérifie ensuite la cohérence avec des procédures de décision de la théorie. S'il y a cohérence, on a effectivement une formule satisfiable. Sinon, on enrichit la formule initiale avec de l'information qui représente l'incohérence. Plus précisément, 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.

Applications[modifier | modifier le code]

Solveurs SMT[modifier | modifier le code]

Voici des exemples de solveurs SMT :

Liens externes[modifier | modifier le code]