Solucionador de Unificação vs. SAT

10

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.

Val
fonte
A ciência da computação geralmente se refere ao "problema de satisfação", mas esse é realmente um caso especial do problema geral [referido no artigo da wikipedia sobre unificação], que pode ter cláusulas mais complexas, como "existe" e "para todos", exceto apenas variáveis ​​booleanas. no CS, a referência ao "problema de satisfação" pode ser realmente uma abreviação para o problema de satisfação proposicional ou booleano , abreviado SAT. processo de unificação no SAT é chamado de resolução
vzn

Respostas:

12

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(abc)(¬a¬bc)(a¬b¬c)(¬ab¬c)a=trueb=truec=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:inty:intf:intintf(x+2)f(y1)x=(y4)x=2y=2f(0)=1f(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,"Fishing",2010)book(D.~Smith,y,2010){xD. Smith,y"Fishing"}

Dave Clarke
fonte
Todas as palavras são familiares na frase "A unificação provavelmente é usada em algum lugar dos solucionadores SMT (e talvez nos solucionadores SAT)", mas eu não entendo. Você também encontra essa definição de SMT que é difícil entender se o SAT é um caso especial dele.
Val
O SAT lida com a lógica proposicional. A lógica de primeira ordem, na qual o SMT se baseia, é mais geral.
21412 Dave Clarke