# Unification vs. SAT solver

I read on Wikipedia that unification is a process of solving the satisfability problem.

At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different names for the same thing?

If you say that they are different, please point out a flaw in my treatment.

• computer science often refers to the "satisfiability problem" but that is actually a special case of the general problem [refered to in the wikipedia article on unification] which may have more complex clauses like with "there exists" and "for all" other than merely boolean variables. in CS, reference to the "satisfiability problem" may be really shorthand for the propositional or boolean satisfiability problem, abbreviated SAT. unification process in SAT is called resolution – vzn Sep 21 '12 at 17:43

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$.
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.