Lecture: Practical SAT Solving
Summer Term 2026 • GitHub repository • Web page • Karlsruhe Institute of Technology (KIT)
This lecture with exercises is offered by Ashlin Iser (ITI Sanders) and Dominik Schreiber (KASTEL-VADS SAtRes), with Niccolò Rigi-Luperti (SAtRes) serving as co-manager of exercises.
The lecture provides a friendly and practical overview of propositional satisfiability (SAT) solving, covering its theoretical background, important algorithms and techniques, parallelization, proofs, applications, and related tools (MaxSAT, SMT). No particular prior knowledge beyond basic foundations of computer science is required.
All lectures and exercises take place at 15:45 in building 50.34 room 301.
Our first appointment is the lecture on Monday, April 20.
Lectures
We try to link each slide set here shortly before the lecture takes place.
See also the page from last year.
(to be extended)
- Monday, April 20: L1 - Organisation, Introduction, Applications, Encodings, IPASIR [AI+DS]
- Monday, April 27: L2 - Tractable Subclasses, Encodings [AI]
- Monday, May 4: L3 - Elementary SAT Solving Algorithms (SLS, Resolution, Saturation, DP, DPLL) [DS]
- Monday, May 11: L4 - Application Highlights I (until slide 13) [DS]
- Monday, May 18: L5 - Application Highlights II (from slide 14) [DS]
- Monday, June 1: L6 - Elementary SAT Solving Heuristics, Conflict-Driven Clause Learning [AI]
- Monday, June 8: L7 - Conflict-Driven Clause Learning [AI]
- Monday, June 15: L8 - Preprocessing [AI]
Exercises
- Tuesday, May 5: E1 - Getting Started, Release of Exercise Sheet 1 (Introduction, Encodings) [AI]
- Tuesday, May 19: E2 - Discussing Exercise Sheet 1 (Introduction, Encodings), Release of Exercise Sheet 2 (Applications, Local search) [DS]
- Tuesday, June 2: E3 - Discussing Exercise Sheet 2 (Applications, Local Search), Release of Exercise Sheet 3 (Resolution, CDCL, SDVSTP) [AI]
- Tuesday, June 16: E4 - Discussing Exercise Sheet 3 (CDCL, MC-DPLL, SDVSTP), Release of Exercise Sheet 4 (Preprocessing, SDVSTPP) [NRL]
Competition Results
Code