Satisfiability Modulo Theories (SMT)
- Satisfiability Modulo Theories (SMT)
-
Problème SMT (Satisfiability Modulo Theories) est un problème de la décision pour les formules logiques dans le respect d'une théorie exprimée dans la logique du premier ordre contenant l'é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 d'une variété de structures de données comme les listes, les tableaux, les vecteurs de bits, etc.
Terminologie
Formellement, une instance SMT est une formule du premier ordre libre de quantificateur. Le problème SMT est de problème 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.
Solveurs SMT
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
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Satisfiability Modulo Theories (SMT) de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
Satisfiability Modulo Theories — (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first order logic with equality. Examples of theories typically used in computer science are the theory of real… … Wikipedia
Satisfiability Modulo Theories — В программировании, Satisfiability Modulo Theories (SMT) это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT формул являются: теории целых и вещественных чисел, теории списков,… … Википедия
SMT — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Sigles d’une seule lettre Sigles de deux lettres > Sigles de trois lettres Sigles de quatre lettres … Wikipédia en Français
SMT — ist die Abkürzung für: Sauerstoff Mehrschritt Therapie Shanghai Maglev Train, siehe Transrapid Shanghai Simultaneous Multithreading Sowjetisches Militärtribunal, siehe Militärgericht#Sowjetische Militärtribunale, Rote Armee Surface Mounted… … Deutsch Wikipedia
SMT — may refer to:*Satisfiability Modulo Theories *Statistical machine translation *Scottish Motor Traction, a former bus company in Scotland *Sequential manual transmission *Shanghai Maglev Train *Shin Megami Tensei *Simple motor tic *Simultaneous… … Wikipedia
Boolean satisfiability problem — For the concept in mathematical logic, see Satisfiability. 3SAT redirects here. For the Central European television network, see 3sat. In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of… … Wikipedia
Beaver Bit-vector Decision Procedure — Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier free finite precision bit vector arithmetic ( [http://combination.cs.uiowa.edu/smtlib/logics/QF BV.smt QF BV] ). Its prototype implementation… … Wikipedia
Constraint satisfaction problem — Constraint satisfaction problems (CSP)s are mathematical problems defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite… … Wikipedia
Constraint programming — Programming paradigms Agent oriented Automata based Component based Flow based Pipelined Concatenative Concurrent computin … Wikipedia
Решатель — (англ. solver) программное обеспечение, предназначенное для решения рассматриваемой математической задачи. На вход решателю поступает описание задачи в некоторой заданной форме, а на выходе он выдает решение задачи. Виды решаемых задач … Википедия
