Satisfiability modulo theories

From HandWiki
Short description: 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.

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 a binary-valued function of non-binary variables. Example predicates include linear inequalities (e.g., [math]\displaystyle{ 3x + 2y - z \geq 4 }[/math]) or equalities involving uninterpreted terms and function symbols (e.g., [math]\displaystyle{ f(f(u, v), v) = f(u, v) }[/math] where [math]\displaystyle{ 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 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). Other theories include the theories of arrays and list structures (useful for modeling and verifying computer 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 [math]\displaystyle{ x - y \gt c }[/math] for variables [math]\displaystyle{ x }[/math] and [math]\displaystyle{ y }[/math] and constant [math]\displaystyle{ c }[/math].

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

Relationship to automated theorem proving

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.[1] The line is blurry enough that some ATPs participate in SMT-COMP, while some SMT solvers participate in CASC.[2]

Expressive power

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.[citation needed] SMT solvers have also been extended to solve formulas in higher-order logic.[3]

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 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]\displaystyle{ 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-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.[4]

Dubbed DPLL(T),[5] 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.

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.[6]

Another line of research involves the development of specialized decidable theories, including linear arithmetic over rationals and integers, fixed-width bitvectors,[7] floating-point arithmetic (often implemented in SMT solvers via bit-blasting, i.e., reduction to bitvectors),[8][9] strings,[10] (co)-datatypes,[11] sequences (used to model dynamic arrays),[12] finite sets and relations,[13][14] separation logic,[15] finite fields,[16] 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.[17] Monotonic theories support only boolean variables (boolean is the only sort), and all their functions and predicates p obey the axiom

[math]\displaystyle{ 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 graph reachability, collision detection for convex hulls, minimum cuts, and computation tree logic.[18] Every Datalog program can be interpreted as a monotonic theory.[19]

SMT for undecidable theories

Most of the common SMT approaches support 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 functions. This fact motivates an extension of the SMT problem to non-linear theories, such as determining whether the following equation is satisfiable:

[math]\displaystyle{ \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 \lt -34.4 \vee \exp(x) \gt {y \over x}\right) \end{array} }[/math]

where

[math]\displaystyle{ b \in {\mathbb B}, x,y \in {\mathbb R}. }[/math]

Such problems are, however, undecidable in general. (On the other hand, the theory of real closed fields, and thus the full first order theory of the real numbers, are 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,[20] which employs a classical DPLL(T) architecture with a non-linear optimization packet as (necessarily incomplete) subordinate theory solver, iSAT, building on a unification of DPLL SAT-solving and interval constraint propagation called the iSAT algorithm,Cite error: Closing </ref> missing for <ref> tag[21] 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).[22]

Applications

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[23][24] and for modelling theoretic scenarios, including modelling actor beliefs in nuclear arms control.[25]

Verification

Computer-aided 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 SMT solver. Boogie is an intermediate verification language that uses Z3 to automatically check simple imperative programs. The VCC verifier for concurrent C uses Boogie, as well as Dafny for imperative object-based programs, Chalice for concurrent programs, and Spec# for C#. F* is a dependently typed language that uses Z3 to find proofs; the compiler carries these proofs through to produce proof-carrying bytecode. The Viper verification infrastructure encodes verification conditions to Z3. The 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 Alt-Ergo SMT solver. Here is a list of mature applications:

  • 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 uses CVC4 and Alt-Ergo (behind GNATprove) to automate the verification of some assertions in SPARK 2014;
  • Atelier-B can use Alt-Ergo instead of its main prover (increasing success from 84% to 98% on the ANR Bware project benchmarks);
  • Rodin, a B-method framework developed by Systerel, can use Alt-Ergo as a back-end;
  • Cubicle, an open source model checker for verifying safety properties of array-based transition systems.
  • EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code.

Many SMT solvers implement a common interface format called SMTLIB2 (such files usually have the extension ".smt2"). The 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] 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.[citation needed]

Interactive theorem proving

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

See also

Notes

  1. ↑ Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers" (in en). Journal of Automated Reasoning 51 (1): 109–128. doi:10.1007/s10817-013-9278-5. ISSN 1573-0670. https://doi.org/10.1007/s10817-013-9278-5. "ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.". 
  2. ↑ Weber, Tjark; Conchon, Sylvain; Déharbe, David; Heizmann, Matthias; Niemetz, Aina; Reger, Giles (2019-01-01). "The SMT Competition 2015–2018" (in en). Journal on Satisfiability, Boolean Modeling and Computation 11 (1): 221–259. doi:10.3233/SAT190123. https://content.iospress.com/articles/journal-on-satisfiability-boolean-modeling-and-computation/sat190123. "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.". 
  3. ↑ Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark (2019). "Extending SMT solvers to higher-order logic". Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings. Springer. pp. 35–54. doi:10.1007/978-3-030-29436-6_3. hal-02300986. ISBN 978-3-030-29436-6. https://hal.archives-ouvertes.fr/hal-02300986/document. 
  4. ↑ Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Hanna, Ziyad; Nadel, Alexander; Palti, Amit; Sebastiani, Roberto (2007). "A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems". in Damm, Werner; Hermanns, Holger (in en). Computer Aided Verification. Lecture Notes in Computer Science. 4590. Berlin, Heidelberg: Springer. pp. 547–560. doi:10.1007/978-3-540-73368-3_54. ISBN 978-3-540-73368-3. https://link.springer.com/chapter/10.1007/978-3-540-73368-3_54. 
  5. ↑ Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)", Journal of the ACM, 53, pp. 937–977, doi:10.1145/1217856.1217859, http://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf 
  6. ↑ de Moura, Leonardo; Bjørner, Nikolaj (August 12–15, 2008). "Automated Reasoning". in Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (in en). 4th International Joint Conference on Automated Reasoning, Sydney, NSW, Australia. Berlin, Heidelberg: Springer. pp. 410–425. doi:10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7. 
  7. ↑ Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors". in Biere, Armin; Bloem, Roderick (in en). Computer Aided Verification. Lecture Notes in Computer Science. 8559. Cham: Springer International Publishing. pp. 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9. https://link.springer.com/chapter/10.1007/978-3-319-08867-9_45. 
  8. ↑ Brain, Martin; Schanda, Florian; Sun, Youcheng (2019). "Tools and Algorithms for the Construction and Analysis of Systems". in Vojnar, Tomáš; Zhang, Lijun (in en). 25th International Conference, Tools and Algorithms for the Construction and Analysis of Systems 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I. Cham: Springer International Publishing. pp. 79–98. doi:10.1007/978-3-030-17462-0_5. ISBN 978-3-030-17462-0. 
  9. ↑ Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "Computer Aided Verification". in Dillig, Isil; Tasiran, Serdar (in en). 31st International Conference, Computer Aided Verification 2019, New York City, July 15–18, 2019. Cham: Springer International Publishing. pp. 116–136. doi:10.1007/978-3-030-25543-5_8. ISBN 978-3-030-25543-5. 
  10. ↑ Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). "A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings". in Lutz, Carsten; Ranise, Silvio (in en). Frontiers of Combining Systems. Lecture Notes in Computer Science. 9322. Cham: Springer International Publishing. pp. 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0. https://link.springer.com/chapter/10.1007/978-3-319-24246-0_9. 
  11. ↑ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "A Decision Procedure for (Co)datatypes in SMT Solvers". in Felty, Amy P.; Middeldorp, Aart (in en). Automated Deduction - CADE-25. Lecture Notes in Computer Science. 9195. Cham: Springer International Publishing. pp. 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6. https://link.springer.com/chapter/10.1007/978-3-319-21401-6_13. 
  12. ↑ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz et al. (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences" (in en). Journal of Automated Reasoning 67 (3): 32. doi:10.1007/s10817-023-09682-2. ISSN 1573-0670. https://doi.org/10.1007/s10817-023-09682-2. 
  13. ↑ Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT". in Olivetti, Nicola; Tiwari, Ashish (in en). Automated Reasoning. Lecture Notes in Computer Science. 9706. Cham: Springer International Publishing. pp. 82–98. doi:10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1. https://link.springer.com/chapter/10.1007/978-3-319-40229-1_7. 
  14. ↑ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "Relational Constraint Solving in SMT". in de Moura, Leonardo (in en). Automated Deduction – CADE 26. Lecture Notes in Computer Science. 10395. Cham: Springer International Publishing. pp. 148–165. doi:10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5. https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10. 
  15. ↑ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT". in Artho, Cyrille; Legay, Axel; Peled, Doron (in en). Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. 9938. Cham: Springer International Publishing. pp. 244–261. doi:10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. https://hal.archives-ouvertes.fr/hal-01418883/file/Atva2016-2.pdf. 
  16. ↑ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfiability Modulo Finite Fields". in Enea, Constantin; Lal, Akash (in en). Computer Aided Verification. Lecture Notes in Computer Science. 13965. Cham: Springer Nature Switzerland. pp. 163–186. doi:10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8. 
  17. ↑ Bayless, Sam; Bayless, Noah; Hoos, Holger; Hu, Alan (2015-03-04). "SAT Modulo Monotonic Theories" (in en). Proceedings of the AAAI Conference on Artificial Intelligence 29 (1). doi:10.1609/aaai.v29i1.9755. ISSN 2374-3468. https://ojs.aaai.org/index.php/AAAI/article/view/9755. 
  18. ↑ Klenze, Tobias; Bayless, Sam; Hu, Alan J. (2016). "Fast, Flexible, and Minimal CTL Synthesis via SMT". in Chaudhuri, Swarat; Farzan, Azadeh (in en). Computer Aided Verification. Lecture Notes in Computer Science. 9779. Cham: Springer International Publishing. pp. 136–156. doi:10.1007/978-3-319-41528-4_8. ISBN 978-3-319-41528-4. https://link.springer.com/chapter/10.1007/978-3-319-41528-4_8. 
  19. ↑ Bembenek, Aaron; Greenberg, Michael; Chong, Stephen (2023-01-11). "From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems". Proceedings of the ACM on Programming Languages 7 (POPL): 7:185–7:217. doi:10.1145/3571200. https://dl.acm.org/doi/10.1145/3571200. 
  20. ↑ Bauer, A.; Pister, M.; Tautschnig, M. (2007), "Tool-support for the analysis of hybrid systems and models", Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07), IEEE Computer Society, p. 1, doi:10.1109/DATE.2007.364411, ISBN 978-3-9810801-2-4 
  21. ↑ Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). "The SMT-LIB Initiative and the Rise of SMT: (HVC 2010 Award Talk)". in Barner, Sharon; Harris, Ian; Kroening, Daniel et al.. Hardware and Software: Verification and Testing. Lecture Notes in Computer Science. 6504. Springer. pp. 3. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9. Bibcode: 2011LNCS.6504....3B. 
  22. ↑ "SMT-COMP 2020" (in en-US). https://smt-comp.github.io/2020/. 
  23. ↑ Hassan, Mostafa; Urban, Caterina; Eilers, Marco; Müller, Peter (2018). "MaxSMT-Based Type Inference for Python 3". Computer Aided Verification. Lecture Notes in Computer Science. 10982. pp. 12–19. doi:10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5. https://link.springer.com/chapter/10.1007/978-3-319-96142-2_2. 
  24. ↑ Loncaric, Calvin, et al. "A practical framework for type inference error explanation." ACM SIGPLAN Notices 51.10 (2016): 781-799.
  25. ↑ Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). "Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks". in Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar. Computer Security -- ESORICS 2015. Lecture Notes in Computer Science. 9326. Springer. pp. 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6. 
  26. ↑ Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: A Plug-In for Integrating SMT Solvers into Coq". in Majumdar, Rupak; Kunčak, Viktor (in en). Computer Aided Verification, 29th International Conference. Lecture Notes in Computer Science. 10427. Cham: Springer International Publishing. pp. 126–133. doi:10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. https://hal.archives-ouvertes.fr/hal-01669345/file/main.pdf. 
  27. ↑ Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers" (in en). Journal of Automated Reasoning 51 (1): 109–128. doi:10.1007/s10817-013-9278-5. ISSN 1573-0670. https://doi.org/10.1007/s10817-013-9278-5. 

References

This article was originally adapted from a column in the ACM SIGDA e-newsletter by Prof. Karem A. Sakallah. Original text is available here



Retrieved from "https://handwiki.org/wiki/index.php?title=Satisfiability_modulo_theories&oldid=3382431"