Português English
Contato

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

CREDITS: 1

SEMESTRES OFERECIDOS: Primeiro semestre

SUMMARY

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.

OBJECTIVES

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.

PROGRAM

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.

ACTIVITIES

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.

EVALUATION

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.

BIBLIOGRAPHY

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.