Kaisa_2012_3_photo by Veikko Somerpuro

** THIS COURSE WILL BE LECTURED NEXT TIME IN 2020-2021. PLEASE CONTACT THE LECTURER FOR DETAILS IN CASE YOU WISH TO PASS THE COURSE IN 2019-2020. **

From designing provably-correct safety-critical hardware and software systems to explainable AI, the ability to efficiently reason about complex systems through automated symbolic reasoning---instead of e.g. purely statistical methods---is central in various real-world problem settings where exactness is a necessity.

Boolean satisfiability (SAT), despite being an archetypical NP-complete problem, has today become a central declarative paradigm for exactly solving various important computationally hard problems. This success is based on recent breakthroughs in practical implementations of decision procedures for SAT, i.e., SAT solvers, that are today used as core procedures in various industrial and AI applications, ranging from automated hardware and software verification, planning, and scheduling, to data analysis and automated mathematical theorem proving.

This 5-credit course gives an up-to-date coverage of central computational aspects of SAT and related approaches, focusing modelling and algorithmic techniques that are important for real-world applications. Preliminary topics include: modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP; counterexample-guided search and satisfiability modulo theories.

While the course aims at being relatively self-contained, students are assumed to have good basic background on algorithms and programming from the suitable bachelor's-level courses in computer science. Knowledge of propositional logic is an asset but not a necessity. The course is primarily intended for algorithmically/mathematically oriented master's-level students and postgraduate students. Students majoring in mathematics interested in real-world applications of formal logic are also encouraged to attend.

Enrol

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

Other teaching

14.03. - 11.04.2019 Thu 14.15-16.00
25.04. - 02.05.2019 Thu 14.15-16.00
Paul Saikko
Teaching language: English

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