Satisfiability modulo theories: Introduction and applications

Leonardo de Moura, Nikolaj Bjørner
[doi] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 23 June 2020

Communications of the ACM 54(9)
Association for Computing Machinery
New York, NY, USA
Pages 69-77
September 2011
Note(s): SAT solver, SMT solver, survey
Papers: malik:cacm:2009

This paper is a great intro/overview of SMT solver: what it is, how it builds on SAT, an example of how one particular theory (difference arithmetic) is implemented, and the many applications of SMT solvers in program analysis, program verification, etc.

Worth reading in conjunction with the SAT solver intro/overview in malik:cacm:2009,

  • Boolean satisfiability from theoretical hardness to practical success [malik:cacm:2009]