In
computer scienceComputer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, the
Satisfiability Modulo Theories (
SMT)
problem is a
decision problemIn computability theory and computational complexity theory, a decision problem is a question in some formal system with a yesorno answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
for logical formulas with respect to combinations of background
theoriesIn mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
expressed in classical
firstorder logicFirstorder logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: firstorder predicate calculus, the lower predicate calculus, quantification theory, and predicate 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 structureIn computer science, a data structure is a particular way of storing and organizing data in a computer so that it can be used efficiently.Different kinds of data structures are suited to different kinds of applications, and some are highly specialized to specific tasks...
s such as
lists, arrays, bit vectors and so on. SMT can be thought of as a form of the
constraint satisfaction problemConstraint satisfaction problems 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 constraints over variables, which is solved by constraint...
and thus a certain formalized approach to
constraint programmingConstraint programming is a programming paradigm wherein relations between variables are stated in the form of constraints. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties...
.
Basic terminology
Formally speaking, an SMT instance is a
formulaIn mathematics, a formula is an entity constructed using the symbols and formation rules of a given logical language....
in
firstorder logicFirstorder logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: firstorder predicate calculus, the lower predicate calculus, quantification theory, and predicate 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 problemIn computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
(SAT) in which some of the binary variables are replaced by predicates over a suitable set of nonbinary variables. A predicate is basically a binaryvalued function of nonbinary variables. Example predicates include linear inequalities (e.g.,
) or equalities involving uninterpreted terms and function symbols (e.g.,
where
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
arithmeticArithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple daytoday counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
, whereas predicates involving uninterpreted terms and function symbols are evaluated using the rules of the theory of
uninterpreted functionIn mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and arity. Function symbols are used, together with constants and variables, to form terms....
s with equality (sometimes referred to as the empty theory). 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 subtheory of linear arithmetic in which each inequality is restricted to have the form
for variables
and
and constant
.
Most SMT solvers support only quantifier free fragments of their logics.
Expressive power of SMT
An SMT instance is a generalization of a
Boolean SATIn computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
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
languageLanguage may refer either to the specifically human capacity for acquiring and using complex systems of communication, or to a specific instance of such a system of complex communication...
than is possible with Boolean SAT formulas. For example, an SMT formula allows us to model the
datapathA datapath is a collection of functional units, such as arithmetic logic units or multipliers, that perform data processing operations. Most central processing units consist of a datapath and a control unit, with a large part of the control unit dedicated to regulating the interaction between the...
operations of a
microprocessorA microprocessor incorporates the functions of a computer's central processing unit on a single integrated circuit, or at most a few integrated circuits. It is a multipurpose, programmable device that accepts digital data as input, processes it according to instructions stored in its memory, and...
at the word rather than the bit level.
By comparison,
answer set programmingAnswer set programming is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers  programs for generating stable...
is also based on predicates (more precisely, on
atomic sentenceIn logic, an atomic sentence is a type of declarative sentence which is either true or false and which cannot be broken down into other simpler sentences...
s created from
atomic formulaIn mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest wellformed formulas of the logic...
). Unlike SMT, answerset programs do not have quantifiers, and cannot easily express constraints such as linear arithmetic or difference logic  ASP is at best suitable for boolean problems that reduce to the free theory of uninterpreted functions. Implementing 32bit integers as bitvectors in ASP suffers from most of the same problems that early SMT solvers faced: "obvious" identities such as
x+
y=
y+
x are difficult to deduce.
Constraint logic programming does provide support for linear arithmetic constraints, but within a completely different theoretical framework.
SMT solvers
Early attempts for solving SMT instances involved translating them to Boolean SAT instances (e.g., a 32bit integer variable would be encoded by 32 bit variables with appropriate weights and wordlevel operations such as 'plus' would be replaced by lowerlevel logic operations on the bits) and passing this formula to a Boolean SAT solver. This approach, which is referred to as
the eager approach, has its merits: by preprocessing the SMT formula into an equivalent Boolean SAT formula we can use existing Boolean SAT solvers "asis" and leverage their performance and capacity improvements over time. On the other hand, the loss of the highlevel 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
for integer addition.) This observation led to the development of a number of SMT solvers that tightly integrate the Boolean reasoning of a
DPLLThe Davis–Putnam–Logemann–Loveland algorithm is a complete, backtrackingbased algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNFSAT problem....
style search with theoryspecific solvers (
Tsolvers) that handle
conjunctionsIn logic and mathematics, a twoplace logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
(ANDs) of predicates from a given theory. This approach is referred to as
the lazy approach.
Dubbed DPLL(T) , this architecture gives the responsibility of Boolean reasoning to the DPLLbased SAT solver which, in turn, interacts with a solver for theory T through a welldefined 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
backtrackableBacktracking is a general algorithm for finding all solutions to some computational problem, that incrementally builds candidates to the solutions, and abandons each partial candidate c as soon as it determines that c cannot possibly be completed to a valid solution.The classic textbook example...
.
SMT for undecidable theories
Most of the common SMT approaches support
decidableIn logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
theories. However, many realworld systems can only be modelled by means of nonlinear arithmetic over the real numbers involving
transcendental functionA transcendental function is a function that does not satisfy a polynomial equation whose coefficients are themselves polynomials, in contrast to an algebraic function, which does satisfy such an equation...
s, e.g. an aircraft and its behavior. This fact motivates an extension of the SMT problem to nonlinear theories, e.g. determine whether

where

is satisfiable. Then, such problems become undecidableIn computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yesorno answer....
in general. (It is important to note, however, that the theory of real closed fieldIn mathematics, a real closed field is a field F that has the same firstorder properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.Definitions:...
s, and thus the full first order theory of the real numberIn mathematics, a real number is a value that represents a quantity along a continuum, such as 5 , 4/3 , 8.6 , √2 and π...
s, are decidableIn logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
using quantifier eliminationQuantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification...
. This is due to Alfred TarskiAlfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the LwowWarsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
.) The first order theory of the natural numbers with addition (but not multiplication), called Presburger arithmeticPresburger arithmetic is the firstorder theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
, is also decidable. Since multiplication by constants can be implemented as nested additions, the arithmetic in many computer programs can be expressed using Presburger arithmetic, resulting in decidable formulas.
Examples of SMT solvers addressing Boolean combinations of theory atoms from undecidable arithmetic theories over the reals are ABsolver, which employs a classical DPLL(T) architecture with a nonlinear optimization packet as (necessarily incomplete) subordinate theory solver, and HySAT2, building on a unification of DPLL SATsolving and interval constraint propagation called the iSAT algorithm .
SMT solvers
The table below summarizes some of the features of the many available SMT solvers. The column "SMTLIB" indicates compatibility with the SMTLIB language; many systems marked 'yes' may support only older versions of SMTLIB, or offer only partial support for the language. The column "CVC" indicates support for the CVC language. The column "DIMACS" indicates support for the DIMACS format.
Projects differ not only in features and performance, but also in the viability of the surrounding community, its ongoing interest in a project, and its ability to contribute documentation, fixes, tests and enhancements. Based on these measures, it appears that the most vibrant, wellorganized projects are OpenSMT, STP and CVC4.
Platform 
Features 
Notes 
Name 
OS 
License 
SMTLIB 
CVC 
DIMACS 
Builtin theories 
API 
SMTCOMP http://www.smtcomp.org/ 

ABsolver 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

CPL In computing, the CPL is a free software / opensource software license published by IBM. The Free Software Foundation and Open Source Initiative have approved the license terms of the CPL....




linear arithmetic, nonlinear arithmetic 
C++C++ is a statically typed, freeform, multiparadigm, compiled, generalpurpose programming language. It is regarded as an intermediatelevel language, as it comprises a combination of both highlevel and lowlevel language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...

no 
DPLLbased 
AltErgo 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OSMac OS is a series of graphical user interfacebased operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

Free softwareFree software, software libre or libre software is software that can be used, studied, and modified without restriction, and which can be copied and redistributed in modified or unmodified form either without restriction, or with restrictions that only ensure that further recipients can also do...




empty theory, linear arithmetic 
OCaml 
2008 
based on congruence closure 
Barcelogic 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

Proprietary 



empty theory, difference logic 
C++C++ is a statically typed, freeform, multiparadigm, compiled, generalpurpose programming language. It is regarded as an intermediatelevel language, as it comprises a combination of both highlevel and lowlevel language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...

2009 
DPLLbased, congruence closure 
Beaver 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

BSD BSD licenses are a family of permissive free software licenses. The original license was used for the Berkeley Software Distribution , a Unixlike operating system after which it is named....




bitvectors 
OCaml 
2009 
SATsolver based 
Boolector 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

GPLv3 



bitvectors, arrays 
C 
2009 
SATsolver based 
CVC3 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

BSD BSD licenses are a family of permissive free software licenses. The original license was used for the Berkeley Software Distribution , a Unixlike operating system after which it is named....




empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers 
C/C++ 
2010 
proof output to HOL In mathematics and logic, a higherorder logic is a form of predicate logic that is distinguished from firstorder logic by additional quantifiers and a stronger semantics...

CVC4 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

BSD BSD licenses are a family of permissive free software licenses. The original license was used for the Berkeley Software Distribution , a Unixlike operating system after which it is named....




prealpha 

2010 
active development; prealpha 
Decision Procedure Toolkit (DPT) 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

ApacheThe Apache License is a copyfree free software license authored by the Apache Software Foundation . The Apache License requires preservation of the copyright notice and disclaimer....





OCaml 
no 
DPLLbased 
iSAT 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

Proprietary 



nonlinear arithmetic 

no 
DPLLbased 
MathSAT 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

Proprietary 



empty theory, difference logics, linear arithmetic 

2010 
DPLLbased 
MiniSmt 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

LGPL 



nonlinear arithmetic 

2010 
Yicesbased 
OpenSMT 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

GPLv3 



empty theory, differences, linear arithmetic, bitvectors 
C++ 
2010 
lazy SMT Solver 
SatEEn 
? 
Proprietary 



linear arithmetic, difference logic 
none 
2009 

SONOLAR 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

Proprietary 



bitvectors 
C 
2010 
SATsolver based 
Spear 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OSMac OS is a series of graphical user interfacebased operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

Proprietary 



bitvectors 

2008 

STP 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , OpenBSDOpenBSD is a Unixlike computer operating system descended from Berkeley Software Distribution , a Unix derivative developed at the University of California, Berkeley. It was forked from NetBSD by project leader Theo de Raadt in late 1995... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... , Mac OSMac OS is a series of graphical user interfacebased operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface...

MIT The MIT License is a free software license originating at the Massachusetts Institute of Technology . It is a permissive license, meaning that it permits reuse within proprietary software provided all copies of the licensed software include a copy of the MIT License terms...




bitvectors, arrays 
C, C++C++ is a statically typed, freeform, multiparadigm, compiled, generalpurpose programming language. It is regarded as an intermediatelevel language, as it comprises a combination of both highlevel and lowlevel language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell... , PythonPython is a generalpurpose, highlevel programming language whose design philosophy emphasizes code readability. Python claims to "[combine] remarkable power with very clear syntax", and its standard library is large and comprehensive... , OCaml, JavaJava is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer lowlevel facilities...

2010 
SATsolver based 
SWORD 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

Proprietary 



bitvectors 

2009 

UCLID 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

BSD BSD licenses are a family of permissive free software licenses. The original license was used for the Berkeley Software Distribution , a Unixlike operating system after which it is named....




empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.) 

no 
SATsolver based, written in Moscow ML Moscow ML is an implementation of Standard ML.The codebase is derived from Caml Light.The latest release is 2.01. Supported platforms include Unix, Windows, Mac OS and .NET. External links :*... . Input language is SMV model checker. Welldocumented! 
veriT 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...

BSD BSD licenses are a family of permissive free software licenses. The original license was used for the Berkeley Software Distribution , a Unixlike operating system after which it is named....




empty theory, difference logic 
C/C++ 
2010 
SATsolver based 
Yices 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OSMac OS is a series of graphical user interfacebased operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

Proprietary 





2009 

Z3 
LinuxLinux is a Unixlike computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , WindowsMicrosoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an addon to MSDOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal...

Proprietary 



empty theory, linear arithmetic, bitvectors, arrays, quantifiers 
C, .Net, OCaml 
2008 
