satisfiability modulo theories (smt)
**Satisfiability Modulo Theories (SMT)** is a decision problem for **determining the satisfiability of logical formulas with respect to combinations of background theories** — extending boolean satisfiability (SAT) with theories like arithmetic, arrays, bit-vectors, and uninterpreted functions, enabling powerful automated reasoning for program verification, test generation, and constraint solving.
**What Is SMT?**
- **SAT**: Determine if boolean formula can be satisfied.
- Example: (x ∨ y) ∧ (¬x ∨ z) — can we assign true/false to make this true?
- **SMT**: SAT + Theories — formulas involve not just booleans but integers, reals, arrays, etc.
- Example: (x + y > 10) ∧ (x < 5) — can we find integer values satisfying this?
- **Theories**: Background domains with specific semantics.
- **Linear Arithmetic**: x + 2y ≤ 10
- **Bit-Vectors**: x[7:0] & 0xFF == 0x42
- **Arrays**: select(store(a, i, v), i) == v
- **Uninterpreted Functions**: f(f(x)) == x
**Why SMT?**
- **Expressive**: Can express complex constraints beyond boolean logic.
- **Automated**: SMT solvers automatically find solutions or prove unsatisfiability.
- **Efficient**: Modern SMT solvers are highly optimized.
- **Versatile**: Used in verification, test generation, program synthesis, security analysis.
**How SMT Solvers Work**
- **DPLL(T) Architecture**: Combine SAT solver with theory solvers.
1. **SAT Solver**: Find boolean assignment satisfying formula structure.
2. **Theory Solver**: Check if assignment is consistent with theory constraints.
3. **Conflict**: If inconsistent, SAT solver learns conflict clause and tries again.
4. **Iterate**: Repeat until consistent assignment found or proven unsatisfiable.
**Example: SMT Problem**
```
Formula: (x + y == 10) ∧ (x > 5) ∧ (y < 3)
SMT solver reasoning:
- x + y == 10
- x > 5 → x >= 6
- y < 3 → y <= 2
- If x >= 6 and y <= 2, then x + y <= 6 + 2 = 8
- But we need x + y == 10
- Contradiction!
- Result: UNSAT (unsatisfiable)
Modified formula: (x + y == 10) ∧ (x > 5) ∧ (y < 5)
- x > 5 → x >= 6
- y < 5 → y <= 4
- x + y == 10 with x = 6, y = 4 ✓
- Result: SAT with model x=6, y=4
```
**SMT Theories**
- **QF_LIA**: Quantifier-Free Linear Integer Arithmetic
- Constraints: ax + by + c ≤ 0 (linear inequalities over integers)
- **QF_LRA**: Quantifier-Free Linear Real Arithmetic
- Constraints: ax + by + c ≤ 0 (linear inequalities over reals)
- **QF_BV**: Quantifier-Free Bit-Vectors
- Bit-level operations: &, |, ^, <<, >>, arithmetic on fixed-width integers
- **QF_A**: Quantifier-Free Arrays
- Array operations: select (read), store (write)
- **QF_UF**: Quantifier-Free Uninterpreted Functions
- Functions with no defined semantics — only equality matters
**Applications**
- **Symbolic Execution**: Solve path constraints to generate test inputs.
```python
# Path constraint: (x > 0) ∧ (x + y < 10) ∧ (y > 5)
# SMT solver finds: x=1, y=6
```
- **Program Verification**: Prove program properties.
```
# Verify: x >= 0 ∧ y >= 0 → x + y >= 0
# SMT solver: Valid (always true)
```
- **Bounded Model Checking**: Encode reachability as SMT formula.
- **Program Synthesis**: Find programs satisfying specifications.
- **Compiler Optimization**: Prove optimizations preserve semantics.
**SMT Solvers**
- **Z3**: Microsoft's SMT solver — widely used, supports many theories.
- **CVC4 / CVC5**: SMT solver from Stanford/Iowa — strong theory support.
- **Yices**: Fast SMT solver for QF_LIA, QF_LRA.
- **MathSAT**: SMT solver with optimization capabilities.
- **Boolector**: Specialized for bit-vector and array theories.
**Example: Using Z3**
```python
from z3 import *
# Variables
x = Int('x')
y = Int('y')
# Constraints
solver = Solver()
solver.add(x + y == 10)
solver.add(x > 5)
solver.add(y < 5)
# Check satisfiability
if solver.check() == sat:
model = solver.model()
print(f"SAT: x={model[x]}, y={model[y]}")
else:
print("UNSAT")
# Output: SAT: x=6, y=4
```
**SMT in Symbolic Execution**
```python
def test(x, y):
if x + y > 10:
if x > 5:
return "A"
return "B"
# Symbolic execution path: x + y > 10 ∧ x > 5
# SMT query: Is (x + y > 10) ∧ (x > 5) satisfiable?
# Z3 returns: SAT with x=6, y=5
# Test input: test(6, 5) → "A"
```
**SMT in Program Verification**
```c
// Verify: If x >= 0 and y >= 0, then x + y >= 0
// SMT formula: (x >= 0) ∧ (y >= 0) → (x + y >= 0)
// Equivalently: ¬((x >= 0) ∧ (y >= 0) ∧ (x + y < 0))
// SMT solver: UNSAT (no counterexample exists)
// Conclusion: Property is valid ✓
```
**Challenges**
- **Decidability**: Some theories are undecidable — solver may not terminate.
- **Scalability**: Complex formulas with many variables can be slow.
- **Theory Combination**: Combining multiple theories increases complexity.
- **Quantifiers**: Formulas with quantifiers (∀, ∃) are much harder.
**Optimization**
- **Incremental Solving**: Reuse solver state across related queries.
- **Simplification**: Simplify formulas before solving.
- **Theory-Specific Heuristics**: Exploit theory structure for efficiency.
**LLMs and SMT**
- **Formula Generation**: LLMs can translate natural language constraints to SMT formulas.
- **Result Interpretation**: LLMs can explain SMT solver results in natural language.
- **Debugging**: LLMs can help debug unsatisfiable formulas — identify conflicting constraints.
**Benefits**
- **Automation**: Automatically solves complex constraint problems.
- **Expressiveness**: Handles rich theories beyond boolean logic.
- **Efficiency**: Modern solvers are highly optimized.
- **Versatility**: Applicable to diverse problems — verification, testing, synthesis.
**Limitations**
- **Complexity**: Some problems are inherently hard — exponential worst case.
- **Undecidability**: Some theories don't guarantee termination.
- **Learning Curve**: Requires understanding of logic and theories.
SMT solving is a **foundational technology for automated reasoning** — it powers symbolic execution, program verification, test generation, and many other applications, providing automated decision procedures for complex logical formulas.