Abstract
Satisfiability modulo theories (SMT) are concerned with mathematical formulas that combine propositional logic and decidable (or sometimes semi-decidable) mathematical theories: non-interpreted functions, various arithmetic theories (real or integer linear programming, difference inequalities, Presburger arithmetic with addition and comparisons, etc.), array theory, bitvector manipulation, pointer theories for memory management, etc. Like SMT solvers, SAT solvers are making steady progress, both in terms of efficiency and applications. Like SMT solvers, SAT solvers are making constant progress, both in terms of efficiency and applications. They are increasingly used in static analysis and program verification, constraint programming, optimization and more. For example, as Thomas Jensen demonstrated in his seminar on November 4, 2015, and as Sylvain Conchon will show in his seminar today, the strong coupling of a well-designed programming language and a powerful SMT system enables efficient bug detection as early as program writing, and even complete formal proof of programs in some cases.
The formulas processed by SMT solvers allow logic and various theories to interact very freely. The solvers finely decompose them to build propositional formulas such that each atom belongs to a single theory, while allowing the sharing of variables between atoms. We show how satisfiability analysis of CNFs obtained by SAT solvers interacts with solvers for particular theories, and detail the difficulties of this interaction. We present the main theories used in practice, and the algorithms on which they are based. Finally, we show how quantifiers can be introduced to simplify and generalize formulas, while losing decidability in the most controlled way possible. All this is illustrated by examples related to program verification.
