Theory and Practice of SMT Solving

Course given by DCC-UFMG

Outline

  1. Theory and Practice of SMT Solving
  2. Topic 1: SAT solving
    1. Propositional Logic
    2. Resolution
    3. Efficient CNF conversion
    4. DPLL and CDCL
    5. Efficient SAT solving
  3. Topic 2: CDCL(T) Architecture
  4. TODO

A deep dive into how SMT solvers work.

There is no required textbook for the course. We will use a variety of reading materials which will be linked from the lecture notes. That said, the following books provide important background:

  • H.B. Enderton. A Mathematical Introduction to Logic (Second Edition), Academic Press.
  • D. Kroening, O. Strichman. Decision Procedures, Springer.
  • A. Bradley, Z. Manna. The Calculus of Computation, Springer-Verlag.
  • A. Biere, M. Heule, H. van Maaren, T. Walsh. Handbook of Satisfiability (Second Edition), IOS Press.

Topic 1: SAT solving

Propositional Logic

Resolution

Efficient CNF conversion

DPLL and CDCL

Efficient SAT solving

Topic 2: CDCL(T) Architecture

TODO