Parameterized Algorithms and Implementations for SAT and Generalizations
Many fundamental problems in the area of reasoning and artificial intelligence in general are known to be NP-hard, famous examples are SAT, model counting (#SAT), and weighted model counting (WMC), which can be used in probabilistic and behavioral reasoning.
Under standard complexity theoretical assumptions, it is quite unlikely that efficient algorithms for these problems on arbitrary input instances exist. However, problem instances that originate in practical applications are often structured in a way that facilitate obtaining a solution relatively fast. Such instances appear to be harder in theory than they are in practice, especially for problems such as solving SAT, #SAT, and WMC.
In the course, we consider practical problem solving in SAT, #SAT, and WMC, including concepts and algorithms of actual implementations and applications. Further, we look at parameterized complexity and its fundamentals with a focus on solving SAT and model counting exploiting the parameter treewidth and if time techniques to obtain algorithm lower bounds.
Students will have the chance to take a closer look at solvers, including sequential and parallel implementations, and experimenting and benchmarking with solvers. The course is accompanied by hands on tutorials and assignments on practical exercises how to use SAT solvers and techniques from parameterized algorithmics for problems solving.
After latest decisions from the VR of Studies, the course will take part as online course for the full semester.
We start from April 15th, 2020 with self studying and home exercises.
From May 6th, 2020 on I will try to prepare online sessions or lecture videos for self download.
Regular Course Dates: