Português English

Lista de Disciplinas | CMP594

Tópicos Especiais em Computação DXCIV: The Quest for Efficient SAT Solvers

RESPONSÁVEL: André Inácio Reis

PREREQUISITES: Students are assumed to have good background the basics of propositional logic, algorithms and C programming from the suitable bachelor’s-level courses in computer science.

HOURS: 15 hs




This course gives an up-to-date coverage of central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT.


The purpose of this course is to provide students an introduction to the area of satisfiability and the development of an efficient solver. At the end of the course is expected that the student knows the basic internal structure of state-of-art solvers. After successful completion of the course, the students are expected to be able to modify current solvers or build one their own.


Basics of SAT. Complete algorithms for SAT: The Davis-Putnam algorithm (DP). Unit propagation. Resolution. Complete algorithms for SAT: The Davis-Putnam-Logemann-Loveland algorithm (DPLL). Backtraking. Backjumping. Lazy data structures. Branching. Complete algorithms for SAT: CDCL. Conflict analysis. Restarts: Luby, Glucose. VSIDS Branching Heuristic. Clause database management.


The course consists of four talks and around 20 hours of extra class work. The four talks will be given at room AUD1 from 13:30 to 15:10 on April 4th, 6th, 11th and 13th 2017. The extra class work will be passed through the moodle system and is composed of SAT code development tasks as well as some tests on moodle.


The extra class work on the moodle system will be graded. Students with a success rate of 90% or more will receive grade A. Students with a success rate between 90% and 75% will receive grade B. Students with a success rate between 60% and 75% will receive grade C. Students with a success rate inferior to 60% will receive grade D. Students that fail to participate at least of 75% of the activities will receive grade FF.


The course material consists of the lectures, lecture slides, and the tutorials. The course is not based on any single book, and it is not necessary to purchase a book in order to successfully complete the course. However, the following materials are helpful.
[1] A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands.
[2] The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability by Donald E. Knuth.
[3] Lecture Notes on SAT, by Bruno Schmitt.