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