{{Short description|Logical problem studied in computer science}}
In [[computer science]] and [[mathematical logic]], '''satisfiability modulo theories''' ('''SMT''') is the [[decision problem|problem]] of determining whether a [[Well-formed formula|mathematical formula]] is [[Satisfiability|satisfiable]]. It generalizes the [[Boolean satisfiability problem]] (SAT) to more complex formulas involving [[real numbers]], [[integers]], and/or various [[data structure]]s such as [[List (computing)|list]]s, [[Array data structure|arrays]], [[bit vector]]s, and [[String (computer science)|strings]]. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain [[Theory (mathematical logic)|formal theory]] in [[first-order logic|first-order logic with equality]] (often disallowing [[Quantifier (logic)|quantifiers]]). '''SMT solvers''' are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as [[Z3 Theorem Prover|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]], [[Formal verification|program verification]], and [[white-box testing|software testing]].
Since Boolean satisfiability is already [[NP-complete]], the SMT problem is typically [[NP-hardness|NP-hard]], and for many theories it is [[Undecidable problem|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]].
==Terminology and examples== Formally speaking, an SMT instance is a [[Well-formed formula|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 data|binary variables]] are replaced by [[predicate (mathematical logic)|predicate]]s over a suitable set of non-binary variables. A predicate is a binary-valued function of non-binary variables. Example predicates include linear [[inequality (mathematics)|inequalities]] (e.g., <math>3x + 2y - z \geq 4</math>) or equalities involving [[uninterpreted term]]s and function symbols (e.g., <math>f(f(u, v), v) = f(u, v)</math> where <math>f</math> is some unspecified function of two arguments). These predicates are classified according to each respective theory assigned. For instance, linear inequalities over [[real number|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 function]]s with equality (sometimes referred to as the [[empty theory]]). Other theories include the theories of [[array data structure|arrays]] and [[List (computing)|list]] structures (useful for modeling and verifying [[computer program]]s), and the theory of [[bit vectors]] (useful in modeling and verifying [[hardware design]]s). 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 <math>x - y > c</math> for variables <math>x</math> and <math>y</math> and constant <math>c</math>.
The examples above show the use of linear integer arithmetic over inequalities. Other examples include: <ul> <li>Satisfiability: Determine if <math>x\vee (y\wedge \neg z)</math> is satisfiable. </li> <li>Array access: Find a value for array ''A'' such that ''A''[0] = 5.</li> <li> Bit vector arithmetic: Determine if ''x'' and ''y'' are distinct 3-bit numbers. </li> <li> Uninterpreted functions: Find values for ''x'' and ''y'' such that <math> f(x) = 2</math> and <math> g(x) = 3</math>. </ul>
Most SMT solvers support only [[Quantifier (logic)|quantifier]]-free fragments of their logics.{{citation needed|date=April 2024}}
==Relationship to automated theorem proving==
There is substantial overlap between SMT solving and [[automated theorem proving]] (ATP). 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.<ref>{{Cite journal |last1=Blanchette |first1=Jasmin Christian |last2=Böhme |first2=Sascha |last3=Paulson |first3=Lawrence C. |date=2013-06-01 |title=Extending Sledgehammer with SMT Solvers |url=https://doi.org/10.1007/s10817-013-9278-5 |journal=Journal of Automated Reasoning |language=en |volume=51 |issue=1 |pages=109–128 |doi=10.1007/s10817-013-9278-5 |issn=1573-0670|quote=ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.|url-access=subscription }}</ref> The line is blurry enough that some ATPs participate in SMT-COMP, while some SMT solvers participate in [[CADE ATP System Competition|CASC]].<ref>{{Cite journal |last1=Weber |first1=Tjark |last2=Conchon |first2=Sylvain |last3=Déharbe |first3=David |last4=Heizmann |first4=Matthias |last5=Niemetz |first5=Aina |last6=Reger |first6=Giles |date=2019-01-01 |title=The SMT Competition 2015–2018 |journal=Journal on Satisfiability, Boolean Modeling and Computation |language=en |volume=11 |issue=1 |pages=221–259 |doi=10.3233/SAT190123|s2cid=210147712 |quote=In recent years, we have seen a blurring of lines between SMT-COMP and CASC with SMT solvers competing in CASC and ATPs competing in SMT-COMP.|doi-access=free }}</ref>
==Expressive power== An SMT instance is a generalization of a [[Boolean satisfiability problem|Boolean SAT]] instance in which various sets of variables are replaced by [[predicate (mathematical logic)|predicate]]s 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 sentence]]s created from [[atomic formula]]s). 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.{{citation needed|date=July 2020}} SMT solvers have also been extended to solve formulas in [[higher-order logic]].<ref>{{cite book |first1=Haniel |last1=Barbosa |first2=Andrew |last2=Reynolds |first3=Daniel |last3=El Ouraoui |first4=Cesare |last4=Tinelli |first5=Clark |last5=Barrett |chapter=Extending SMT solvers to higher-order logic |chapter-url=https://hal.archives-ouvertes.fr/hal-02300986/document |title=Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings |publisher=Springer |date=2019 |isbn=978-3-030-29436-6 |pages=35–54 |doi=10.1007/978-3-030-29436-6_3 |s2cid=85443815 |id=hal-02300986}}</ref>
==Solver approaches== 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 evaluation|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 <math>x + y = y + x</math> for integer addition.) This observation led to the development of a number of SMT solvers that tightly integrate the Boolean reasoning of a [[DPLL algorithm|DPLL]]-style search with theory-specific solvers (''T-solvers'') that handle [[Logical conjunction|conjunctions]] (ANDs) of predicates from a given theory. This approach is referred to as ''the [[Lazy evaluation|lazy]] approach''.<ref>{{Cite book |last1=Bruttomesso |first1=Roberto |last2=Cimatti |first2=Alessandro |last3=Franzén |first3=Anders |last4=Griggio |first4=Alberto |last5=Hanna |first5=Ziyad |last6=Nadel |first6=Alexander |last7=Palti |first7=Amit |last8=Sebastiani |first8=Roberto |chapter=A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems |date=2007 |editor-last=Damm |editor-first=Werner |editor2-last=Hermanns |editor2-first=Holger |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-540-73368-3_54 |series=Lecture Notes in Computer Science |volume=4590 |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=547–560 |doi=10.1007/978-3-540-73368-3_54 |isbn=978-3-540-73368-3}}</ref>
Dubbed [[DPLL(T)]],<ref>{{Citation | first1 = R. | last1 = Nieuwenhuis | first2 = A. | last2 = Oliveras | first3 = C. | last3 = Tinelli | contribution-url = http://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf | contribution = Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) | title = [[Journal of the ACM]] | volume = 53 | pages = 937–977 | year = 2006 |doi=10.1145/1217856.1217859 | issue=6| s2cid = 14058631 }}</ref> 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 [[Backtracking|backtrackable]].
==Decidable theories==
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]].<ref>{{Cite conference |conference=4th International Joint Conference on Automated Reasoning, Sydney, NSW, Australia|date= August 12–15, 2008|last1=de Moura |first1=Leonardo |last2=Bjørner |first2=Nikolaj |editor-last=Armando |editor-first=Alessandro |editor2-last=Baumgartner |editor2-first=Peter |editor3-last=Dowek |editor3-first=Gilles |chapter=Deciding Effectively Propositional Logic Using DPLL and Substitution Sets |chapter-url=https://link.springer.com/chapter/10.1007/978-3-540-71070-7_35 |title=Automated Reasoning |series=Lecture Notes in Computer Science |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=410–425 |doi=10.1007/978-3-540-71070-7_35 |isbn=978-3-540-71070-7}}</ref>
Another line of research involves the development of specialized [[Decidability (logic)|decidable theories]], including linear arithmetic over [[Rational number|rationals]] and [[integer]]s, fixed-width bitvectors,<ref>{{Cite book |last1=Hadarean |first1=Liana |last2=Bansal |first2=Kshitij |last3=Jovanović |first3=Dejan |last4=Barrett |first4=Clark |last5=Tinelli |first5=Cesare |chapter=A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors |date=2014 |editor-last=Biere |editor-first=Armin |editor2-last=Bloem |editor2-first=Roderick |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-08867-9_45 |series=Lecture Notes in Computer Science |volume=8559 |language=en |location=Cham |publisher=Springer International Publishing |pages=680–695 |doi=10.1007/978-3-319-08867-9_45 |isbn=978-3-319-08867-9}}</ref> [[floating-point arithmetic]] (often implemented in SMT solvers via ''bit-blasting'', i.e., reduction to bitvectors),<ref>{{Cite conference |last1=Brain |first1=Martin |last2=Schanda |first2=Florian |last3=Sun |first3=Youcheng |date=2019 |editor-last=Vojnar |editor-first=Tomáš |editor2-last=Zhang |editor2-first=Lijun |chapter=Building Better Bit-Blasting for Floating-Point Problems |title=Tools and Algorithms for the Construction and Analysis of Systems |conference= 25th International Conference, Tools and Algorithms for the Construction and Analysis of Systems 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=79–98 |doi=10.1007/978-3-030-17462-0_5 |isbn=978-3-030-17462-0|s2cid=92999474 |doi-access=free }}</ref><ref>{{Cite conference |last1=Brain |first1=Martin |last2=Niemetz |first2=Aina |last3=Preiner |first3=Mathias |last4=Reynolds |first4=Andrew |last5=Barrett |first5=Clark |last6=Tinelli |first6=Cesare |date=2019 |editor-last=Dillig |editor-first=Isil |editor2-last=Tasiran |editor2-first=Serdar |chapter=Invertibility Conditions for Floating-Point Formulas |title=Computer Aided Verification |conference= 31st International Conference, Computer Aided Verification 2019, New York City, July 15–18, 2019 |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=116–136 |doi=10.1007/978-3-030-25543-5_8 |isbn=978-3-030-25543-5|s2cid=196613701 |doi-access=free }}</ref> [[String (computer science)|string]]s,<ref>{{Cite book |last1=Liang |first1=Tianyi |last2=Tsiskaridze |first2=Nestan |last3=Reynolds |first3=Andrew |last4=Tinelli |first4=Cesare |last5=Barrett |first5=Clark |chapter=A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings |date=2015 |editor-last=Lutz |editor-first=Carsten |editor2-last=Ranise |editor2-first=Silvio |title=Frontiers of Combining Systems |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-24246-0_9 |series=Lecture Notes in Computer Science |volume=9322 |language=en |location=Cham |publisher=Springer International Publishing |pages=135–150 |doi=10.1007/978-3-319-24246-0_9 |isbn=978-3-319-24246-0}}</ref> [[Data type|(co)-datatypes]],<ref>{{Cite book |last1=Reynolds |first1=Andrew |last2=Blanchette |first2=Jasmin Christian |chapter=A Decision Procedure for (Co)datatypes in SMT Solvers |date=2015 |editor-last=Felty |editor-first=Amy P. |editor2-last=Middeldorp |editor2-first=Aart |title=Automated Deduction - CADE-25 |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-21401-6_13 |series=Lecture Notes in Computer Science |volume=9195 |language=en |location=Cham |publisher=Springer International Publishing |pages=197–213 |doi=10.1007/978-3-319-21401-6_13 |isbn=978-3-319-21401-6}}</ref> [[sequence]]s (used to model [[dynamic array]]s),<ref>{{Cite journal |last1=Sheng |first1=Ying |last2=Nötzli |first2=Andres |last3=Reynolds |first3=Andrew |last4=Zohar |first4=Yoni |last5=Dill |first5=David |last6=Grieskamp |first6=Wolfgang |last7=Park |first7=Junkil |last8=Qadeer |first8=Shaz |last9=Barrett |first9=Clark |last10=Tinelli |first10=Cesare |date=2023-09-15 |title=Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences |url=https://doi.org/10.1007/s10817-023-09682-2 |journal=Journal of Automated Reasoning |language=en |volume=67 |issue=3 |pages=32 |doi=10.1007/s10817-023-09682-2 |s2cid=261829653 |issn=1573-0670|url-access=subscription }}</ref> finite [[Set (mathematics)|sets]] and [[Relation (mathematics)|relations]],<ref>{{Cite book |last1=Bansal |first1=Kshitij |last2=Reynolds |first2=Andrew |last3=Barrett |first3=Clark |last4=Tinelli |first4=Cesare |chapter=A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT |date=2016 |editor-last=Olivetti |editor-first=Nicola |editor2-last=Tiwari |editor2-first=Ashish |title=Automated Reasoning |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-40229-1_7 |series=Lecture Notes in Computer Science |volume=9706 |language=en |location=Cham |publisher=Springer International Publishing |pages=82–98 |doi=10.1007/978-3-319-40229-1_7 |isbn=978-3-319-40229-1}}</ref><ref>{{Cite book |last1=Meng |first1=Baoluo |last2=Reynolds |first2=Andrew |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |chapter=Relational Constraint Solving in SMT |date=2017 |editor-last=de Moura |editor-first=Leonardo |title=Automated Deduction – CADE 26 |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10 |series=Lecture Notes in Computer Science |volume=10395 |language=en |location=Cham |publisher=Springer International Publishing |pages=148–165 |doi=10.1007/978-3-319-63046-5_10 |isbn=978-3-319-63046-5}}</ref> [[separation logic]],<ref>{{Cite book |last1=Reynolds |first1=Andrew |last2=Iosif |first2=Radu |last3=Serban |first3=Cristina |last4=King |first4=Tim |chapter=A Decision Procedure for Separation Logic in SMT |date=2016 |editor-last=Artho |editor-first=Cyrille |editor2-last=Legay |editor2-first=Axel |editor3-last=Peled |editor3-first=Doron |title=Automated Technology for Verification and Analysis |chapter-url=https://hal.science/hal-01418883 |series=Lecture Notes in Computer Science |volume=9938 |language=en |location=Cham |publisher=Springer International Publishing |pages=244–261 |doi=10.1007/978-3-319-46520-3_16 |isbn=978-3-319-46520-3|s2cid=6753369 }}</ref> [[finite field]]s,<ref>{{Cite book |last1=Ozdemir |first1=Alex |last2=Kremer |first2=Gereon |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |chapter=Satisfiability Modulo Finite Fields |date=2023 |editor-last=Enea |editor-first=Constantin |editor2-last=Lal |editor2-first=Akash |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8 |series=Lecture Notes in Computer Science |volume=13965 |language=en |location=Cham |publisher=Springer Nature Switzerland |pages=163–186 |doi=10.1007/978-3-031-37703-7_8 |isbn=978-3-031-37703-7|s2cid=257235627 }}</ref> and [[uninterpreted function]]s 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.<ref>{{Cite journal |last1=Bayless |first1=Sam |last2=Bayless |first2=Noah |last3=Hoos |first3=Holger |last4=Hu |first4=Alan |date=2015-03-04 |title=SAT Modulo Monotonic Theories |url=https://ojs.aaai.org/index.php/AAAI/article/view/9755 |journal=Proceedings of the AAAI Conference on Artificial Intelligence |language=en |volume=29 |issue=1 |doi=10.1609/aaai.v29i1.9755 |s2cid=9567647 |issn=2374-3468|doi-access=free |arxiv=1406.0043 }}</ref> Monotonic theories support only Boolean variables (Boolean is the only ''sort''), and all their functions and predicates {{mvar|p}} obey the axiom
: <math>p(\ldots,b_{i-1},0,b_{i+1},\ldots)\implies p(\ldots,b_{i-1},1,b_{i+1},\ldots)</math>
Examples of monotonic theories include [[Reachability|graph reachability]], collision detection for [[convex hull]]s, [[minimum cut]]s, and [[computation tree logic]].<ref>{{Cite book |last1=Klenze |first1=Tobias |last2=Bayless |first2=Sam |last3=Hu |first3=Alan J. |chapter=Fast, Flexible, and Minimal CTL Synthesis via SMT |date=2016 |editor-last=Chaudhuri |editor-first=Swarat |editor2-last=Farzan |editor2-first=Azadeh |title=Computer Aided Verification |chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-41528-4_8 |series=Lecture Notes in Computer Science |volume=9779 |language=en |location=Cham |publisher=Springer International Publishing |pages=136–156 |doi=10.1007/978-3-319-41528-4_8 |isbn=978-3-319-41528-4}}</ref> Every [[Datalog]] program can be interpreted as a monotonic theory.<ref>{{Cite journal |last1=Bembenek |first1=Aaron |last2=Greenberg |first2=Michael |last3=Chong |first3=Stephen |date=2023-01-11 |title=From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems |journal=Proceedings of the ACM on Programming Languages |volume=7 |issue=POPL |pages=7:185–7:217 |doi=10.1145/3571200|s2cid=253525805 |doi-access=free }}</ref>
==SMT for undecidable theories== Most of the common SMT approaches support [[Decidability (logic)|decidable]] theories. However, many real-world systems, such as an aircraft and its behavior, can only be modelled by means of non-linear arithmetic over the real numbers involving [[transcendental function]]s. This fact motivates an extension of the SMT problem to non-linear theories, such as determining whether the following equation is satisfiable:
: <math> \begin{array}{lr} & (\sin(x)^3 = \cos(\log(y)\cdot x) \vee b \vee -x^2 \geq 2.3y) \wedge \left(\neg b \vee y < -34.4 \vee \exp(x) > {y \over x}\right) \end{array} </math>
where
: <math>b \in {\mathbb B}, x,y \in {\mathbb R}.</math>
Such problems are, however, [[undecidable problem|undecidable]] in general. (On the other hand, the theory of [[real closed field]]s, and thus the full first order theory of the [[real number]]s, are [[Decidability (logic)|decidable]] using [[quantifier elimination]]. This is due to [[Alfred Tarski]].) The first order theory of the [[natural numbers]] with addition (but not multiplication), called [[Presburger arithmetic]], 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,<ref>{{Citation | first1 = A. | last1 = Bauer | author-link = | 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 | year = 2007 | doi = 10.1109/DATE.2007.364411 | page = 1 | isbn = 978-3-9810801-2-4 | citeseerx = 10.1.1.323.6807 | s2cid = 9159847 }}</ref> which employs a classical DPLL(T) architecture with a non-linear optimization packet as (necessarily incomplete) subordinate theory solver, [http://isat.gforge.avacs.org/ iSAT], building on a unification of DPLL SAT-solving and [[Interval arithmetic#Interval arithmetic|interval constraint propagation]] called the iSAT algorithm,<ref>{{Citation | first1 = M. | last1 = 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 | title = Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure | issue = 3–4 JSAT Special Issue on SAT/CP Integration | volume =1 |doi=10.3233/SAT190012 | pages = 209–236 |journal=Journal on Satisfiability, Boolean Modeling and Computation | year = 2007 }}</ref> and [[cvc5]].<ref>{{Cite book |last1=Barbosa |first1=Haniel |last2=Barrett |first2=Clark |last3=Brain |first3=Martin |last4=Kremer |first4=Gereon |last5=Lachnitt |first5=Hanna |last6=Mann |first6=Makai |last7=Mohamed |first7=Abdalrhman |last8=Mohamed |first8=Mudathir |last9=Niemetz |first9=Aina |last10=Nötzli |first10=Andres |last11=Ozdemir |first11=Alex |last12=Preiner |first12=Mathias |last13=Reynolds |first13=Andrew |last14=Sheng |first14=Ying |last15=Tinelli |first15=Cesare |date=2022 |editor-last=Fisman |editor-first=Dana |editor2-last=Rosu |editor2-first=Grigore |chapter=cvc5: A Versatile and Industrial-Strength SMT Solver |chapter-url=https://link.springer.com/chapter/10.1007/978-3-030-99524-9_24 |title=Tools and Algorithms for the Construction and Analysis of Systems, 28th International Conference|series=Lecture Notes in Computer Science |volume= 13243|language=en |location=Cham |publisher=Springer International Publishing |pages=415–442 |doi=10.1007/978-3-030-99524-9_24 |isbn=978-3-030-99524-9|s2cid=247857361 }}</ref>
==Solvers{{anchor|SMT solvers}}== 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 {{abbr|CVC|Cooperating Validity Checker}} language. The column "DIMACS" indicates support for the [[DIMACS]] [http://www.satcompetition.org/2009/format-benchmarks2009.html 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.
{| class="wikitable" |- ! colspan="3" | Platform ! colspan="6" | Features ! colspan="1" | Notes |- ! style="background:#ffdead;" | Name ! style="background:#ffdead;" | OS ! style="background:#ffdead;" | License ! style="background:#ffdead;" | SMT-LIB ! style="background:#ffdead;" | CVC ! style="background:#ffdead;" | DIMACS ! style="background:#ffdead;" | Built-in theories ! style="background:#ffdead;" | API ! style="background:#ffdead;" | SMT-COMP [http://www.smtcomp.org/] ! |- | ABsolver | [[Linux]] | [[Common Public License|CPL]] | {{yes|v1.2}} | {{no}} | {{yes}} | linear arithmetic, non-linear arithmetic | [[C++]] | no | DPLL-based |- | [[Alt-Ergo]] | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]] | [[CeCILL-C]] (roughly equivalent to [[LGPL]]) | {{yes|partial v1.2 and v2.0}} | {{no}} | {{no}} | [[empty theory]], linear integer and rational arithmetic, non-linear arithmetic, [[polymorphic array]]s, [[enumerated datatype]]s, [[AC symbol]]s, [[bitvector]]s, [[record datatype]]s, [[Quantifier (logic)|quantifier]]s | [[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 | {{yes|v1.2}} | | | [[empty theory]], [[difference logic]] | [[C++]] | 2009 | DPLL-based, [[congruence closure]] |- | Beaver | [[Linux]], [[Microsoft Windows|Windows]] | [[BSD licenses|BSD]] | {{yes|v1.2}} | {{no}} | {{no}} | bitvectors | [[OCaml]] | 2009 | SAT-solver based |- | Boolector | [[Linux]] | [[MIT License|MIT]] | {{yes|v1.2}} | {{no}} | {{no}} | [[bitvector]]s, arrays | [[C (programming language)|C]] | 2009 | SAT-solver based |- | CVC3 | [[Linux]] | [[BSD licenses|BSD]] | {{yes|v1.2}} | {{yes}} | | [[empty theory]], linear arithmetic, arrays, tuples, types, records, bitvectors, [[Quantifier (logic)|quantifier]]s | [[C (programming language)|C]]/[[C++]] | 2010 | proof output to [[Higher-order logic|HOL]] |- | CVC4 | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]] | [[BSD licenses|BSD]] | {{yes}} | {{yes}} | | 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]], [[Microsoft Windows|Windows]] | [[BSD licenses|BSD]] | {{yes}} | {{yes}} | | rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, finite fields, 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 license|Apache]] | {{no}} | | | | [[OCaml]] | no | DPLL-based |- | iSAT | [[Linux]] | Proprietary | {{no}} | | | non-linear arithmetic | | no | DPLL-based |- | MathSAT | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]] | Proprietary | {{yes}} | | {{yes}} | [[empty theory]], linear arithmetic, nonlinear arithmetic, bitvectors, arrays | [[C (programming language)|C]]/[[C++]], [[Python (programming language)|Python]], [[Java (programming language)|Java]] | 2010 | DPLL-based |- | MiniSmt | [[Linux]] | [[LGPL]] | {{yes|partial v2.0}} | | | non-linear arithmetic |[[OCaml]] | 2010 | SAT-solver based, Yices-based |- | Norn | | | | | | | | | SMT solver for string constraints |- |- | [[OpenCog]] | [[Linux]] | [[Affero General Public License|AGPL]] | {{no}} | {{no}} | {{no}} | [[probabilistic logic]], arithmetic. [[relational model]]s | [[C++]], [[Scheme (programming language)|Scheme]], [[Python (programming language)|Python]] | no | subgraph isomorphism |- | OpenSMT | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]] | [[GPLv3]] | {{yes|partial v2.0}} | | {{yes}} | [[empty theory]], differences, linear arithmetic, bitvectors | [[C++]] | 2011 | lazy SMT Solver |- |raSAT |Linux |GPLv3 |v2.0 | | |real and integer nonlinear arithmetic | |2014, 2015 |extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem |- | SatEEn | ? | Proprietary | {{yes|v1.2}} | | | linear arithmetic, difference logic | none | 2009 | |- | SMTInterpol | [[Linux]], [[Mac OS]], [[Windows]] | [[LGPLv3]] | {{yes|v2.5|align=|style=|color=}} | | | uninterpreted functions, linear real arithmetic, and linear integer arithmetic | [[Java (programming language)|Java]] | 2012 | Focuses on generating high quality, compact interpolants. |- | SMCHR | [[Linux]], [[Mac OS]], [[Windows]] | [[GPLv3]] | {{no}} | {{no}} | {{no}} | linear arithmetic, nonlinear arithmetic, heaps | [[C (programming language)|C]] | no | Can implement new theories using [[Constraint Handling Rules]]. |- | SMT-RAT | [[Linux]], [[Mac OS]] | [[MIT License|MIT]] | {{yes|v2.0}} | {{no}} | {{no}} | linear arithmetic, nonlinear arithmetic | [[C++]] | 2015 | Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations. |- | SONOLAR | [[Linux]], [[Microsoft Windows|Windows]] | Proprietary | {{yes|partial v2.0}} | | | bitvectors | [[C (programming language)|C]] | 2010 | SAT-solver based |- | Spear | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]] | Proprietary | {{yes|v1.2}} | | | bitvectors | | 2008 | |- | STP | [[Linux]], [[OpenBSD]], [[Microsoft Windows|Windows]], [[Mac OS]] | [[MIT License|MIT]] | {{yes|partial v2.0}} | {{yes}} | {{no}} | bitvectors, arrays | [[C (programming language)|C]], [[C++]], [[Python (programming language)|Python]], [[OCaml]], [[Java (programming language)|Java]] | 2011 | SAT-solver based |- | SWORD | [[Linux]] | Proprietary | {{yes|v1.2}} | | | bitvectors | | 2009 | |- | UCLID | [[Linux]] | [[BSD licenses|BSD]] | {{no}} | {{no}} | {{no}} | [[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 licenses|BSD]] | {{yes|partial v2.0}} | | | [[empty theory]], rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols | [[C (programming language)|C]]/[[C++]] | 2010 | SAT-solver based, can produce proofs |- | {{Visible anchor|Yices}} | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]] | [[GPLv3]] | {{yes| v2.0}} | {{no}} | {{yes}} | rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols | [[C (programming language)|C]] | 2014 | Source code is available online |- | [[Z3 Theorem Prover]] | [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]] | [[MIT License|MIT]] | {{yes| v2.0}} | | {{yes}} | [[empty theory]], linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, [[Quantifier (logic)|quantifier]]s, strings | [[C (programming language)|C]]/[[C++]], [[.NET Framework|.NET]], [[OCaml]], [[Python (programming language)|Python]], [[Java (programming language)|Java]], [[Haskell (programming language)|Haskell]] | 2011 | Source code is available online |}
=== Standardization and the SMT-COMP solver competition === There are multiple attempts to describe a standardized interface to SMT solvers (and [[Automated theorem proving|automated theorem provers]], a term often used synonymously). The most prominent is the SMT-LIB standard,{{citation needed|reason=Provide a source for the standard definition; similar for other standards.|date=October 2020}} which provides a language based on [[S-expression]]s. Other standardized formats commonly supported are the DIMACS format{{citation needed|date=October 2020}} supported by many Boolean SAT solvers, and the CVC format{{citation needed|date=October 2020}} 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),<ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Stump|first3=Aaron|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|chapter=SMT-COMP: Satisfiability Modulo Theories Competition|chapter-url=https://link.springer.com/chapter/10.1007%2F11513988_4|title=Computer Aided Verification|series=Lecture Notes in Computer Science|volume=3576|publisher=Springer|pages=20–23|doi=10.1007/11513988_4|isbn=978-3-540-31686-2}}</ref><ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Ranise|first3=Silvio|last4=Stump|first4=Aaron|last5=Tinelli|first5=Cesare|date=2011|editor-last=Barner|editor-first=Sharon|editor2-last=Harris|editor2-first=Ian|editor3-last=Kroening|editor3-first=Daniel|editor4-last=Raz|editor4-first=Orna|chapter=The SMT-LIB Initiative and the Rise of SMT: (HVC 2010 Award Talk)|title=Hardware and Software: Verification and Testing|series=Lecture Notes in Computer Science|volume=6504|publisher=Springer|pages=3|doi=10.1007/978-3-642-19583-9_2|bibcode=2011LNCS.6504....3B|isbn=978-3-642-19583-9|doi-access=free}}</ref> 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).<ref>{{Cite web|title=SMT-COMP 2020|url=https://smt-comp.github.io/2020/|access-date=2020-10-19|website=SMT-COMP|language=en-US}}</ref>
==Applications== SMT solvers are useful both for verification, proving the [[correctness (computer science)|correctness]] of programs, software testing based on [[symbolic execution]], and for [[program synthesis|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]]<ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-96142-2_2|doi=10.1007/978-3-319-96142-2_2|chapter=MaxSMT-Based Type Inference for Python 3|title=Computer Aided Verification|series=Lecture Notes in Computer Science|year=2018|last1=Hassan|first1=Mostafa|last2=Urban|first2=Caterina|last3=Eilers|first3=Marco|last4=Müller|first4=Peter|volume=10982|pages=12–19|isbn=978-3-319-96141-5}}</ref><ref>Loncaric, Calvin, et al. [https://manu.sridharan.net/files/mycroft-preprint.pdf "A practical framework for type inference error explanation."] ACM SIGPLAN Notices 51.10 (2016): 781-799.</ref> and for modelling theoretic scenarios, including modelling actor beliefs in nuclear [[arms control]].<ref>{{Cite book|last1=Beaumont|first1=Paul|last2=Evans|first2=Neil|last3=Huth|first3=Michael|last4=Plant|first4=Tom|title=Computer Security -- ESORICS 2015 |chapter=Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks |date=2015|editor-last=Pernul|editor-first=Günther|editor2-last=Y A Ryan|editor2-first=Peter|editor3-last=Weippl|editor3-first=Edgar|series=Lecture Notes in Computer Science|volume=9326|publisher=Springer |pages=521–540|doi=10.1007/978-3-319-24174-6_27|isbn=978-3-319-24174-6|doi-access=free}}</ref>
===Verification<!--'CVC4' redirects here-->=== Computer-aided [[formal verification|verification of computer programs]] often uses SMT solvers. A common technique is to translate preconditions, postconditions, loop conditions, and assertions into SMT formulas in order to determine if all properties can hold.
There are many verifiers built on top of the [[Z3 Theorem Prover|Z3 SMT solver]]. [http://research.microsoft.com/en-us/projects/boogie/ Boogie] is an intermediate verification language that uses Z3 to automatically check simple imperative programs. The [https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ VCC] verifier for concurrent C uses Boogie, as well as [http://research.microsoft.com/en-us/projects/dafny/ Dafny] for imperative object-based programs, [http://research.microsoft.com/en-us/projects/chalice/ Chalice] for concurrent programs, and [http://research.microsoft.com/en-us/projects/specsharp/ Spec#] for C#. [http://research.microsoft.com/en-us/projects/fstar/ F*] is a dependently typed language that uses Z3 to find proofs; the compiler carries these proofs through to produce proof-carrying bytecode. The [http://viper.ethz.ch Viper verification infrastructure] encodes verification conditions to Z3. The [https://hackage.haskell.org/package/sbv sbv] library provides SMT-based verification of Haskell programs, and lets the user choose among a number of solvers such as Z3, ABC, Boolector, cvc5, MathSAT and Yices.
There are also many verifiers built on top of the [http://alt-ergo.ocamlpro.com/ Alt-Ergo] SMT solver. Here is a list of mature applications: * [http://why3.lri.fr/ Why3], a platform for deductive program verification, uses Alt-Ergo as its main prover; * CAVEAT, a C-verifier developed by CEA and used by Airbus; Alt-Ergo was included in the qualification DO-178C of one of its recent aircraft; * [[Frama-C]], a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins (dedicated to "deductive program verification"); * [[SPARK (programming language)|SPARK]] uses CVC4 and Alt-Ergo (behind GNATprove) to automate the verification of some assertions in SPARK 2014; * [[B-Method|Atelier-B]] can use Alt-Ergo instead of its main prover (increasing success from 84% to 98% on the [http://alt-ergo.lri.fr/documents/ABZ-2014.pdf ANR Bware project benchmarks] {{Webarchive|url=https://web.archive.org/web/20141129015810/http://alt-ergo.lri.fr/documents/ABZ-2014.pdf |date=2014-11-29 }}); * [[Rodin tool|Rodin]], a B-method framework developed by Systerel, can use Alt-Ergo as a back-end; * [http://cubicle.lri.fr/ Cubicle], an open source model checker for verifying safety properties of array-based transition systems. * [https://www.easycrypt.info/ EasyCrypt], a toolset for reasoning about relational properties of probabilistic computations with adversarial code.
Many SMT solvers implement a common interface format called [http://smt-lib.org/ SMTLIB2] (such files usually have the extension "<code>.smt2</code>"). The [https://ucsd-progsys.github.io/liquidhaskell-blog/ LiquidHaskell] tool implements a refinement type based verifier for Haskell that can use any SMTLIB2 compliant solver, e.g. cvc5, MathSat, or Z3.
===Symbolic-execution based analysis and testing===
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.{{citation needed|date=November 2021}} Example tools in this category include [http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf SAGE] from [[Microsoft Research]], [https://klee.github.io/ KLEE], [http://s2e.epfl.ch/ S2E], and [https://triton.quarkslab.com Triton]. SMT solvers that have been used for symbolic-execution applications include [https://github.com/Z3Prover/z3 Z3], [https://sites.google.com/site/stpfastprover/ STP] {{Webarchive|url=https://web.archive.org/web/20150406115407/https://sites.google.com/site/stpfastprover/ |date=2015-04-06 }}, the [https://z3string.github.io/ Z3str family of solvers], and [http://fmv.jku.at/boolector/ Boolector].{{citation needed|date=November 2021}}
===Interactive theorem proving===
SMT solvers have been integrated with proof assistants, including [[Rocq]]<ref>{{Cite book |last1=Ekici |first1=Burak |last2=Mebsout |first2=Alain |last3=Tinelli |first3=Cesare |last4=Keller |first4=Chantal |last5=Katz |first5=Guy |last6=Reynolds |first6=Andrew |last7=Barrett |first7=Clark |date=2017 |editor-last=Majumdar |editor-first=Rupak |editor2-last=Kunčak |editor2-first=Viktor |chapter=SMTCoq: A Plug-In for Integrating SMT Solvers into Coq |chapter-url=https://hal.science/hal-01669345 |title= Computer Aided Verification, 29th International Conference |series=Lecture Notes in Computer Science | volume= 10427 |language=en |location=Cham |publisher=Springer International Publishing |pages=126–133 |doi=10.1007/978-3-319-63390-9_7 |isbn=978-3-319-63390-9|s2cid=206701576 }}</ref> and [[Isabelle/HOL]].<ref>{{Cite journal |last1=Blanchette |first1=Jasmin Christian |last2=Böhme |first2=Sascha |last3=Paulson |first3=Lawrence C. |date=2013-06-01 |title=Extending Sledgehammer with SMT Solvers |url=https://doi.org/10.1007/s10817-013-9278-5 |journal=Journal of Automated Reasoning |language=en |volume=51 |issue=1 |pages=109–128 |doi=10.1007/s10817-013-9278-5 |issn=1573-0670|url-access=subscription }}</ref>
===Synthesis===
SMT solvers are a core building block in [[program synthesis]], the automated generation of programs from specifications. A prominent approach is [[counterexample-guided inductive synthesis]] (CEGIS), in which a synthesiser proposes a candidate program that is verified by an SMT solver; counterexamples from failed checks guide the synthesiser until a correct solution is found.<ref>{{cite book |last1= Abate |first1= Alessandro |last2= David |first2= Cristina |last3= Kesseli |first3= Pascal |last4= Kroening |first4= Daniel |last5= Polgreen |first5= Elizabeth |chapter= Counterexample Guided Inductive Synthesis Modulo Theories |title= Computer Aided Verification |series= Lecture Notes in Computer Science |date= 2018 |volume= 10981 |pages= 270–288 |doi= 10.1007/978-3-319-96145-3_15 |isbn= 978-3-319-96144-6 }}</ref>
A related application is [[automatic bug fixing|automatic program repair]]: given a buggy program and a test suite, an SMT formula is constructed whose solution yields a patch. For example, Nopol encodes the problem of finding a repaired conditional expression as an SMT instance, translating the solution back into a source-code patch for Java programs.<ref>{{cite journal |last1= Xuan |first1= Jifeng |last2= Martinez |first2= Matias |last3= DeMarco |first3= Favio |last4= Clement |first4= Maxime |last5= Marcote |first5= Sebastian Lamelas |last6= Durieux |first6= Thomas |last7= Le Berre |first7= Daniel |last8= Monperrus |first8= Martin |title= Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs |journal= IEEE Transactions on Software Engineering |date= January 2017 |volume= 43 |issue= 1 |pages= 34–55 |doi= 10.1109/tse.2016.2560811 |arxiv= 1811.04211 |bibcode= 2017ITSEn..43...34X }}</ref>
==See also== * [[Answer set programming]] * [[Automated theorem proving]] * [[Boolean satisfiability problem#Algorithms for solving SAT|SAT solver]] * [[First-order logic]] * [[Theory of pure equality]]
==Notes== <references />
==References== {{refbegin}} * {{cite book |first1=C. |last1=Barrett |first2=R. |last2=Sebastiani |first3=S. |last3=Seshia |first4=C. |last4=Tinelli |chapter=Satisfiability Modulo Theories |chapter-url=https://books.google.com/books?id=shLvAgAAQBAJ&q=%22Satisfiability+Modulo+Theories%22 |editor1-first=A. |editor1-last=Biere |editor2-first=M.J.H. |editor2-last=Heule |editor3-first=H. |editor3-last=van Maaren |editor4-first=T. |editor4-last=Walsh |title=Handbook of Satisfiability |publisher=IOS Press |series=Frontiers in Artificial Intelligence and Applications |volume=185 |date=2009 |isbn= 9781607503767|pages=825–885 |url=}} * {{cite thesis |first=Vijay |last=Ganesh |title=Decision Procedures for Bit-Vectors, Arrays and Integers |date=September 2007 |type=PhD |publisher=Computer Science Department, Stanford University |url=https://ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-PhD-STANFORD.pdf}} * {{cite book |first1=Susmit |last1=Jha |first2=Rhishikesh |last2=Limaye |first3=Sanjit A. |last3=Seshia |chapter=Beaver: Engineering an efficient SMT solver for bit-vector arithmetic |chapter-url= |title=Proceedings of 21st International Conference on Computer-Aided Verification |publisher= |location= |date=2009 |isbn=978-3-642-02658-4 |pages=668–674 |doi=10.1007/978-3-642-02658-4_53}} * {{cite book |first1=R.E. |last1=Bryant |first2=S.M. |last2=German |first3=M.N. |last3=Velev |chapter=Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions |chapter-url=https://kilthub.cmu.edu/articles/Microprocessor_Verification_Using_Efficient_Decision_Procedures_for_a_Logic_of_Equality_with_Uninterpreted_Functions/6607286/files/12097826.pdf |editor= |title=Analytic Tableaux and Related Methods |publisher= |location= |date=1999 |isbn= |pages=1–13 |url=}}, pp. , . * {{cite journal |first1=M. |last1=Davis |first2=H. |last2=Putnam |title=A Computing Procedure for Quantification Theory |journal=Journal of the Association for Computing Machinery |volume=7 |issue= 3|pages=201–215 |date=1960 |doi=10.1145/321033.321034 |s2cid=31888376 |url=|doi-access=free }} * {{cite journal |first1=M. |last1=Davis |first2=G. |last2=Logemann |first3=D. |last3=Loveland |title=A Machine Program for Theorem-Proving |journal=[[Communications of the ACM]] |volume=5 |issue=7 |pages=394–397 |date=1962 |doi=10.1145/368273.368557 |hdl=2027/mdp.39015095248095 |s2cid=15866917 |url=|hdl-access=free }} * {{cite book |first1=D. |last1=Kroening |first2=O. |last2=Strichman |title=Decision Procedures — an algorithmic point of view |publisher=Springer |series=Theoretical Computer Science series |date=2008 |isbn=978-3-540-74104-6 |pages= |url=https://books.google.com/books?id=anJsH3Dq5BIC&q=SMT}} * {{cite journal |first1=G.-J. |last1=Nam |first2=K.A. |last2=Sakallah |first3=R. |last3=Rutenbar |title=A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability |journal=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |volume=21 |issue=6 |pages=674–684 |date=2002 |doi=10.1109/TCAD.2002.1004311 |bibcode=2002ITCAD..21..674N |url=}} * [http://smtlib.org/ 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] * {{cite journal |first=R. |last=Sebastiani |title=Lazy Satisfiability Modulo Theories |journal=Journal on Satisfiability, Boolean Modeling and Computation |volume=3 |issue=3–4 |pages=141–224 |date=2007 |doi=10.3233/SAT190034 |citeseerx=10.1.1.100.221}} {{refend}} * This article was originally adapted from a column in the ACM [http://www.sigda.org SIGDA] [https://web.archive.org/web/20070208034716/http://www.sigda.org/newsletter/index.html e-newsletter] by [[Karem A. Sakallah]]. The original text is [http://archive.sigda.org/newsletter/2006/061215.txt available here].
[[Category:Constraint programming]] [[Category:Electronic design automation]] [[Category:Formal methods]] [[Category:Logic in computer science]] [[Category:NP-complete problems]] [[Category:Satisfiability problems]] [[Category:Satisfiability modulo theories solvers| ]]