Satisfaisant modulo les théories

En informatique et en logique mathématique , la satisfiabilité modulo théories ( SMT ) est le problème consistant à déterminer si une formule mathématique est satisfiable . Elle généralise le problème de satisfiabilité booléenne (SAT) à des formules plus complexes impliquant des nombres réels , des entiers et/ou diverses structures de données telles que des listes , des tableaux , des vecteurs de bits et des chaînes . Le nom est dérivé du fait que ces expressions sont interprétées dans le cadre (« modulo ») d'une certaine théorie formelle en logique du premier ordre avec égalité (interdisant souvent les quantificateurs ). Les solveurs SMT sont des outils qui visent à résoudre le problème SMT pour un sous-ensemble pratique d'entrées. Les solveurs SMT tels que Z3 et cvc5 ont été utilisés comme élément de base pour une large gamme d'applications en informatique, notamment dans la démonstration automatique de théorèmes , l'analyse de programmes , la vérification de programmes et les tests de logiciels .

La satisfiabilité booléenne étant déjà NP-complète , le problème SMT est généralement NP-difficile et, pour de nombreuses théories, il est indécidable . Les chercheurs étudient les théories ou sous-ensembles de théories qui conduisent à un problème SMT décidable et la complexité de calcul des cas décidables. Les procédures de décision qui en résultent sont souvent implémentées directement dans les solveurs SMT ; voir, par exemple, la décidabilité de l'arithmétique de Presburger . Le SMT peut être considéré comme un problème de satisfaction de contraintes et donc comme une certaine approche formalisée de la programmation par contraintes .

Formellement parlant, une instance SMT est une formule en logique du premier ordre , où certains symboles de fonction et de prédicat ont des interprétations supplémentaires, et SMT est le problème de déterminer si une telle formule est satisfaisable. En d'autres termes, imaginez une instance du problème de satisfiabilité booléenne (SAT) dans laquelle certaines des variables binaires sont remplacées par des prédicats sur un ensemble approprié de variables non binaires. Un prédicat est une fonction à valeur binaire de variables non binaires. Les exemples de prédicats incluent les inégalités linéaires (par exemple, ) ou les égalités impliquant des termes non interprétés et des symboles de fonction (par exemple, où est une fonction non spécifiée de deux arguments). Ces prédicats sont classés en fonction de chaque théorie respective attribuée. Par exemple, les inégalités linéaires sur des variables réelles sont évaluées à l'aide des règles de la théorie de l'arithmétique réelle linéaire , tandis que les prédicats impliquant des termes non interprétés et des symboles de fonction sont évalués à l'aide des règles de la théorie des fonctions non interprétées avec égalité (parfois appelée théorie vide ). D'autres théories incluent les théories des tableaux et des structures de listes (utiles pour la modélisation et la vérification des programmes informatiques ), et la théorie des vecteurs de bits (utile pour la modélisation et la vérification des conceptions matérielles ). Des sous-théories sont également possibles : par exemple, la logique différentielle est une sous-théorie de l'arithmétique linéaire dans laquelle chaque inégalité est limitée à la forme pour les variables et et constante . $cx-\mathrm{et}>c$c}" data-src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f1e5d7d28050c4f73c5e3bd642dcda484b2e214e">

Les exemples ci-dessus illustrent l'utilisation de l'arithmétique linéaire sur les nombres entiers pour résoudre des inégalités. D'autres exemples incluent :

• Satisfaisant : Déterminer si c'est satisfaisable.
• Accès au tableau : recherchez une valeur pour le tableau A telle que A[0]=5.
• Arithmétique vectorielle binaire : Déterminer si x et y sont des nombres distincts de 3 bits.
• Fonctions non interprétées : Trouver des valeurs pour x et y telles que et .

La plupart des solveurs SMT ne prennent en charge que les fragments sans quantificateur de leur logique.

Il existe un chevauchement substantiel entre la résolution SMT et la démonstration automatique de théorèmes (ATP). En général, les démonstrateurs de théorèmes automatiques se concentrent sur la prise en charge de la logique complète du premier ordre avec des quantificateurs, tandis que les solveurs SMT se concentrent davantage sur la prise en charge de diverses théories (symboles de prédicats interprétés). Les ATP excellent dans les problèmes avec de nombreux quantificateurs, tandis que les solveurs SMT réussissent bien sur les grands problèmes sans quantificateurs. La ligne est suffisamment floue pour que certains ATP participent à SMT-COMP, tandis que certains solveurs SMT participent à CASC .

Une instance SMT est une généralisation d'une instance SAT booléenne dans laquelle divers ensembles de variables sont remplacés par des prédicats issus de diverses théories sous-jacentes. Les formules SMT fournissent un langage de modélisation beaucoup plus riche que celui des formules SAT booléennes. Par exemple, une formule SMT permet de modéliser les opérations de chemin de données d'un microprocesseur au niveau du mot plutôt qu'au niveau du bit.

En comparaison, la programmation par ensemble de réponses est également basée sur des prédicats (plus précisément, sur des phrases atomiques créées à partir de formules atomiques ). Contrairement à la SMT, les programmes par ensemble de réponses n'ont pas de quantificateurs et ne peuvent pas facilement exprimer des contraintes telles que l'arithmétique linéaire ou la logique différentielle. La programmation par ensemble de réponses est mieux adaptée aux problèmes booléens qui se réduisent à la théorie libre des fonctions non interprétées. L'implémentation d'entiers 32 bits sous forme de vecteurs de bits dans la programmation par ensemble de réponses souffre de la plupart des mêmes problèmes que ceux rencontrés par les premiers solveurs SMT : les identités « évidentes » telles que x + y = y + x sont difficiles à déduire.

La programmation logique par contraintes prend en charge les contraintes arithmétiques linéaires, mais dans un cadre théorique complètement différent. Les solveurs SMT ont également été étendus pour résoudre des formules en logique d'ordre supérieur .

Les premières tentatives de résolution des instances SMT consistaient à les traduire en instances SAT booléennes (par exemple, une variable entière de 32 bits serait codée par 32 variables à un bit avec des poids appropriés et des opérations au niveau du mot telles que « plus » seraient remplacées par des opérations logiques de niveau inférieur sur les bits) et à transmettre cette formule à un solveur SAT booléen. Cette approche, appelée approche avide ( ou bitblasting ), a ses mérites : en prétraitant la formule SMT en une formule SAT booléenne équivalente, les solveurs SAT booléens existants peuvent être utilisés « tels quels » et leurs améliorations de performances et de capacité peuvent être exploitées au fil du temps. D'autre part, la perte de la sémantique de haut niveau des théories sous-jacentes signifie que le solveur SAT booléen doit travailler beaucoup plus dur que nécessaire pour découvrir des faits « évidents » (comme pour l'addition d'entiers). Cette observation a conduit au développement d'un certain nombre de solveurs SMT qui intègrent étroitement le raisonnement booléen d'une recherche de style DPLL avec des solveurs spécifiques à la théorie ( T-solvers ) qui gèrent les conjonctions (AND) de prédicats d'une théorie donnée. Cette approche est appelée l' approche paresseuse .

Baptisée DPLL(T) [ cette architecture confie la responsabilité du raisonnement booléen au solveur SAT basé sur DPLL qui, à son tour, interagit avec un solveur pour la théorie T via une interface bien définie. Le solveur de théorie n'a qu'à se soucier de vérifier la faisabilité des conjonctions de prédicats de théorie qui lui sont transmises par le solveur SAT lorsqu'il explore l'espace de recherche booléen de la formule. Pour que cette intégration fonctionne bien, cependant, le solveur de théorie doit être capable de participer à l'analyse de propagation et de conflit, c'est-à-dire qu'il doit être capable de déduire de nouveaux faits à partir de faits déjà établis, ainsi que de fournir des explications succinctes de l'infaisabilité lorsque des conflits théoriques surviennent. En d'autres termes, le solveur de théorie doit être incrémental et rétroactif .

Les chercheurs étudient les théories ou sous-ensembles de théories qui conduisent à un problème SMT décidable et la complexité computationnelle des cas décidables. Étant donné que la logique du premier ordre complète n'est que semi-décidable , une ligne de recherche tente de trouver des procédures de décision efficaces pour des fragments de logique du premier ordre tels que la logique propositionnelle effective .

Une autre ligne de recherche implique le développement de théories décidables spécialisées , y compris l'arithmétique linéaire sur les rationnels et les entiers , les vecteurs de bits à largeur fixe, l'arithmétique à virgule flottante (souvent implémentée dans les solveurs SMT via le bit-blasting , c'est-à-dire la réduction aux vecteurs de bits), les chaînes , les (co)-types de données , les séquences (utilisées pour modéliser les tableaux dynamiques ), les ensembles et relations finis , la logique de séparation , les corps finis , et les fonctions non interprétées entre autres.

Les théories booléennes monotones sont une classe de théories qui prennent en charge la propagation efficace de la théorie et l'analyse des conflits, permettant une utilisation pratique dans les solveurs DPLL(T). Les théories monotones ne prennent en charge que les variables booléennes (booléennes est le seul type ), et toutes leurs fonctions et prédicats p obéissent à l'axiome

Les exemples de théories monotones incluent l'accessibilité des graphes , la détection de collision pour les enveloppes convexes , les coupes minimales et la logique de l'arbre de calcul . Chaque programme Datalog peut être interprété comme une théorie monotone.

La plupart des approches SMT courantes prennent en charge les théories décidables . Cependant, de nombreux systèmes du monde réel, tels qu'un avion et son comportement, ne peuvent être modélisés qu'au moyen d'une arithmétique non linéaire sur les nombres réels impliquant des fonctions transcendantes . Ce fait motive une extension du problème SMT aux théories non linéaires, comme la détermination de la satisfaisabilité de l'équation suivante :

où

De tels problèmes sont cependant indécidables en général. (D'un autre côté, la théorie des corps réels fermés , et donc la théorie complète du premier ordre des nombres réels , sont décidables en utilisant l'élimination des quantificateurs . Cela est dû à Alfred Tarski .) La théorie du premier ordre des nombres naturels avec addition (mais pas multiplication), appelée arithmétique de Presburger , est également décidable. Comme la multiplication par des constantes peut être implémentée sous forme d'additions imbriquées, l'arithmétique de nombreux programmes informatiques peut être exprimée en utilisant l'arithmétique de Presburger, ce qui donne des formules décidables.

Des exemples de solveurs SMT traitant des combinaisons booléennes d'atomes de théorie à partir de théories arithmétiques indécidables sur les réels sont ABsolver, qui utilise une architecture DPLL(T) classique avec un paquet d'optimisation non linéaire comme solveur de théorie subordonné (nécessairement incomplet), iSAT, s'appuyant sur une unification de la résolution DPLL SAT et de la propagation de contraintes d'intervalle appelée algorithme iSAT, et cvc5 .

Le tableau ci-dessous résume certaines des fonctionnalités des nombreux solveurs SMT disponibles. La colonne « SMT-LIB » indique la compatibilité avec le langage SMT-LIB ; de nombreux systèmes marqués « oui » peuvent ne prendre en charge que les anciennes versions de SMT-LIB ou n'offrir qu'une prise en charge partielle du langage. La colonne « CVC » indique la prise en charge du langage CVC . La colonne « DIMACS » indique la prise en charge du format DIMACS .

Les projets diffèrent non seulement par leurs fonctionnalités et leurs performances, mais également par la viabilité de la communauté environnante, son intérêt continu pour un projet et sa capacité à contribuer à la documentation, aux correctifs, aux tests et aux améliorations.

Il existe plusieurs tentatives pour décrire une interface standardisée pour les solveurs SMT (et les démonstrateurs de théorèmes automatisés , un terme souvent utilisé comme synonyme). La plus connue est la norme SMT-LIB, qui fournit un langage basé sur les expressions S. D'autres formats standardisés couramment pris en charge sont le format DIMACS pris en charge par de nombreux solveurs SAT booléens, et le format CVC utilisé par le démonstrateur de théorèmes automatisé CVC.

Le format SMT-LIB est également accompagné d'un certain nombre de repères standardisés et a permis l'organisation d'une compétition annuelle entre les solveurs SMT appelée SMT-COMP. Initialement, la compétition a eu lieu lors de la conférence sur la vérification assistée par ordinateur (CAV), mais depuis 2020, la compétition est organisée dans le cadre de l'atelier SMT, qui est affilié à la Conférence internationale conjointe sur le raisonnement automatisé (IJCAR).

Les solveurs SMT sont utiles à la fois pour la vérification, pour prouver l' exactitude des programmes, pour tester des logiciels basés sur l'exécution symbolique , et pour la synthèse , pour générer des fragments de programmes en recherchant dans l'espace des programmes possibles. En dehors de la vérification de logiciels, les solveurs SMT ont également été utilisés pour l'inférence de type et pour la modélisation de scénarios théoriques, y compris la modélisation des croyances des acteurs dans le contrôle des armes nucléaires .

La vérification assistée par ordinateur des programmes informatiques utilise souvent des solveurs SMT. Une technique courante consiste à traduire les préconditions, les postconditions, les conditions de boucle et les assertions en formules SMT afin de déterminer si toutes les propriétés peuvent être vérifiées.

Il existe de nombreux vérificateurs construits sur le solveur SMT Z3 . Boogie est un langage de vérification intermédiaire qui utilise Z3 pour vérifier automatiquement les programmes impératifs simples. Le vérificateur VCC pour C concurrent utilise Boogie, ainsi que Dafny pour les programmes impératifs basés sur des objets, Chalice pour les programmes concurrents et Spec# pour C#. F* est un langage typé de manière dépendante qui utilise Z3 pour trouver des preuves ; le compilateur transporte ces preuves pour produire un bytecode porteur de preuves. L'infrastructure de vérification Viper encode les conditions de vérification en Z3. La bibliothèque sbv fournit une vérification basée sur SMT des programmes Haskell et permet à l'utilisateur de choisir parmi un certain nombre de solveurs tels que Z3, ABC, Boolector, cvc5, MathSAT et Yices.

Il existe également de nombreux vérificateurs construits sur le solveur Alt-Ergo SMT. Voici une liste d'applications matures :

• Why3, une plateforme de vérification de programmes déductive, utilise Alt-Ergo comme principal démonstrateur ;
• CAVEAT, un C-verifier développé par le CEA et utilisé par Airbus ; Alt-Ergo a été inclus dans la qualification DO-178C d'un de ses avions récents ;
• Frama-C , un framework pour analyser le code C, utilise Alt-Ergo dans les plugins Jessie et WP (dédiés à la « vérification déductive des programmes ») ;
• SPARK utilise CVC4 et Alt-Ergo (derrière GNATprove) pour automatiser la vérification de certaines assertions dans SPARK 2014 ;
• L'Atelier-B peut utiliser Alt-Ergo à la place de son prouveur principal (augmentant le succès de 84% à 98% sur les benchmarks du projet ANR Bware) ;
• Rodin , un framework de méthode B développé par Systerel, peut utiliser Alt-Ergo comme back-end ;
• Cubicle, un vérificateur de modèles open source pour vérifier les propriétés de sécurité des systèmes de transition basés sur des réseaux.
• EasyCrypt, un ensemble d'outils permettant de raisonner sur les propriétés relationnelles des calculs probabilistes avec du code contradictoire.

De nombreux solveurs SMT implémentent un format d'interface commun appelé SMTLIB2 (ces fichiers ont généralement l'extension " .smt2"). L'outil LiquidHaskell implémente un vérificateur basé sur le type de raffinement pour Haskell qui peut utiliser n'importe quel solveur compatible SMTLIB2, par exemple cvc5, MathSat ou Z3.

Une application importante des solveurs SMT est l'exécution symbolique pour l'analyse et le test de programmes (par exemple, les tests concoliques ), visant notamment à trouver des vulnérabilités de sécurité. Les exemples d'outils dans cette catégorie incluent SAGE de Microsoft Research , KLEE, S2E et Triton. Les solveurs SMT qui ont été utilisés pour des applications d'exécution symbolique incluent Z3, STP , la famille de solveurs Z3str et Boolector.

Les solveurs SMT ont été intégrés à des assistants de preuve, notamment Coq et Isabelle/HOL .