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.

# 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

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

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

// 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.