10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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 $\endgroup$ – vzn Sep 21 '12 at 17:43
12
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ All the words are familiar in the sentence "Unification is probably used somewhere SMT solvers (and maybe in SAT solvers)" but I do not understand it. You also find such definition of SMT that it is difficult to understand if SAT is a special case of it. $\endgroup$ – Val Sep 21 '12 at 9:11
  • $\begingroup$ SAT deals with propositional logic. First order logic, upon which SMT is based, is more general. $\endgroup$ – Dave Clarke Sep 21 '12 at 9:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.