Satisfiability Modulo Theories

Satisfiability Modulo Theories

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 numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on.

Basic terminology

Formally speaking, an SMT instance is a formula in first-order logic, where some function and predicate symbols have additional interpretations, and SMT is the problem of determining whether such a formula is satisfiable. In other words, imagine an instance of the Boolean satisfiability problem (SAT) in which some of the binary variables are replaced by predicates over a suitable set of non-binary variables. A predicate is basically a binary-valued function of non-binary variables. Example predicates include linear inequalities (e.g., 3x+ 2y - z geq 4) or equalities involving so-called uninterpreted terms and function symbols (e.g., f(f(u, v), v) = f(u, v) where f is some unspecified function of two unspecified arguments.) These predicates are classified according to the theory they belong to. For instance, linear inequalities over real variables are evaluated using the rules of the theory of linear real arithmetic, whereas predicates involving uninterpreted terms and function symbols are evaluated using the rules of the theory of uninterpreted functions with equality (sometimes referred to as the empty theory [http://www.csl.sri.com/users/demoura/smt-comp/introduction.shtml] ). Other theories include the theories of arrays and list structures (useful for modeling and verifying software programs), and the theory of bit vectors (useful in modeling and verifying
hardware designs). Subtheories are also possible: for example, difference logic is a sub-theory of linear arithmetic in which each inequality is restricted to have the form x - y leq c for variables x and y and constant c.

Most SMT solvers support only quantifier free fragments of their logics.

Expressive power of SMT

An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories. Obviously, SMT formulas provide a much richer modeling language than is possible with Boolean SAT formulas. For example, an SMT formula allows us to model the datapath operations of a microprocessor at the word rather than the bit level.

MT solvers

Early attempts for solving SMT instances involved translating them to Boolean SAT instances (e.g., a 32-bit integer variable would be encoded by 32 bit variables with appropriate weights and word-level operations such as 'plus' would be replaced by lower-level logic operations on the bits) and passing this formula to a Boolean SAT solver. This approach has its merits: by pre-processing the SMT formula into an equivalent Boolean SAT formula we can use existing Boolean SAT solvers "as-is" and leverage their performance and capacity improvements over time. On the other hand, the loss of the high-level semantics of the underlying theories means that the Boolean SAT solver has to work a lot harder than necessary to discover "obvious" facts (such as x + y = y + x for integer addition.) This observation led to the development of a number of SMT solvers that tightly integrate the Boolean reasoning of a DPLL-style search with theory-specific solvers that handle conjunctions (ANDs) of predicates from a given theory.

Dubbed DPLL(T), this architecture gives the responsibility of Boolean reasoning to the DPLL-based SAT solver which, in turn, interacts with a solver for theory T through a well-defined interface. The theory solver need only worry about checking the feasibility of conjunctions of theory predicates passed on to it from the SAT solver as it explores the Boolean search space of the formula. For this integration to work well, however, the theory solver must be able to participate in propagation and conflict analysis, i.e., it must be able to infer new facts from already established facts, as well as to supply succinct explanations of infeasibility when theory conflicts arise. In other words, the theory solver must be incremental and backtrackable.

CVC (for Cooperating Validity Checker) is an automatic theorem prover for the Satisfiability Modulo Theories problem.It was developed originally by the [http://verify.stanford.edu Stanford Verification Group] as a successor to the [http://verify.stanford.edu/SVC/ Stanford Validity Checker] , but is now maintained primarily by researchers at New York University and the University of Iowa. Its latest release is version 3.0 or CVC3. Previous releases were called CVC Lite (v2.0) and CVC (v1.0).

MT for undecidable theories

Most of the common SMT approaches support decidable theories. However, many real-world systems can only be modelled by means of non-linear arithmetic over the real numbers involving transcendental functions, e.g. an aircraft and its behavior. This fact motivates an extension of the SMT problem to non-linear theories, e.g. determine whether

: egin{align}& (sin(x)^3 = cos(log(y)cdot x) vee b vee -x^2 geq 2.3y) \& wedge left( eg b vee y < -34.4 vee exp(x) > {y over x} ight)end{align}

where

: b in {mathbb B}, x,y in {mathbb R}

is satisfiable. Then, such problems become undecidable in general. (It is important to note, however, that the theory of real closed fields, and thus the full first order theory of the real numbers, are decidable. This is due to Alfred Tarski.)

Examples of SMT solvers addressing Boolean combinations of theory atoms from undecidable arithmetic theories over the reals are ABsolver Harv|Bauer|Pister|Tautschnig|2007, which employs a classical DPLL(T) architecture with a non-linear optimization packet as (necessarily incomplete) subordinate theory solver, and HySAT-2, building on a unification of DPLL SAT-solving and interval constraint propagation called the iSAT algorithm Harv|Fränzle|Herde|Ratschan|Schubert|2007.

External links

* [http://combination.cs.uiowa.edu/smtlib/ SMT-LIB: The Satisfiability Modulo Theories Library]
* [http://www.smtcomp.org SMT-COMP: The Satisfiability Modulo Theories Competition]
* [http://www.decision-procedures.org: Decision procedures - an algorithmic point of view]

MT solvers

* [http://absolver.sourceforge.net/ ABsolver]
* [http://www.lsi.upc.edu/~oliveras/bclt-main.html Barcelogic]
* [http://www.eecs.berkeley.edu/~jha/beaver.html Beaver]
* [http://fmv.jku.at/boolector/index.html Boolector]
* [http://www.cs.nyu.edu/acsys/cvc3/ CVC3]
* [http://sourceforge.net/projects/dpt The Decision Procedure Toolkit (DPT)]
* [http://ergo.lri.fr/ Ergo]
* [http://hysat.informatik.uni-oldenburg.de/ HySAT]
* [http://mathsat4.disi.unitn.it/ MathSAT]
* [http://www.cs.ubc.ca/~babic/index_spear.htm Spear]
* [http://yices.csl.sri.com/ Yices]
* [http://research.microsoft.com/projects/z3/ Z3]

References

# Citation
first = A.
last = Bauer
authorlink =
first2 = M.
last2 = Pister
first3 = M.
last3 = Tautschnig
contribution = Tool-support for the analysis of hybrid systems and models
title = Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07)
publisher = IEEE Computer Society
date = 2007
doi = 10.1109/DATE.2007.364411

# R. E. Bryant, S. M. German, and M. N. Velev, "Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions," in Analytic Tableaux and Related Methods, pp. 1&ndash;13, 1999.
# M. Davis and H. Putnam, doi-inline|10.1145/321033.321034|A Computing Procedure for Quantification Theory, Journal of the Association for Computing Machinery, vol. 7, no., pp. 201&ndash;215, 1960.
# M. Davis, G. Logemann, and D. Loveland, doi-inline|10.1145/368273.368557|A Machine Program for Theorem-Proving, Communications of the ACM, vol. 5, no. 7, pp. 394&ndash;397, 1962.
# Citation
first = M.
last = Fränzle
first2 = C.
last2 = Herde
first3 = S.
last3 = Ratschan
first4 = T.
last4 = Schubert
first5 = T.
last5 = Teige
url = http://jsat.ewi.tudelft.nl/content/volume1/JSAT1_11_Fraenzle.pdf
contribution = Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure
title = JSAT Special Issue on SAT/CP Integration
volume =1
pages = 209&ndash;236
date = 2007

# D. Kroening and O. Strichman, Decision Procedures &mdash; an algorithmic point of view (2008), Springer (Theoretical Computer Science series) ISBN 978-3540741046.
# G.-J. Nam, K. A. Sakallah, and R. Rutenbar, doi-inline|10.1109/TCAD.2002.1004311|A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 6, pp. 674&ndash;684, 2002.
# C. Tinelli, "A DPLL-based Calculus for Ground Satisfiability Modulo Theories," in Europ. Conf. on Logic in AI (JELIA), pp., 2002.

----"This article is adapted from a column in the ACM [http://www.sigda.org SIGDA] [http://www.sigda.org/newsletter/index.html e-newsletter] by [http://www.eecs.umich.edu/~karem Prof. Karem Sakallah]
Original text is available [http://www.sigda.org/newsletter/2006/eNews_061215.html here] ."


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать реферат

Look at other dictionaries:

  • Satisfiability Modulo Theories — В программировании, Satisfiability Modulo Theories (SMT) это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для 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… …   Wikipédia en Français

  • 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

  • Maximum satisfiability problem — In computational complexity theory, the Maximum Satisfiability problem (MAX SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula, that can be satisfied by some assignment. It is an FNP generalization of SAT …   Wikipedia

  • Constraint satisfaction — In artificial intelligence and operations research, constraint satisfaction is the process of finding a solution to a set of constraints that impose conditions that the variables must satisfy. A solution is therefore a vector of variables that… …   Wikipedia

  • Решатель — (англ. solver)  программное обеспечение, предназначенное для решения рассматриваемой математической задачи. На вход решателю поступает описание задачи в некоторой заданной форме, а на выходе он выдает решение задачи. Виды решаемых задач …   Википедия

  • 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

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Constraint programming — Programming paradigms Agent oriented Automata based Component based Flow based Pipelined Concatenative Concurrent computin …   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

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”