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

  • Taking the course

    Prerequisites

    This is a Master's level course in Computer Science. The prerequisites are:
    • Programming skills in some procedural language such as Python, Java, Scala or C++. We use Python in some exercises and you should be able to learn the syntax of Python quickly if you don't know it already.
    • Fundamental data structures and algorithms, for instance the Aalto course "CS-A1140 Data Structures and Algorithms".
    • Basics on discrete mathematics.
    • Basics of propositional logic covered, e.g., in the Aalto course "CS-E4800 Artificial Intelligence". But a sufficient recap will be provided in Round 1.

    Grading

    In order to pass the course, one must:

    1. Pass the online exercises (see below) by getting a certain amount of points from them.
    2. And pass an exam before the next course instance starts in September 2022.
      The exams are as follows:
      • On December 20, 2021.
        The "course exam", registration for the course in Sisu is necessary and sufficient for taking part in this exam.
      • On February 22, 2022 (a regular exam, a separate registration in Sisu is required).

    The exams will be graded, as usual, with a grade from 0 to 5, 0 meaning "not passed".
    The grade from the online exercises will be determined by the following point limits:
    • grade 0: 0 - 199 points
    • grade 1: 200 - 349 points
    • grade 2: 350 - 499 points
    • grade 3: 500 - 649 points
    • grade 4: 650 - 799 points
    • grade 5: 800 or more points
    The total grade from the course is the rounded average of the exam grade and the online exercises grade, with the exception that both the online exercises and the exam must be passed. This is illustrated in the following table, where the x-axis gives the exam grade and the y-axis gives the online exercises points.
    Total grade calculation
    Exam grade
    0 1 2 3 4 5
    Online
    exercises
    points    		 0 - 199 0 0 0 0 0 0
    200 - 349 0 1 2 2 3 3
    350 - 499 0 2 2 3 3 4
    500 - 649 0 2 3 3 4 4
    650 - 799 0 3 3 4 4 5
    800 - 0 3 4 4 5 5

    Online exercises

    The obligatory online exercises are provided in the A+ system at https://plus.cs.aalto.fi/cs-e3220/2021/.
    They are also divided in ten rounds and each round has two deadlines:
    • Main full points deadline is roughly 2 weeks after the start of the round. Completing an exercise correctly before this deadline provides full points for the exercise.
    • Late submission deadline is after the full points deadline but before the December 2021 exam. Only 70 percent of the full points will be awarded for correct solutions submitted after the full points deadline but before the late submission deadline of the round.
    Submitting solutions after the late submission deadlines is not possible. The deadline dates and times are shown in the A+ system.

    Validity of the exercise points and personal extensions:

    • The exercise points obtained during Autumn 2021 are valid in all the exams before the next course instance starts in September 2022.
    • The exercise points from the previous course instance(s) are not valid anymore.
    • Personalized arrangements, including deadline extensions etc, can only be considered on the basis of non-short-term medical reasons (a certificate from the study administration is required), please contact a lecturer in such a case but do not provide any documents until explicitly asked for.

    The online exercises are personal assignments and thus, for instance, producing code together, copying code from others, and making one's own solutions available to others (either privately or by posting to some public forum) is not allowed. Discussing general concepts and techniques with fellow students is of course allowed, even encouraged, as long as the level of details is abstract enough so that the submitted solutions of the participating students do not start to look similar.

    Online exercise sessions and discussion forum

    In case you need help with the assignments, you can visit an exercise session or post a question in our discussion forum.
    The discussion forum, used to organize the exercise sessions as well, can be found at https://cs-e3220-2021.zulip.cs.aalto.fi/; please read these instructions for the details first!
    Due to the corona virus situation, the exercise sessions will be online only.
    The weekly exercise session schedule is:
    • Tuesdays 14:16-16:00
    • Fridays 12:15-14:00
    The exercise sessions are organized between September 17th and December 7th. Exceptions:
    • No exercise sessions from October 25 to October 29 due to the evaluation week. Naturally, you can continue solving and submitting the online exercises during this period as well if you wish, but there will be no exercise sessions or deadlines then.

  • Exams and results

    Not available unless any of:
    • You are a(n) Teacher
    • You are a(n) Non-editing teacher
    • You are a(n) Student

    Online exams, exam results and final grading will be published here.