Overview of course contents
The course gives an advanced introduction to algorithms, methods, models and applications of Boolean satisfiability. Boolean satisfiability (SAT) has emerged as the most scalable framework for automated reasoning during the last two decades, with important applications in design and analysis of computer software and hardware, artificial intelligence, and other areas. The goal of the course is to give an introduction to the most important algorithms and methods related to Boolean satisfiability and propositional logic.
The course includes
- algorithms for solving the SAT problem, including the Davis-Putnam-Logemann-Loveland procedure, the Conflict-Driven Clause Learning algorithm, as well as stochastic local search
- inference and preprocessing methods and implementation technology
- normal forms, including CNF, DNF, NNF, DNNF, OBDD
- extensions of the basic SAT problem, including weighted model-counting, optimization, SAT modulo Theories
- applications: state-space search, model-checking of finite-state systems, planning, diagnosis, probabilistic reasoning
The course starts on Monday, April 10, 2017 at 12:15. The lecture hall is T6.
The course is lectured by Tomi Janhunen, Tommi Junttila, and Jussi Rintanen.