Unifikacja vs. solver SAT

Czytałem na Wikipedii, że zjednoczenie jest procesem rozwiązywania problemu satysfakcji.

Jednocześnie wiem, że takie solwery nazywane są „solverami SAT” lub „solverami SMT”. Czy są to różne nazwy dla tej samej rzeczy?

Jeśli powiesz, że się różnią, proszę wskazać wadę mojego leczenia.

Solvery SAT rozwiązują problem logicznej satysfakcji . Jest to „problem z określeniem, czy zmienne danej formuły boolowskiej można przypisać w taki sposób, aby formuła uzyskała wartość PRAWDA”.

$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$. , c = t r u $b=true$$c=true$

Solvery SMT rozwiązują bardziej ogólny problem, mianowicie Solvery teorie satysfakcji Modulo . Jest to „problem decyzyjny dla formuł logicznych w odniesieniu do kombinacji teorii tła wyrażonych w klasycznej logice pierwszego rzędu z równością”. Teorie te mogą obejmować „teorię liczb rzeczywistych, teorię liczb całkowitych oraz teorie różnych struktur danych, takich jak listy, tablice, wektory bitowe i tak dalej”.

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

$book(x,\text{"Fishing"},2010)$$book(\text{D.~Smith},y,2010)$ , ujednolicenie spowoduje powstanie podstawienia$\{x\mapsto\text{D. Smith},y\mapsto\text{"Fishing"}\}$. Ujednolicenie jest prawdopodobnie stosowane w rozwiązaniach SMT.