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.
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]
- Monday, June 22: L9 - Redundancy Notions and Proof Systems [AI]
- Monday, June 29 and July 6: L10 - Parallel SAT Solving [DS]
- Monday, July 13: L11 - Proof Pragmatics and Parallel Proof Tech [DS]
- 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) and 1 (Graph Coloring competition), Release of Exercise Sheet 3 (Resolution, CDCL, SDVSTP) [AI]
- Tuesday, June 16: E4 - Discussing Exercise Sheet 3 (CDCL, MC-DPLL) and 2 (Local Search competition), Release of Exercise Sheet 4 (Preprocessing, SDVSTPP) [NRL]
- Tuesday, June 30: E5 - Discussing Exercise Sheet 4 (Preprocessing) and 3 (SDVSTP competition), Release of Exercise Sheet 5 (Parallel SAT) [NRL+DS]
- Tuesday, July 14: E6 - Discussing Exercise Sheet 5 (Parallel SAT)
and 4 (SDVSTPP competition), Release of Exercise Sheet 6 (Proofs, SMT) [DS] - Tuesday, July 28: E7 - Discussing Exercise Sheet 6 (Proofs, SMT) and 4/5 (SDVSTPP and Clause sharing competition), Exam questions
- E1 Graph-Coloring [NRL]
- E2 Local Search [NRL]
- E3 SDVSTP [NRL] (updated 03.07.2026)
- Tuesday, May 5: E0 - Pigeon Hole Principle, Cardinality Contraint Encodings, Incremental SAT Solving [AI]