Theory of Satisfiability Algorithms

Lecturer: Marvin Künnemann

Lecture Dates (21.04. to 28.07.):

• Tuesday, 14:00 - 15:30, InformatiKOM II – 50.28 Seminarraum 1

The Satisfiability (SAT) problem for Boolean formulas is fundamental for computer science, due to a variety of applications (cf. the practical success of SAT solvers) as well as its central role for the theory of computation. This course focuses on theoretical aspects of the problem, which includes topics among:

• exponential-time algorithms with provable worst-case guarantees (e.g., for k-SAT, CNF-SAT and further variants)
• tractable special cases of the problem
• classification of constraint satisfaction problems
• combinatorial insights (e.g., the algorithmic Lovasz Local Lemma)
• the sparsification lemma and its limits
• generalizations: MaxSAT, #SAT, Quantified SAT
• hardness hypotheses and their implications: ETH, SETH, NSETH, MASETH, Formula-SETH
• isolation lemma

Basic knowledge of algorithms and data structures (e.g., Algorithms 1) and theoretical computer science (e.g., TGI) is assumed. Basic knowledge in the analysis of randomized algorithms may be helpful (e.g., Probability and Computing), but is not a strict requirement.

TBA