Satisfiability modulo theories

En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. 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 tableaux de bits, ainsi que des combinaisons de celles-ci. Formellement, une instance de SMT est une formule du premier ordre sans quantificateur. Par exemple : 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. 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.