SAT Solving Lecture Summer Semester 2023
Organization
- Mode: lecture is streamed and recorded with Zoom
- Lecture & Exercise Class: Mondays 10am-12am, Thursdays 10am-12am
- Room: SR 01 016/18 Geb. 101
- Credits: 6 ECTS
- Dependencies: none
- Responsible: Prof. Dr. Armin Biere
- Support: Bernhard Gstrein
- Exercises: Bi-weekly meeting of the single exercise group every second Thursday.
Projects
- Four projects implementing different versions of SAT solvers.
- Template code available in our NextCloud (see ILIAS)
- Presentation of projects on: 25. May, 15. June, 3. July and 20. July.
- Solutions are due Mondays in those weeks through ILIAS
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 2022 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