# SMT

# SAT solvers

## Cons

Require input problem to be a propositional logic formula in conjunctive normal form (CNF). This is not a natural way to express most problems that require SAT

Computing CNF formulas is often bad and hard so SAT solvers aren't really at the right "level" for use by the working programmer

Look up `cardinality constraints CNF` on google scholar - reveals lots of problems and tradeoffs that can be made

## Why SMT over SAT?

SMT solvers allow more freedom in the expression of input problems - support integers, fixed width floats, arrays and potentially other datatypes, as well as common operations on those types, without requiring a specific normal form!

API that allows for the manipulation of the input formula exposed by the solver, unlike strict

## How do they work?

### Bit blasting

Directly convert input formula into an equivalent Boolean formula in CNF

Limited to formulas where every data type has a finite set of values

Need a SAT solver as a backend, any improvement to SAT translates directly to an improvement to an SMT solver - so this is just additional tooling around a SAT solver to make it much easier to use.

### CDCL(T)

Definition: conflict driven cause learning - the algorithm employed by most modern SAT solvers.