Number of hours
- Lectures 18.0
- Projects -
- Tutorials -
- Internship -
- Laboratory works -
- Written tests -
ECTS
ECTS 3.0
Goal(s)
Understanding how decision procedures for SAT (Boolean satisfiability) and SMT (SAT enriched with arithmetic etc.) work, and how to use them in practice.
These procedures can be used in automatic analysis of software or hardware, in combinatorial optimisation or in search for solutions in operation research.
Responsible(s)
David MONNIAUX
Content(s)
- Basics in logic
- SAT algorithms: DPLL, CDCL
- BDD (binary decision diagrams) algorithmics
- SMT (satisfiability modulo theory) algorithmics
- Lab classes: using a SMT solver
Basic mathematical logic: Boolean operators, quantifiers
Algorithmics
Programming
Test
Small practical development work + written final exam
70% exam at the end of the course
30% practical assignment
The exam is given in english only 
Calendar
The course exists in the following branches:
- Curriculum - Master in Computer Science - Semester 9 (this course is given in english only
)
Additional Information
Course ID : WMM9MO46
Course language(s):
You can find this course among all other courses.
Bibliography
Kroening & Strichman, Decision procedures
Bradley & Manna, The calculus of computation
Biere et al, ed., The Handbook of Satisfiability