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
- Introductions and Tutorials
- SAT Solvers
- Solvers for related problems
- Other Software and Libraries
- Research
- 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
- MiniZinc tutorial - An intro to constraint satisfaction taking you through solving combinatorial optimisation problems
- LogicNG tutorial - Uses the Java LogicNG library to solve SAT problems, includes a general introduction to SAT.
- Modern SAT solvers: fast, neat and underused (part 1 of N) - Popular blog series introducing SAT
- The Silent (R)evolution of SAT - Academic Survey from 2023
- Boolean Satisfiability: From Theoretical Hardness to Practical Success - An older academic survey from 2007
- Satisfiability Solvers - overview of whole SAT solvers area from Knowledge Representation Handbook 2008
- A Peek Inside SAT Solvers - Jon Smock - Accessible 30 minute overview
- 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.
- Constraint Satisfaction @Monash via Coursera
- 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
- Course from Armin Biere for undergrads - 2023
- Bug Catching: Automated Program Verification - 2017
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 espcially version 1.12! code | paper
- CryptoMiniSAT (2009) - Uses XOR primitive - code | paper
- Glucose (2009) - Introduced different heuristics for SAT and UNSAT - code | paper
- PicoSAT (2010) - website
- Lingeling (2010) - version
Lingeling aqwwon several tracks in 2013 website | 2013 paper - MapleSAT (2016) - 2016 winner used machine learning based branching and restarts policies website | paper
- CaDiCaL (2019) - paper | code
- Kissat (2020) - - code
- SBVA-CaDiCaL (2023) - overall winner in SAT competition. Develops heuristic for structured bounded variable addition (SBVA), a preprocessing technique which automatically reencodes formulas by introducing new variables to eliminating clauses which frequently results in reducing formula size. code paper
- Slime (2021) - code
- MergeSAT (2021) - code
- Satch - expository solver by Armin Biere
- gopher - solver written in Go
- varisat - solver written in Rust
- 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
- backjumping - Efficient backtracking is one of the main differences between DPLL and CDCL - wiki
- SAT heuristics - Heuristics are essential to modern SAT solvers. wiki
- 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
- The Quest for Efficient Boolean Satisfiability Solvers - This is a great place to start learning about how to write SAT solvers
- Improving SAT Solvers Using State-of-the-Art Techniques - Very clear master's thesis describing the state of the art up until 2010
- good theoretical CS stackexchange post
- Anatomy and empirical evaluation of modern SAT solvers 2011 paper
- notes on Implementation from bug catcher course
There many theoretical problems which are closely related to SAT. Solvers for the following adjacent problems are worth knowing about:
- MaxSAT, #SAT and QBF are all progressively harder generalisations of SAT
- SMT extends the SAT problem with soluble theories.
- CSP and Integer programming are alternate approaches to solving NP-hard problems
MaxSAT is the problem of the finding the maximum number of clauses which can be satisfied for a particular formula. MaxSAT can be seen as an optimisation version of the SAT problem. Minimally Unsatisfiable Subformulas (MUSs) are like duals MaxSAT, they ask for the minimal set of assignments which will show a formula is unsatisfiable. - wiki
Solvers include:
The #SAT is the problem of counting all the assignments which satisfy a Boolean formula. - wiki
Solvers include:
- ApproxMCv6 (by creators of CryptoMiniSAT)
- SharpSAT (sota circa 2011)
Quantified boolean formula (QBF) is generalisation boolean formula which allows existential and universal quanitifiers. The SAT problem for QBF formula (QSAT) is the canonical PSPACE problem. In addition to CDCL, a standard QBF solver algorithm is CounterExample-Guided Abstraction Refinement (CEGAR) - wiki
Solvers include:
Satisfiable Modulo Theory (SMT) solvers are generally built on top of SAT solvers and make use of expressive theories such as bit-vectors and or uninterpreted functions. SMT solvers generally use an extension of the DPLL algorithm called DPLL(T) (T is for Theory) | wiki
Solvers include:
Constraint Satisfaction 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. wiki | recent book on CSP modelling | recent book on 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
0-1 integer programming was the first in Karp's list of 21 NP-complete problems which was reducible to SAT. Pseudo-boolean constraints are another term for 0-1 integer linear programming (ILP). While ILP solvers also use exhaustive search (e.g. branch and bound) they make heavy use of relaxations of the problem. - wiki | IP solvers from the SAT perspective | Academic survey of Branch-and-bound algorithms
Solvers include:
Besides solvers, there are many other pieces of helpful software for solving SAT and related problems.
Many complex problems can be solved by compiling the problem into a SAT encoding. Examples of domain problems which can be solved by reduction include planning problems (SATPLAN), automated theorem proving (via SMT), and formal verification (by bounded model checking).
- 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)
There is a vast literature on SAT.
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
- more info
- Successful SAT encoding techniques paper
- Arithmetic operations paper
- practical reduction of linear constraints to SAT is described here: Encoding Linear Constraints into SAT (paper)
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
- Karp's 21 NP-complete problems (1971) paper
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
- Machine Learning for Automated Theorem Proving - A survey of recent work paper
- DIMACS file format - website
- SAT association - website
- Simons Institute Workshops (2021, 2023) website
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 19 Planning and SAT
- CH 23 MaxSAT, Hard and Soft Constraints (2nd Ed.)
- CH -2 SMT (1st Ed.)
- 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 Competition link
- MiniZinc Competition link
- LP/CP programming contest link
- MaxSAT competition link
- Model count competition link
- QBF competition (more irregular) link
- Other research competitions link
- ‘SATLIB - Benchmark Problems’
- Original 1992 DIMACS workshop problems ftp site
- Historic SAT benchmark database website | paper