SAT Solving Lecture Summer Semester 2025
Organization
- Mode: lecture will again not be recorded nor zoomed this year
- Credits: 6 ECTS
- Dependencies: none
- Responsible: Prof. Dr. Armin Biere
Goals
Introduction into advanced data structures and algorithms for SAT Solving.
Exercises
There will be four exercises; in each, we build parts of a SAT solver. You may write your SAT solver in your preferred language, and we will provide C++ templates and solutions.
Participation in the exercises is mandatory (Studienleistung).
ILIAS
The course will be similar to the course taught last year in 2024 as well as its predecessors at UFR and at JKU for which you find additional resources here:
Slides are updated and available on our NextCloud reachable from
which also contain additional material including recordings.
Course Outline
Copied from summer semester 2023 (might be slightly outdated)
- Lecture 01 Introduction, hands-on encoding into SAT: graph coloring, Sudoku, Schur, Pythagorean Triples
- Lecture 01a Terminology, motivate the use of SAT
- Lecture 02 DP, resolution, correctness and completeness of resolution
- Lecture 03 Unit resolution, DPLL, correctness of DPLL, shannon expansion, BCP implementation
- Lecture 04 Decision heuristics: static, dynamic, Cuts, Horn, DLIS, look-ahead heuristics, NNF
- Lecture 05 NNF to CNF, detecting sharing, Tseitin transformation and optimizations, bit-blasting, AIGs
- Lecture 06 Counting as optimization for DPLL, bit-stuffing, complexity of AIGs, logical constraints: fixed points, at-most-one
- Lecture 07 BDD based encoding of cardinality constraints, backjumping, implication graph as hyper graph, conflict driven backtracking/learning
- Lecture 08 Unique implication point, local and recursive clause minimization, poison, butterfly effect in benchmarking
- Lecture 09 Talk: Large-Scale SAT Solving by Dominik Schreiber
- Lecture 10 VSIDS, EVISIDS, NVISIDS, VMTF
- Lecture 11 Reduce, restarts, phase saving, target phases, watches
- Lecture 12 Overview of SAT-related fields, master theses topics
- Lecture 13 Variable Elimination, Bounded Variable Addition, Fast (Self) Subsumption, Vivification/Distillation, Autarkies
- Lecture 14 Stålmarck’s method, recursive learning, blocked clauses, proofs
Supplementary Material
- check-solver.py: a Python script that checks the sanity of your SAT solver
- SATRacer: educational tool that visualizes the implication graph in a CDCL SAT solver
- Debugging SAT Solvers: SAT solver debugging tools
- Blocked Literals: A brief explanation of blocked literals