Logic and Algebra in Computer Science (LAI)

In this part of the course, we will focus on the use of propositional logic in Computer Science. More specifically, the goal of the course is to understand how a SAT solver works. The course is self-contained, i.e. no strong background in logics is required. Do not expect deep theorems, our aim is to understand the real insights of SAT solvers so to understand why they have had such a big impact in areas such as software and hardware verification.

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.
  1. Introduccion to Propositional Logic

  2. The original DPLL algorithm

  3. Resolution in Propositional Logic

  4. Conflict-Driven-Clause-Learning (CDCL) SAT solvers

  5. Class exercise:SAT encoding [generator.cpp]

  6. Preprocessing SAT instances

  7. Extracting unsatisfiable proofs from CDCL SAT solvers

  8. A little bit more of SAT and beyond

  9. (Material developed by Albert Oliveras and Enric Rodriguez)

Deduction and Verification Techniques (TDV)

This part of the course will be devoted to the study of Satisfiability Modulo Theories (SMT). We will try to understand how an SMT solver works, which components it has, some rough ideas about how to implement an SMT system, how to use an SMT system and learn some of the applications it has. Although the course is mostly self-contained, it is recommended to have taken the LAI course.

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.
  1. Introduccion to Satisfiability Modulo Theories

  2. Design of a solver for EUF

  3. Design of a solver for Difference Logic

  4. Class exercise: SMT encoding [generator.cpp]

  5. Combining Decision Procedures: the Nelson-Oppen approach

  6. SLAM

  7. (Material developed by Albert Oliveras and Enric Rodriguez)