Definition
Plain language
Software that finds an assignment of true/false values to variables that makes a set of logical constraints all hold.
As stated in the literature
A program implementing decision procedures for SAT or SMT problems, finding satisfying assignments to logical or arithmetic constraints.
Also called: SAT solver
Why it matters: Solvers are how computers turn vague "find a valid configuration" problems into routine queries, underpinning verification, planning, and many AI-meets-formal-methods workflows.
For example, given the rules of a Sudoku puzzle as constraints, a SAT solver can return a complete solution — or prove no solution exists — in seconds.
Heard on the show
“… They take a sub-one-billion model, hook the auxiliary up to Z3 — the standard satisfiability solver, the kind of program that takes a stack of logical constraints and finds an assignment that …”Episode 040 — Two Frozen Models Learn to Whisper: Coupling Through Hidden States