Unification vs solveur SAT

J'ai lu sur Wikipedia que l' unification est un processus de résolution du problème de satisfaction.

En même temps, je sais que de tels solveurs sont appelés "solveurs SAT" ou "solveurs SMT". Alors, sont-ils des noms différents pour la même chose?

Si vous dites qu'ils sont différents, veuillez signaler une faille dans mon traitement.

terminology sat-solvers unification Val
la source

l'informatique se réfère souvent au "problème de satisfiabilité" mais c'est en fait un cas particulier du problème général [mentionné dans l'article de wikipedia sur l'unification] qui peut avoir des clauses plus complexes comme avec "il existe" et "pour tous" autres que simplement des variables booléennes. dans CS, la référence au "problème de satisfiabilité" peut être vraiment un raccourci pour le problème de satisfiabilité propositionnelle ou booléenne , abrégé SAT. le processus d'unification dans SAT est appelé résolution

vzn

Réponses:

Les solveurs SAT résolvent le problème de satisfaction booléenne . C'est "le problème de déterminer si les variables d'une formule booléenne donnée peuvent être affectées de manière à rendre la formule évaluée à VRAI".

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

Les solveurs SMT résolvent un problème plus général, à savoir les théories de Modulo de Satisfiance . Il s'agit "d'un problème de décision pour les formules logiques en ce qui concerne les combinaisons de théories de fond exprimées en logique classique du premier ordre avec égalité". Ces théories pourraient inclure «la théorie des nombres réels, la théorie des nombres entiers et les théories de diverses structures de données telles que les listes, les tableaux, les vecteurs de bits, etc.».

$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)$ $\{x\mapsto\text{D. Smith},y\mapsto\text{"Fishing"}\}$

Dave Clarke
la source

Tous les mots sont familiers dans la phrase "L'unification est probablement utilisée quelque part dans les solveurs SMT (et peut-être dans les solveurs SAT)" mais je ne la comprends pas. Vous trouvez également une telle définition de SMT qu'il est difficile de comprendre si SAT en est un cas particulier.

Val

SAT traite de la logique propositionnelle. La logique du premier ordre, sur laquelle SMT est basé, est plus générale.

Dave Clarke