Topic outline

  • General

    Lecturers Jussi Rintanen
    Tommi Junttila
    Teaching assistant Saurabh Fadnis
    Time & place The lectures, exercises sessions and exams will be on campus. The material and exercises will be available online.
    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 2023 edition of the course starts on September 6, welcome!

    • The participation of the course includes reading the course material, completing exercises, and taking an exam. Participation in lectures and exercise sessions is not obligatory.
    • To get help in the exercises, weekly exercise sessions are organized.
    • For the grading principles, please see the "Taking the course" section.
    • In order to obtain the credits, access the exercise system, and get the course announcements, please remember to register to the course in Sisu.

    The 10 rounds of the course are as follows (a tentative schedule):

    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 (September 27)
    5. Symbolic (Logic-Based) Search, Binary Decision Diagrams (October 4 lecture moved to Thursday October 5 at 10:15am in hall T1)
    6. Symbolic Search with SAT (October 11)
    7. Modal and temporal logics (October 25 lecture moved to Friday October 27 at 12:15-14:00 in hall T1)
    8. Model-checking in verification and validation  (November 1)
    9. Satisfiability Modulo Theories I (November 8)
    10. Satisfiability Modulo Theories II (November 15)