SAT Solving Lecture Summer Semester 2024
Organization
- Mode: lecture will not be recorded this year
- Lecture & Exercise Class: Mondays 10am-12am, Thursdays 10am-12am
- Room: R 03 026 Seminarraum (G.-Köhler-Allee 051)
- Credits: 6 ECTS
- Dependencies: none
- Responsible: Prof. Dr. Armin Biere
- Support: Bernhard Gstrein
Projects
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.
ILIAS
The course will be similar to the course taught last year in 2023 as well as its predecessors from JKU for which you find more resources here:
Slides are updated and available on our NextCloud reachable from
which also contain additional material including recordings.
Course Outline
- 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