SMT

src - maybe?

SAT solvers

Cons

Why SMT over SAT?

How do they work?

Bit blasting

CDCL(T)