Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2018/19 / SAT Solving


SAT Solving


The satisfiability problem for classical propositional logic (SAT) is the canonical NP-complete problem, therefore algorithms for solving it are of essential importance for theoretical computer science, their development and study forms an entire area of research.

Recently there has been a lot of progress in this area, in theory as well as in practice. On the theoretical side, there are new algorithms for which worst-case upper bounds on the run-time can be proven, that are better than the obvious O(2n) for brute-force search. The current best such (probabilistic) algorithms have a run-time of O(1.308n) for 3-SAT and O(1.469n) for 4-SAT.

On the other hand, there are very good heuristics and implementations for the classic backtracking algorithms (DPLL), which can solve even very large inputs with hundred thousands of variables and millions of clauses in reasonably short time. These so-called SAT solvers have by now such a good performance that they are routinely used in applications for the solution of combinatorial optimization problems.

The course will treat these theoretical and practical algorithms, as well as some methods for proving lower bounds, and also some applications. The course will be held in English.


There will be no oral or written exam. Instead, in order to obtain the credits for the course, the participants will have to successfully complete a number of small implementation projects specified in the problem sets. These projects can be done in teams of up to 3 participants. An approximate schedule for the problem completion is:

  • 10-25: first project issued
  • 11-15: first project due, second project issued
  • 12-20: second project due, third project issued
  • 02-07: third project due.

After each due date, there will be an oral presentation and review of the projects.


  • Umfang: 3+1 Semesterwochenstunden
  • Vorkenntnisse: Algorithmen und Datenstrukturen und Formale Sprachen und Komplexität bzw. Theoretische Informatik für Medieninformatiker
  • Vorlesung & Übung: Dr. Jan Johannsen, Leah Neukirchen

Die Vorlesung wird anerkannt:

  • für Studierende im Studiengang Informatik Master für das Modul Algorithmik und Komplexität
  • für Studierende im Studiengang Medieninformatik Master für das Modul Vertiefende Themen der Informatik für Master
  • für Studierende in den Studiengängen Informatik und Medieninformatik Bachelor für das Modul Vertiefende Themen der (Medien-) Informatik
  • für Studierende mit Nebenfach Informatik nach Vereinbarung

Time and Place

Lecture Di, 16-18 Uhr Raum A 022 (Hauptgebäude)
Lecture / Tutorial Do, 14-16 Uhr Raum V 002 (Prof.-Huber-Platz 2)



A manuscript (in German) is in preparation, a draft of the first three chapters and of chapter 5 is available. The draft will be extended soon. I am grateful for any corrections or hints for improvement.


U. Schöning and J. Torán, The Satisfiability Problem: Algorithms and Analyses, Lehmans 2013, ISBN 978-3865415271


The tutorials will be held every two weeks in the Thursday timeslot of the course, first on October 25.