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.

terminology sat-solvers unification

— Val
źródło

informatyka często odnosi się do „problemu satysfakcji”, ale w rzeczywistości jest to szczególny przypadek problemu ogólnego [o którym mowa w artykule na temat unifikacji w Wikipedii], który może zawierać bardziej złożone klauzule, takie jak „istnieje” i „dla wszystkich” innych niż tylko zmienne boolowskie. w CS odniesienie do „problemu satysfakcji” może być naprawdę skrótem dla proposycyjnego lub logicznego problemu satysfakcji , w skrócie SAT. proces unifikacji w SAT nazywa się rozdzielczością

— dniu

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

— Dave Clarke
źródło

Wszystkie słowa są znane w zdaniu „Unifikacja jest prawdopodobnie używana gdzieś w rozwiązaniach SMT (i może w rozwiązaniach SAT)”, ale ja tego nie rozumiem. Znajdziesz również taką definicję SMT, że trudno jest zrozumieć, czy SAT jest jej szczególnym przypadkiem.

— Val

SAT zajmuje się logiką zdań. Logika pierwszego rzędu, na której opiera się SMT, jest bardziej ogólna.

— Dave Clarke,