| CARVIEW |
Select Language
HTTP/2 301
server: GitHub.com
content-type: text/html
location: https://satlecture.github.io/kit2024/
x-github-request-id: 734D:2E380F:42EA4:4C196:6967F966
accept-ranges: bytes
age: 0
date: Wed, 14 Jan 2026 20:15:34 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210063-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1768421735.623775,VS0,VE201
vary: Accept-Encoding
x-fastly-request-id: 0621478e3bc3be2bc57d26d7e0538789e73a5f53
content-length: 162
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Tue, 22 Apr 2025 07:56:41 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"68074bb9-1aad"
expires: Wed, 14 Jan 2026 20:25:34 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 5FF3:3663CF:400F9:49436:6967F966
accept-ranges: bytes
age: 0
date: Wed, 14 Jan 2026 20:15:35 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210063-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1768421735.838242,VS0,VE220
vary: Accept-Encoding
x-fastly-request-id: 76e8415a1541eba35388b0a9f917bd527788eb1b
content-length: 2569
Lecture: Practical SAT Solving | kit2024
kit2024
Lecture: Practical SAT Solving
Summer Term 2024, Computer Science, Karlsruhe Institute of Technology (KIT)
Slides
- Monday, April 15: Organisation, Introduction, Applications, Encodings, IPASIR
- Monday, April 22: Tractable Subclasses, Tseitin Encoding, Cardinality Constraints, Finite Domain Encodings
- Monday, April 29: Local Search, Resolution, DP Algorithm, DPLL Algorithm
- Monday, May 6: Branching Heuristics, Restart Strategies, Backtracking, Clause Learning
- Monday, May 13: Parallel SAT Solving 1: Puzzle nerds analogy, Search space partitioning, Portfolios, Clause sharing, Massively parallel basics (slides 1-25)
- Monday, May 27: Modern SAT Solving 2: Efficient Unit Propagation, Clause Forgetting, VSIDS, Community Structure, Preprocessing
- Monday, June 3: Preprocessing: Subsumption, BVE, BCE, Gates
- Monday, June 10: Parallel SAT Solving 2: Mallob(Sat) deep dive and insights on distributed SAT solving (slides 25-36 and 49)
- Monday, June 17: MaxSat
- Tuesday, June 18: Planning
- Monday, July 1: Application highlights
- Monday, July 8: Propagation-based Redundancy and Proofs
- Monday, July 15: Proof Pragmatics and Parallel Proofs (until slide 17; to be continued July 22)
- Monday, July 22: SMT Solving
Exercises
- Tuesday, April 23: Assignment 1 (Coloring and Sudoku Competitions, Pythagorean Triples, Tseitin Encoding)
- Tuesday, May 7: Assignment 2 (Tetris and Local Search Competitions, Resolution, Hidden Horn)
- Tuesday, June 4: Assignment 3 (Hidoku Competition, CDCL, BVE, BCE)
- Tuesday, June 18: Assignment 4 (Multiplier Encodings, Perfect Hashing Competition)
- Tuesday, July 9: Assignment 5 (Application-specific Analysis, Planning via MaxSAT, Distributed SAT, Miter Challenge)
- Tuesday, July 23: Discussion of Assignment 5
Slides and Code used in the Exercises
- Cumulative Slideset
- Code Example: SLUR Satisfier
- Code Example: Trail Class with Propagate and Backtracking
Repository
This page is generated from our repository on GitHub
Code
The code/src/util directory contains a CNF file parser that is called when instantiating the class in CNFFormula.h, which can also read packed CNF files.
The parser uses `libarchive’ (for unpacking CNF files), so to use it you need to install libarchive like this:
- For Ubuntu:
apt install libarchive-dev - For macOS:
brew install libarchive
To build the programs from the lecture and exercises, invoke our build script CMakeLists.txt as follows:
cmake -S code -B code/build
cmake --build code/build
This site is open source. Improve this page.