Milestones in SMT solver development:

• results of Nelson and Oppen, including Nelson's dissertation
• inclusion of SAT solvers and the DPLL(T) algorithm: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)
• The SMT-LIB initiative with standardized format, benchmarks, and competitions
• The provers such as Z3 prover

Slides on CDCL SAT from the History and Overview of SAT by Sharad Malik

Introduction from Selected VeriFun slides (Full VeriFun slides are here)

Idea of Quantifier-Free Combination

Atomic Diagram Normal Form

Combining FOL Models

Eager SAT Encoding

Quantifier Instantiation

Summary:

• SAT + theories
• lazy approach and eager approach
• small models and Ackerman encoding
• quantifier instantiation

Deciding Quantifier-Free FOL

Axioms for Equality

Notes on Congruences

Congruence Closure Algorithm and Correctness

Implementing Congruence Closure

Deciding Quantifier-Free FOL over Ground Terms

• Decision Procedures Based on Congruence Closure
• Greg Nelson: Techniques for Program Verification
• Calculus of Computation Textbook
• SAT and SMT Summer school at MIT 2011
• SAT and SMT Summer school in Trento 2012
• Slides Accompanying Decision Procedures textbook
• SRI Summer School 2004