Lecturers Jussi Rintanen
Teaching assistant Saurabh Fadnis Time & place The material, exercises, and exercise sessions are all online. The exam organization (classroom or online) is yet to be decided. Topics
- Constraint programming and constraint satisfaction
- The propositional satisfiability problem SAT
- Algorithms for solving SAT, CSP
- Normal forms and symbolic data structures such as Binary Decision Diagrams (BDD)
- Symbolic state-space traversal
- Linear Temporal Logic LTL, computer-aided verification
- Model-checking with LTL
- Arithmetic constraints and SAT modulo Theories (SMT)
- Real-world applications (software engineering, electronic design automation, artificial intelligence)
The Autumn 2021 edition of the course starts on September 15, welcome!
- Please see these slides for a high-level introduction to the topic.
- The participation of the course includes reading the course material, viewing the lecture videos, completing online exercises, and taking an exam.
- To get help in the exercises, weekly online exercise sessions are organized.
- For the grading principles, and instructions for the online exercise sessions, please see the "Taking the course" section.
- In order to get the credits and the course announcements, please remember to register to the course in Sisu.
The 10 rounds of the course are as follows:
- Propositional logic [lecture notes, see "Material" in the online exercises of the round for more]
- Fundamentals of SAT solvers [lecture notes, see "Material" in the online exercises of the round for more]
- Constraint Satisfaction problems
- Transition systems
- Symbolic (Logic-Based) Search, Binary Decision Diagrams
- Symbolic Search with SAT
- Modal and temporal logics
- Model-checking in verification and validation
- Satisfiability Modulo Theories I
- Satisfiability Modulo Theories II