Summer Term 2025 • GitHub repository • Web page • Karlsruhe Institute of Technology (KIT)
This lecture with exercises is offered by Markus Iser (ITI Sanders) and Dominik Schreiber (KASTEL-VADS SAtRes).
Niccolò Rigi-Luperti (SAtRes) acts as a co-manager of exercises.
The lecture provides a friendly and practical overview of the subject of propositional satisfiability (SAT) solving, including 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 Tuesday, April 22.
We tentatively offer the following exam dates (last updated July 23):
Thursday, July 31- Monday, August 25
- Wednesday, September 24
If neither of these options suit you, please let us know!
The below lecture plan is tentative and subject to changes. We try to link each slide set here shortly before the lecture takes place. See also the page from last year.
- Tuesday, April 22: L1 - Organisation, Introduction, Applications, Encodings, IPASIR [MI+DS]
- Monday, April 28: L2 - Tractable Subclasses, Elementary Encoding Methods [MI]
- Monday, May 5: L3 - Local Search, Resolution, DP Algorithm, DPLL Algorithm [DS]
- Monday, May 12: L4 - Branching Heuristics, Restart Strategies, Clause Learning, Backtracking [MI]
- Monday, May 19: L5 - Efficient Unit Propagation, Clause Forgetting, Community Structure, VSIDS [MI]
- Monday, May 26: L6 - Preprocessing and Propagation-based Redundancy [MI]
- Monday, June 2: L7 - Redundancy and Proof Systems [MI]
- Monday, June 16: L8.1 - Parallel SAT Solving: Search space partitioning, Portfolios, Clause sharing, massively parallel basics [DS]
- Monday, June 23: L8.2 - Frontiers of distributed SAT solving [DS]
- Monday, June 30: L9.1 - Pragmatics of proofs of unsatisfiability [DS]
- Monday, July 7: L9.2 - Parallel proof & distributed technology ; L10 - Applications 1: Automated planning [DS]
- Monday, July 14: L11 - Selected application highlights [DS]
- Monday, July 21: L12 - Satisfiability Modulo Theories (SMT) solving [DS]
- Monday, July 28: L13 - Maximum Satisfiability (MaxSAT) solving [MI]
This is our tentative plan for exercises:
- Tuesday, May 6: E0 - getting started, announcement of assignment 1 (A1) (introduction, algorithms, encodings) [DS]
- Tuesday, May 20: E1 - discussion of A1, announcement of A2 (classic and modern SAT solving) [MI]
- Tuesday, June 3: E2 - discussion of A2, announcement of A3 (preprocessing, proofs) [MI]
- Tuesday, June 17: E3 - discussion of A3, announcement of A4 (parallel SAT) [MI]
- Tuesday, July 1: E4 - discussion of A4, announcement of A5 (proof pragmatics, planning) [DS]
- Tuesday, July 15: E5 - discussion of A5, announcement of A6 (applications, SMT) [DS]
- Tuesday, July 29: E6 - discussion of A6, exam questions
- Tuesday, April 22: Essential Variables