Kaisa_2012_3_photo by Veikko Somerpuro

Enrol
11.2.2019 at 09:00 - 2.5.2019 at 23:59

Timetable

Here is the course’s teaching schedule. Check the description for possible other schedules.

DateTimeLocation
Mon 11.3.2019
14:15 - 16:00
Wed 13.3.2019
14:15 - 16:00
Mon 18.3.2019
14:15 - 16:00
Wed 20.3.2019
14:15 - 16:00
Mon 25.3.2019
14:15 - 16:00
Wed 27.3.2019
14:15 - 16:00
Mon 1.4.2019
14:15 - 16:00
Wed 3.4.2019
14:15 - 16:00
Mon 8.4.2019
14:15 - 16:00
Wed 10.4.2019
14:15 - 16:00
Mon 15.4.2019
14:15 - 16:00
Wed 17.4.2019
14:15 - 16:00
Mon 22.4.2019
14:15 - 16:00
Wed 24.4.2019
14:15 - 16:00
Mon 29.4.2019
14:15 - 16:00
Wed 1.5.2019
14:15 - 16:00

Description

Students from Master's Programme in Computer Science. Available also to students from other degree programmes.

CSM12101 Design and Analysis of Algorithms.

Courses in the Discrete Algorithms study module.

Recommended further studies: CSM12107 Combinatorial Optimization.

Explains the syntax and semantics of propositional logic and normal forms. Models NP search problems using propositional satisfiability. Explains key search techniques in modern SAT solvers. Simulates the DPLL and CDCL SAT solver algorithms. Derives resolutions proofs. Simulates preprocessing rules. Identifies tractable SAT instances. Explains differences and connections between NP-hard decision, search and enumeration, and counting problems. Explains minimal unsatisfiability, maximum satisfiability, and central algorithmic approaches to them. Explains and gives concrete examples of the counterexample-guided abstraction refinement approach. Represents SAT instances using BDDs. Develops and applies SAT solvers to solve instances of NP-hard decision, search, and enumeration problems in practice.

1st or 2nd year of MSc studies. After the course CSM12101 Design and Analysis of Algorithms.

Spring term, period IV, biannually (first time in Spring 2019).

Propositional satisfiability (SAT), syntax and semantics, normal forms and structural representations. Modelling NP-complete real-world problems with SAT. Modern SAT solving algorithms and search techniques, DPLL, conflict-driven clause learning. Resolution and SAT solvers. Preprocessing. Tractable fragments of SAT. Minimal unsatisfiability, maximum satisfiability. Building complex SAT-based procedures, counterexample-guided abstraction refinement, satisfiability modulo theories. Model counting. Knowledge compilation, binary decision diagrams.

The course does not follow any textbook directly.

Lecture slides and tutorials. A list of recommended supplementary literature will be provided when the course begins.

The course activities may vary per instantiation of the course.

The core study material consists of online lecture materials. Weekly lectures present the core study material with additional explanation and examples. Active participation in the lectures by the students is encouraged to support learning.

Students are given exercise problems geared towards learning the knowledge and skills described in the learning outcomes. Students present their solutions in weekly tutorials either in person or in electronic form (as instructed in the individual exercise sheets) and discuss them with a teacher to obtain feedback. The exercise problems may range from theoretical problems to implementation-level tasks.

Homework assignments (passed), final grade based on final exam, grading scale 0-5.

Contact teaching consisting of 2x 2 h lectures and 1x 2 h tutorials weekly. Other forms of activities, such as programming tasks as homework, are also possible.

Completion requirements: homework and final exam.

Matti Järvisalo