Satisfiability Modulo Theories: A Beginner’s Tutorial
Great minds have long dreamed of creating machines that can function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power and automation. This tutorial is a beginner’s guide to SMT. It includes an overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to obtain models and proofs. Throughout the tutorial, examples and exercises are provided as hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either the cvc5 or the z3 SMT solver.
- Introduction
- Overview
- Formal Foundations
- SMT Theories
- SMT Solver Outputs
- Conclusion
- References
- Solutions to Exercises
- Solution to Exercise 1
- Solution to Exercise 2
- Solution to Exercise 3
- Solution to Exercise 4
- Solution to Exercise 5
- Solution to Exercise 6
- Solution to Exercise 7
- Solution to Exercise 8
- Solution to Exercise 9
- Solution to Exercise 10
- Solution to Exercise 11
- Solution to Exercise 12
- Solution to Exercise 13