The course is divided into severial sessions. Each session covers an specific topic of SAT solving. The slides summarize the main ideas, using examples to make it accessible. At the end of each session, a list of papers to get deeper into the topic are given. The material is designed to cover 20 hours of class, 4 of which will be used to solve an exercise.

- Introduccion to Propositional Logic
- The original DPLL algorithm
- Resolution in Propositional Logic
- Conflict-Driven-Clause-Learning (CDCL) SAT solvers
- Class exercise:SAT encoding [generator.cpp]
- Preprocessing SAT instances
- Extracting unsatisfiable proofs from CDCL SAT solvers
- A little bit more of SAT and beyond

(Material developed by Albert Oliveras and Enric Rodriguez)

The course consists of several sessions, each one of them focusing on an specific aspect of SMT. As in the LAI course, slides contain mostly high-level ideas: details can be found at the references suggested at the end of each session. The material provided is designed to cover 20 hours of class, 4 of which will be used to solve an exercise.

- Introduccion to Satisfiability Modulo Theories
- Design of a solver for EUF
- Design of a solver for Difference Logic
- Class exercise: SMT encoding [generator.cpp]
- Combining Decision Procedures: the Nelson-Oppen approach
- SLAM

(Material developed by Albert Oliveras and Enric Rodriguez)