Satisfiability and Theories
Андрей Воронков · 2009
Summary form only given. We give a simple introduction to satisfiability modulo theories intended for non-specialists. No previous background is assumed. The tutorial covers the following topics. 1) Propositional satisfiability. 2) DPLL as the main method for satisfiability checking. 3) Implementations of DPLL. 4) Theories. 5) Decision procedures for theories. Congruence closure, the theory of arrays and linear arithmetic. 6) SMT: satisfiability modulo theories. How to convert a decision procedure for a set of literals to a DPLL modulo theory algorithm. 7) Satisfiability in a combination of theories. Instead of proving theorems, we will try to explain the main ideas using examples. The tutorial serves as a background for the second tutorial by Nikolaj Bjorner "SMT solvers for Testing, Program Analysis and Verification at Microsoft".