I’ve recently been learning about SMT/SAT solvers. Here’s a brief summary.
Concepts
SMT can be viewed as a generalization of SAT. SAT is essentially limited to determining whether a Boolean expression can be satisfied—i.e., whether there exists an assignment of variables that makes the expression evaluate to true (SAT). If no such assignment exists, the expression is unsatisfiable (UNSAT).
Software Verification
This section primarily references the chapter of the same name in Handbook of Satisfiability.
Programs can generally be abstracted as State + State Transitions. States are mappings (e.g., registers and memory), and transitions represent relationships between two states.
Given a program’s current state $s$ and a desired property $p$, we feed $s$ and $\neg p$ to the SMT solver. If the result is UNSAT, the property $p$ holds for state $s$. If SAT, there exists a scenario where property $p$ is violated—and the solver can typically provide a concrete counterexample.
Under the hood, SMT ultimately relies on SAT. In computing, integers are represented as bit vectors (e.g., a 32-bit integer is 32 bits), and their operations can be expressed as bitwise logical arithmetic—essentially the same principle as implementing binary operations with AND/OR/NOT gates in digital circuits. Once states are converted to Boolean values, SMT hands them off to the underlying SAT solver.
Soundness
SMT solvers can sometimes produce incorrect answers, which has spawned a body of work on SMT fuzzing. Some research uses multiple SMT solvers on the same problem and compares their results for inconsistencies.
For more detailed references, see my notes.
To address the soundness issue, researchers have proposed various solutions: designing formally verified SAT/SMT solvers, making proofs independently verifiable, or combining both approaches. Related tools and papers can also be found in the notes linked above.