- SAT
- Given a Boolean formula can we replace variables with T/F such that formula evals to T?
- SAT if yes, UNSAT if no
- valid if yes inputs (i.e., is valid iff is UNSAT)
- SMT
- SAT modulo theories
- Theories: what kinds of thins we can write down and combine w first-order logic to be able to give to SAT solver
- first-order logic: connectives, parens, no quantifiers, constants, n-ary functions and predicates, no variables
- used in one place is the same as another place. No reassignment.
- Universe: non-empty set of values
- Interpretation:
- maps symbol to element of universe
- maps function symbol to function from tuple of universe elems to universe elem
- maps predicate symbol to true/false
- Theories
- Equality with uninterpreted functions
- is interpreted, nothing else is
- Axioms: have some equality axioms
- Fixed-width bitvectors
- LIA