SAT Solving (WiSe 2023/24)

Praktikum, 4-std., Johannsen

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 mainly treat these practical algorithms. The participants will first develop an application solving a puzzle by use of a state-of-the-art SAT solver. Then they will develop their own solver using the currently dominant CDCL paradigm.

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.

• Umfang: 2+2 Semesterwochenstunden
• Zeit und Ort: Plenum Dienstags 14:15-15:45 Uhr (wöchentlich), Tutorial Freitags 14:15-15:45 Uhr (nach Bedarf)
• Durchführung: Dr. Jan Johannsen