SAT and SMT -- Brief ☧
Deep version -> | Back to Arc Consistency ->
Q: Let's start with something familiar. You're planning a dinner party.
You have 5 guests and 5 seats. Guest A can't sit next to Guest B. Guest C
must be near the head of the table. Guest D refuses to sit at the end.
Can you seat everyone so all the rules are satisfied?
A: That's the core question behind satisfiability: given a bunch
of variables (who sits where) and a bunch of constraints (the seating
rules), is there an assignment that makes ALL constraints true at the
same time?
Q: OK. And "SAT" is this idea made precise?
A: Yes. SAT stands for the Boolean Satisfiability Problem.
You write your constraints as a formula using true/false variables, AND,
OR, and NOT. Then you ask: is there a way to set all the variables so the
whole formula comes out true?
(A OR B) AND (NOT A OR C) AND (NOT B OR NOT C) Try A=true, B=false, C=true: (true OR false)=true AND (false OR true)=true AND (true OR false)=true -> ALL true. SATISFIABLE! We found an assignment that works.Q: But real problems aren't just true/false. What if I need actual
numbers or more complex data?
A: That's where SMT comes in -- Satisfiability Modulo Theories.
It extends SAT with richer types: integers, arrays, bitvectors,
strings. Instead of just asking "true or false?" you can ask "what
number? which element? which bit pattern?" SMT solvers like Z3 combine
a SAT engine with specialized theory solvers for each data type.
Q: How does this connect to the domain-narrowing approach we've
been learning about?
A: They share the same key insight. When a domain narrows to a single
value, that's a forced assignment -- exactly like what SAT solvers call
unit propagation:
SAT unit propagation: (A) forces A=true Our domain narrowing: domain=000001 forces variable=0 Both mean: "only one choice left -- take it"The difference is in scope. SAT works with individual boolean variables
(true/false). Our FPGA works with bitmask domains that can encode
up to 262,144 values in a single variable -- much richer than a single bit.
SAT vs Our System
Understanding the relationship between SAT/SMT and our domain-narrowing approach
helps clarify why our hardware is so much faster for certain problems, and why
it cannot handle everything a general-purpose solver can.
| SAT Solver (Z3) | Our FPGA | |
|---|---|---|
| Variables | Boolean (true/false) | Bitmask domains (up to 262K values) |
| Constraints | Clauses (OR of literals) | Domain intersection (AND) |
| Search | DPLL/CDCL with backtracking | Parallel branch evaluation |
| Strength | General, any Boolean formula | Fast, domain-specific |
| Weakness | Sequential, one variable at a time | Limited constraint types |
The fundamental difference is granularity. A SAT solver works with individual
Boolean variables -- each one is either true or false. To encode "person X can
sit in seats 1-5," you need five separate Boolean variables (one per seat).
Our FPGA, by contrast, represents that same information as a single 5-bit
bitmask: 0b11111. Narrowing that domain is a single AND instruction, whereas
the SAT solver must reason about five variables and their interactions through
clause propagation. This is why our approach is dramatically faster for
finite-domain problems -- but a SAT/SMT solver can handle arbitrary Boolean
formulas, arithmetic, and theory combinations that our bitmask hardware cannot
express.
Soli Deo Gloria