Satisfiability Modulo Theories
Determine if a Logical Formula can be made true under background theories by assigning numerical values to its variables.
- extension of Boolean Satisfiability Problem by adding mathematical theories
- background theories include
- linear integer arithmetic: addition, subtraction inequalities
- linear real arithmetic: real-number variables and linear constraints
- bit-vectors: fixed-with binary representations
- arrays: modeling indexed memory or data structures
- uninterpreted functions: abstract functions without defined behaviour
- strings, floating point, sets