Unification vs. SAT solver
SAT solvers solve the Boolean Satisfiability Problem. This is "the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE." 

An example is find an assignment of truth values to variables $a,b,c$ such that
$(a \lor b \lor c)\land (\lnot a \lor \lnot b \lor c)\land (a \lor \lnot b \lor \lnot c)\land (\lnot a \lor b \lor \lnot c)$ is true. A SAT solver could return a solution such as $a=true$, $b=true$, $c=true$.

SMT solvers solve a more general problem, namely Satisfiability Modulo Theories. This is "a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality".
These theories could include "the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on."

An example, given typed variables $x:int$ and $y:int$ and $f:int\to int$, asks whether the following is
$f(x+2) \neq f(y-1) \land x=(y- 4)$ satisfiable. 
An SMT solver would answer yes, with solution  $x=-2$, $y=2$, $f(0)=1$
and $f(1)=3$.

Unification is a specific technique that takes two terms and finds a substitution that would make the terms equal. For example, given terms $book(x,\text{"Fishing"},2010)$ and $book(\text{D.~Smith},y,2010)$, unification would produce substitution $\{x\mapsto\text{D. Smith},y\mapsto\text{"Fishing"}\}$.
Unification is likely used inside SMT solvers.