Solucionador de Unificação vs. SAT

Li na Wikipedia que a unificação é um processo de solução do problema de satisfação.

Ao mesmo tempo, eu sei que esses solucionadores são chamados de "solucionadores SAT" ou "solucionadores SMT". Então, eles são nomes diferentes para a mesma coisa?

Se você diz que eles são diferentes, por favor, indique uma falha no meu tratamento.

Os solucionadores de SAT resolvem o problema de satisfação booleana . Este é "o problema de determinar se as variáveis ​​de uma determinada fórmula booleana podem ser atribuídas de forma a fazer com que a fórmula seja avaliada como VERDADEIRA".

Um exemplo é encontrar uma atribuição de valores de verdade para as variáveis modo que é verdadeiro. Um solucionador SAT pode retornar uma solução como , , .$a,b,c$$(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)$$a=true$$b=true$$c=true$

Os solucionadores SMT resolvem um problema mais geral, a saber, as Teorias do Módulo de Satisfação . Este é "um problema de decisão para fórmulas lógicas no que diz respeito a combinações de teorias de fundo expressas na lógica clássica de primeira ordem com igualdade". Essas teorias podem incluir "a teoria dos números reais, a teoria dos números inteiros e as teorias de várias estruturas de dados, como listas, matrizes, vetores de bits e assim por diante".

Um exemplo, dados variáveis digitadas e e , pergunta se o seguinte é satisfatível . Um solucionador SMT responderia sim, com solução , , e .$x:int$$y:int$$f:int\to int$$f(x+2) \neq f(y-1) \land x=(y- 4)$$x=-2$$y=2$$f(0)=1$$f(1)=3$

A unificação é uma técnica específica que usa dois termos e encontra uma substituição que tornaria os termos iguais. Por exemplo, dados os termos e , a unificação produziria substituição . Provavelmente, a unificação é usada nos solucionadores SMT.$book(x,\text{"Fishing"},2010)$$book(\text{D.~Smith},y,2010)$$\{x\mapsto\text{D. Smith},y\mapsto\text{"Fishing"}\}$