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.
General exams last 3 hours and 30 minutes. Renewal exam (marked with "(U)") is the first general exam after the course and also a renewal exam of course exam(s). In a renewal exam the points student has earned during the course are taken into account. Exams marked with "(HT)" are allowed only to students who have completed the obligatory projects or other exercises included in those courses. Exams marked with "(HT/U)" are renewals to students who have completed the obligatory projects during the course. General exams might cover different area than the lectured course. Check the course web page and contact the responsible teacher if in doubt.
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.