SAT Solving Lecture Summer Semester 2023
- 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.
- 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
Introduction into advanced data structures and algorithms for SAT Solving.
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.
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.
- 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