This is a curated collection of resources for the Boolean Satisfiability Problem (SAT), one of the most famous problems in computer science. It also cover related problems and software like Satisfiability Modulo Theory (SMT) solvers and Constraint Satisfaction Problem (CSP) solvers
- Tutorials
- Books
- SAT Solvers
- Other Solvers
- Libraries
- Handbook of SAT
- Research
- Courses and Lectures
- Competitions
- Other Resources
- Conflict Driven Clause Learning - Basic interactive tutorial on a SAT, DPLL, and CDCL
- Tutorial introduction to Z3 in Python - Short intro to using the z3 python bindings
- Modern SAT solvers: fast, neat and underused (part 1 of N) - Popular blog series introducing SAT
- SAT/SMT school from SAT association - Links to many of the old summer schools from the SAT association with introductory material
- SAT tutorials from SAT association - Links to academic books and tutorials on SAT
- LogicNG tutorial - Uses the Java LogicNG library to solve SAT problems, includes a general introduction to SAT.
- Simons Workshop SAT bootcamp - Workshop from 2021 which has introductory lectures to modern SAT solving
- Theoretical Foundations of Applied SAT Solving - Workshop from 2014 with many useful videos.
- MiniZinc tutorial - An intro to constraint satisfaction taking you through solving combinatorial optimisation problems
- The Calculus of Computations - covers the logic theory background
- Decision Procedures: An Algorithmic Point of View - Great, practical book focusing on the algorithms of SAT and SMT. Strongly recommended.
- SAT/SMT by Example - free pdf available online! - An excellent problem-based introduction to SAT and SMT.
- The Art of Computer Programming - Satisfiability - Preprint available online - Donald Knuth's famous book's section on SAT.
SAT has a nice tradition of making solver public and open source. As Yogi Berra said "You can observe a lot by watchin". Three very important whose source code is informative to read are GRASP, Chaff and MiniSAT. These are important or (historical) state of the art solvers.
- WalkSAT (1994) - local search - code | project page
- GRASP (1996) - GRASP pioneered the modern approach of CDCL. - code | paper
- Chaff (2001) - Chaff introduced important data structures and heuristics. - code | paper
- MiniSAT(2003) - Famous for being good, short (2k LOC), and introducing incremental SAT, MiniSAT is still widely used. Clear and worth reading! code | paper
- CryptoMiniSAT (2009) - Uses XOR primitive - code | paper
- Glucose (2009) - Introduced different heuristics for SAT and UNSAT - code | paper
- Lingeling (2010) - website
- PicoSAT (2010) - website
- Slime - - code
- MergeSAT (2021) - code
- CaDiCaL (2024) - code
- Kissat (2020) - - code
Other solvers of interest:
- Satch - expository solver by Armin Biere
- gopher - solver written in Go
- varisat - solver written in Rust
- The SAT Museum - paper
- Assessing Progress in SAT Solvers Through the Lens of Incremental SAT - paper
- SAT: Disruption, Demise & Resurgence - paper
- A case for simple SAT solvers - paper
- Anatomy and empirical evaluation of modern SAT solvers paper
- DPLL - Davis–Putnam–Logemann–Loveland (DPLL) algorithm is the historic basis for modern solvers - wiki
- CDCL - Conflict-driven Clause learning the contemporary extension of DPLL - wiki
- Implication graph - a key construction used to find conflict clauses - wiki
- Unit propagation - a.k.a. Boolean constraint propagation, a rule for simplifying formulas wiki - see also "An Efficient Algorithm for Unit Propagation"
- backjumping - Efficient backtracking is one of the main differences between DPLL and CDCL - wiki
- SAT heuristics - Heuristics are essential to modern SAT solvers. wiki
MaxSAT is the problem of the finding the maximum number of clauses which can be satisfied for a particular formula
Minimally Unsatisfiable Subformulas are like duals MaxSAT, they ask for the minimal set of assignments which will show a formula is unsatisfiable.
The #SAT is the problem of counting all the assignments which satisfy a Boolean formula.
Solvers include:
- ApproxMCv6 (by creators of CryptoMiniSAT)
- SharpSAT (sota circa 2011)
SMT solvers are generally built on top of SAT solvers and solver more complex problems.
CSP solvers differ from SAT solvers but the communities overlap, and techniques from CSP have proven very important in SAT e.g. Boolean Constraint Propagation.
- Constraint Satisfaction Problems (CSP)
- CSP modelling
- (Constraint Propagation - Models, Techniques, Implementation) - intro to CSP theory
CSP solvers include:
- GeCode - C++ based - good documentation and overview of the code
- Sugar - Solving by reduction to SAT -
- Picat - logic programming-based
- Choco - Java-based
- OptaPlanner - Java-based
solver
- Pseudo-boolean Constraints
- Integer Programming (IP/ILP/MILP)
- Branch-and-bound algorithms: A survey of recent advances in searching, branching, and pruning
Solvers include:
Besides solvers, there are many other pieces of helpful software for solving SAT and related problems.
- PySAT (Python) - wrapper library website
- Sat4j (Java) - modelling and wrapper for Java - website
- ORTools (Python) - general purpose modelling library for optimisation problems but very good as CSP - website
- DRAT-Trim - verifier of proofs of unsatisfiability (UNSAT)
The handbook of SAT is an excellent and comprehensive resources.
- Handbook of Satisfiability (comprehensive and very useful)
- CH 1 A History of Satisfiability
- CH 2 CNF Encodings
- CH 3 Complete Algorithms
- CH 4 Conflict-Driven Clause Learning SAT Solvers
- CH 5 Look-Ahead Based SAT Solvers (1st Ed.)
- CH 6 Incomplete Algorithms
- CH 7 Proof Complexity and SAT Solving
- CH 8 Fundaments of Branching Heuristics
- CH 9 Preprocessing in SAT Solving (2nd Ed.)
- CH 10 Random Satisfiability (2nd Ed.)
- CH 14 Bound Model Checking (1st Ed.)
- CH 15 Proofs of Unsatisfiability (2nd Ed.)
- CH 23 MaxSAT, Hard and Soft Constraints (2nd Ed.)
- CH 19 Planning and SAT
- CH -2 SMT (1st Ed.)
Overviews and reviews.
Lazy data structures have proven to be very important in SAT solvers.
- M. Iser and T. Balyo, ‘Unit Propagation with Stable Watches’, 2021. link
- I. P. Gent, ‘Optimal Implementation of Watched Literals and More General Techniques’, Journal of Artificial Intelligence Research, vol. 48, pp. 231–252, Oct. 2013, doi: 10.1613/jair.4016. link
Heuristics around choosing variables which variables and which assignments to make are an extremely improtant part of SAT Solvers Important heuristics include:
- Variable State Independent Decaying Sum (VSAID) introduced in Chaff
- Clause-move-to-front introduced by HAIFASAT
SAT raises some interesting questions because even though it is the canonical NP-complete problem, practical problems can often be solved in close to linear time. Relating Proof Complexity Measures and Practical Hardness of SAT
SAT is tricky to parallelise, but the cube-and-conquer method has been very popular.
- Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads paper
Machine learning is a related branch of AI and theorem proving. The overlap is mostly in the direction of applying machine learning methods to help SAT solvers e.g.
- SATzilla: Portfolio-based Algorithm Selection for SAT. Journal of Artificial Intelligence Research 32 (2008) 565-606. paper
- Constraint Satisfaction @Monash via Coursera
- Bug Catching: Automated Program Verification
- SAT Competition https://satcompetition.github.io/
- MiniZinc Competition https://www.minizinc.org/challenge/2023/results/
- LP/CP programming contest https://lpcp-contest.github.io/
- MaxSAT competition https://maxsat-evaluations.github.io/
- Model count competition https://mccompetition.org/
- QBF competition (more irregular) https://qbf23.pages.sai.jku.at/gallery/
- Other research competitions https://www.hsu-hh.de/logistik/research/challenges
- DIMACS file format - https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html
- SAT association - https://www.satassociation.org/
- Simons Institute Workshop (2021, 2023) https://simons.berkeley.edu/workshops/satisfiability-theory-practice-beyond