Topic outline

  • General

    Lecturers Jussi Rintanen
    Tommi Junttila
    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:

    1. Propositional logic [lecture notes, see "Material" in the online exercises of the round for more]
    2. Fundamentals of SAT solvers [lecture notes, see "Material" in the online exercises of the round for more]
    3. Constraint Satisfaction problems
    4. Transition systems
    5. Symbolic (Logic-Based) Search, Binary Decision Diagrams
    6. Symbolic Search with SAT
    7. Modal and temporal logics
    8. Model-checking in verification and validation
    9. Satisfiability Modulo Theories I
    10. Satisfiability Modulo Theories II