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
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
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.
Definition: conflict driven cause learning - the algorithm employed by most modern SAT solvers.