SAT Solving

Vorlesung, 3-std., Johannsen; Übungen 1-std., Kondylidou

Content

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(2^n) for brute-force search. The current best such (probabilistic) algorithms have a run-time of O(1.307^n) for 3-SAT and O(1.469^n) 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.

Prerequisites

Knowledge of basic algorithmic techniques, as taught in the module Algorithmen und Datenstrukturen, and of the basics of computational complexity, as taught in the modules Formale Sprachen und Komplexität or Theoretische Informatik für Medieninformatiker, is required.

Organisation

The course will be held in English. The lecture and tutorial will take place in person at the time and place given below. The tutorial will take place approximately every 2nd week in the Thursday slot. The preliminary dates for the tutorials are: 26.10., 09.11., 23.11., 07.12., 21.12., 18.01., and 01.02.

• Umfang: 3+1 Semesterwochenstunden
• Zeit und Ort: Dienstags 16:15-17:45 Uhr, Hörsaal F 007 (HGB) und Donnerstags 14:10-15:40 Uhr, Hörsaal M 010 (HGB)
• Vorlesung: Dr. Jan Johannsen
• Übung: Lydia Kondylidou

Please register for the course in Moodle. All further information will be provided there. The registration key is: SAT_WS23-24

Communication

There is an official chat-stream TCS-23W-SAT for the course at the institute’s chat server, where the topics and organisation of the course can be discussed, and questions will be answered. This is our preferred communication channel, therefore, all participants are encouraged to subscribe to this channel.

A manuscript (in german) is in preparation, so far drafts of chapters 1-3 and 5 are available. I am grateful for any corrections and hints for improvement.

Credits

The course can be credited for the modules Algorithmik und Komplexität in the Informatik Master program, or Vertiefende Themen der Informatik für Master in the Medieninformatik/MCI master program, as well as for Vertiefende Themen der (Medien-)Informatik in the Informatik or Medieninformatik bachelor programs.

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 2 to 3 participants. After each due date, there will be an oral presentation and review of the projects. The preliminary issue and due dates for the projects are:

• Project 1: issued October 26, due November 23
• Project 2: issued November 23, due January 18
• Project 3: issued January 18, due in early to mid March (date tbd)

Participants who have been granted a compensation for disadvantages (Nachteilsausgleich) for exams should contact us immediately, before the first project is issued.