Português English

Lista de Disciplinas | CMP192

Understanding and using satisfiability

Responsável: André Inácio Reis
Pré-requisitos: 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.
Carga Horária: 30h
Créditos: 02
Semestres Oferecidos: Segundo Semestre

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 and SMT (Satisfiability Modulo Theory) solvers.

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 (1) able to modify current solvers or build one their own, (2) efficiently use a sat solver or a SMT solver, (3) understand sat based approaches to problem-solving.

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 13 talks and two exams, and extra class work. 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.