Lecture: Practical SAT Solving
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.
Lectures
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, Tseitin Encoding, Cardinality Constraints, Finite Domain Encodings [MI]
- Monday, May 5: L3 - Local Search, Resolution, DP Algorithm, DPLL Algorithm [DS]
- Monday, May 12: L4 - Modern SAT Solving 1: Branching Heuristics, Restart Strategies, Backtracking, Clause Learning / CDCL [MI]
- Monday, May 19: L5 - Efficient Unit Propagation, Clause Forgetting, VSIDS, Community Structure, Algorithm Selection [MI]
- Monday, May 26: L6 - Preprocessing: Subsumption, BVE, BCE, Gates [MI]
- Monday, June 2: L7 - Propagation-based Redundancy and Proof Systems [MI]
- Monday, June 16: L8 - Parallel SAT Solving: Search space partitioning, Portfolios, Clause sharing, massively parallel basics [DS]
- Monday, June 23: L9 - Frontiers of distributed SAT solving [DS]
- Monday, June 30: L10 - Pragmatics of proofs of unsatisfiability, parallel proof & distributed technology [DS]
- Monday, July 7: L11 - Applications 1: Planning, model checking [DS]
- Monday, July 14: L12 - Applications 2: Selected highlights [DS]
- Monday, July 21: L13 - Satisfiability Modulo Theories (SMT) solving [DS]
- Monday, July 28: L14 - Maximum Satisfiability (MaxSAT) solving [MI]
Exercises
This is our tentative plan for exercises:
- Tuesday, May 6: E0 - getting started, announcement of assignment 1 (A1) (introduction, algorithms, encodings)
- Tuesday, May 20: E1 - discussion of A1, announcement of A2 (modern SAT solving 1+2)
- Tuesday, June 3: E2 - discussion of A2, announcement of A3 (preprocessing, PR, proofs)
- Tuesday, June 17: E3 - discussion of A3, announcement of A4 (parallel SAT)
- Tuesday, July 1: E4 - discussion of A4, announcement of A5 (distributed SAT, proof pragmatics)
- Tuesday, July 15: E5 - discussion of A5, announcement of A6 (applications)
- Tuesday, July 29: E6 - discussion of A6, exam questions
Code