Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
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.
