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.
 Open document (Hedgedoc) at https://doc.anagora.org/smt
 Video call (Jitsi) at https://meet.jit.si/smt