Satisfiability modulo theories

Logical problem studied in computer science

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first order logic with equality (often disallowing quantifiers). SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing. Since Boolean satisfiability is already NP complete, the SMT problem is typically NP hard, and for many theories it is undecidable. Researchers study which theories or subsets of theories lead to a decidable SMT problem and the computational complexity of decidable cases. The resulting decision procedures are often implemented directly in SMT solvers; see, for instance, the decidability of Presburger arithmetic. SMT can be thought of as a constraint satisfaction problem and thus a certain formalized approach to constraint programming.

There is substantial overlap between SMT solving and automated theorem proving. Generally, automated theorem provers focus on supporting full first order logic with quantifiers, whereas SMT solvers focus more on supporting various theories (interpreted predicate symbols). ATPs excel at problems with lots of quantifiers, whereas SMT solvers do well on large problems without quantifiers. The line is blurry enough that some ATPs participate in SMT COMP, while some SMT solvers participate in CASC.

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. SMT formulas provide a much richer modeling language than is possible with Boolean SAT formulas. For example, an SMT formula allows one to model the datapath operations of a microprocessor at the word rather than the bit level. By comparison, answer set programming is also based on predicates (more precisely, on atomic sentences created from atomic formulas). Unlike SMT, answer set programs do not have quantifiers, and cannot easily express constraints such as linear arithmetic or difference logic—answer set programming is best suited to Boolean problems that reduce to the free theory of uninterpreted functions. Implementing 32 bit integers as bitvectors in answer set programming 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 have also been extended to solve formulas in higher order logic.

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 single 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, which is referred to as the eager approach (or bitblasting), has its merits: by pre processing the SMT formula into an equivalent Boolean SAT formula existing Boolean SAT solvers can be used "as is" and their performance and capacity improvements leveraged 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 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 (T solvers) that handle conjunctions (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 DPLL based SAT solver which, in turn, interacts with a solver for theory T through a well defined interface. The theory solver only needs to 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.

Researchers study which theories or subsets of theories lead to a decidable SMT problem and the computational complexity of decidable cases. Since full first order logic is only semidecidable, one line of research attempts to find efficient decision procedures for fragments of first order logic such as effectively propositional logic. Another line of research involves the development of specialized decidable theories, including linear arithmetic over rationals and integers, fixed width bitvectors, floating point arithmetic (often implemented in SMT solvers via bit blasting, i. e., reduction to bitvectors), strings, (co) datatypes, sequences (used to model dynamic arrays), finite sets and relations, separation logic, finite fields, and uninterpreted functions among others. Boolean monotonic theories are a class of theory that support efficient theory propagation and conflict analysis, enabling practical use within DPLL(T) solvers. Monotonic theories support only boolean variables (boolean is the only sort), and all their functions and predicates p obey the axiom

Examples of monotonic theories include graph reachability, collision detection for convex hulls, minimum cuts, and computation tree logic. Every Datalog program can be interpreted as a monotonic theory.

The table below summarizes some of the features of the many available SMT solvers. The column "SMT LIB" indicates compatibility with the SMT LIB language; many systems marked 'yes' may support only older versions of SMT LIB, or offer only partial support for the language. The column "CVC" indicates support for the CVC (Cooperating Validity Checker) 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. Platform Features Notes Name OS License SMT LIB CVC DIMACS Built in theories API SMT COMP ABsolver Linux CPL linear arithmetic, non linear arithmetic C++ no DPLL based Alt Ergo Linux, Mac OS, Windows CeCILL C (roughly equivalent to LGPL) empty theory, linear integer and rational arithmetic, non linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers OCaml 2008 Polymorphic first order input language à la ML, SAT solver based, combines Shostak like and Nelson Oppen like approaches for reasoning modulo theories Barcelogic Linux Proprietary empty theory, difference logic C++ 2009 DPLL based, congruence closure Beaver Linux, Windows BSD bitvectors OCaml 2009 SAT solver based Boolector Linux MIT bitvectors, arrays C 2009 SAT solver based CVC3 Linux BSD empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers C/C++ 2010 proof output to HOL CVC4 Linux, Mac OS, Windows, FreeBSD BSD rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, and equality over uninterpreted function symbols C++ 2021 version 1.8 released May 2021 cvc5 Linux, Mac OS, Windows BSD rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, sequences, bags, and equality over uninterpreted function symbols C++, Python, Java 2021 version 1.0 released April 2022 Decision Procedure Toolkit (DPT) Linux Apache OCaml no DPLL based iSAT Linux Proprietary non linear arithmetic no DPLL based MathSAT Linux, Mac OS, Windows Proprietary empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays C/C++, Python, Java 2010 DPLL based MiniSmt Linux LGPL non linear arithmeticOCaml 2010 SAT solver based, Yices based Norn SMT solver for string constraints OpenCog Linux AGPL probabilistic logic, arithmetic. relational models C++, Scheme, Python no subgraph isomorphism OpenSMT Linux, Mac OS, Windows GPLv3 empty theory, differences, linear arithmetic, bitvectors C++ 2011 lazy SMT SolverraSATLinuxGPLv3v2.0real and integer nonlinear arithmetic2014, 2015extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem SatEEn ? Proprietary linear arithmetic, difference logic none 2009 SMTInterpol Linux, Mac OS, Windows LGPLv3 uninterpreted functions, linear real arithmetic, and linear integer arithmetic Java 2012 Focuses on generating high quality, compact interpolants. SMCHR Linux, Mac OS, Windows GPLv3 linear arithmetic, nonlinear arithmetic, heaps C no Can implement new theories using Constraint Handling Rules. SMT RAT Linux, Mac OS MIT linear arithmetic, nonlinear arithmetic C++ 2015 Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations. SONOLAR Linux, Windows Proprietary bitvectors C 2010 SAT solver based Spear Linux, Mac OS, Windows Proprietary bitvectors 2008 STP Linux, OpenBSD, Windows, Mac OS MIT bitvectors, arrays C, C++, Python, OCaml, Java 2011 SAT solver based SWORD Linux Proprietary bitvectors 2009 UCLID Linux BSD empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.) no SAT solver based, written in Moscow ML. Input language is SMV model checker. Well documented! veriT Linux, OS X BSD empty theory, rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols C/C++ 2010 SAT solver based, can produce proofs Linux, Mac OS, Windows, FreeBSD GPLv3 rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols C 2014 Source code is available online Z3 Theorem Prover Linux, Mac OS, Windows, FreeBSD MIT empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers, strings C/C++, NET, OCaml, Python, Java, Haskell 2011 Source code is available online

There are multiple attempts to describe a standardized interface to SMT solvers (and automated theorem provers, a term often used synonymously). The most prominent is the SMT LIB standard, which provides a language based on S expressions. Other standardized formats commonly supported are the DIMACS format supported by many Boolean SAT solvers, and the CVC format used by the CVC automated theorem prover. The SMT LIB format also comes with a number of standardized benchmarks and has enabled a yearly competition between SMT solvers called SMT COMP. Initially, the competition took place during the Computer Aided Verification conference (CAV), but as of 2020 the competition is hosted as part of the SMT Workshop, which is affiliated with the International Joint Conference on Automated Reasoning (IJCAR).

SMT solvers are useful both for verification, proving the correctness of programs, software testing based on symbolic execution, and for synthesis, generating program fragments by searching over the space of possible programs. Outside of software verification, SMT solvers have also been used for type inference and for modelling theoretic scenarios, including modelling actor beliefs in nuclear arms control.

An important application of SMT solvers is symbolic execution for analysis and testing of programs (e. g., concolic testing), aimed particularly at finding security vulnerabilities. Example tools in this category include SAGE from Microsoft Research, KLEE, S2E, and Triton. SMT solvers that have been used for symbolic execution applications include Z3, STP , the Z3str family of solvers, and Boolector.

SMT solvers have been integrated with proof assistants, including Coq and Isabelle/HOL.