Leí en Wikipedia que la unificación es un proceso para resolver el problema de la satisfacción.
Al mismo tiempo, sé que tales solucionadores se llaman "solucionadores SAT" o "solucionadores SMT". Entonces, ¿son nombres diferentes para la misma cosa?
Si dice que son diferentes, señale una falla en mi tratamiento.
Respuestas:
Los solucionadores de SAT resuelven el problema de satisfacción booleana . Este es "el problema de determinar si las variables de una fórmula booleana dada pueden asignarse de tal manera que la fórmula se evalúe como VERDADERA".
Un ejemplo es encontrar una asignación de valores de verdad a las variables tal que es verdadero. Un solucionador SAT podría devolver una solución como , , .a , b , c ( a ∨ b ∨ c ) ∧ ( ¬ a ∨ ¬ b ∨ c ) ∧ ( a ∨ ¬ b ∨ ¬ c ) ∧ ( ¬ a ∨ b ∨ ¬ c ) a = t r u e b = t r u e c = t r u e
Los solucionadores de SMT resuelven un problema más general, a saber, las Teorías del módulo de satisfacción . Este es "un problema de decisión para fórmulas lógicas con respecto a combinaciones de teorías de fondo expresadas en lógica clásica de primer orden con igualdad". Estas teorías podrían incluir "la teoría de los números reales, la teoría de los enteros y las teorías de varias estructuras de datos como listas, matrices, vectores de bits, etc."
Un ejemplo, dadas las variables tipadas e y , pregunta si lo siguiente es satisfactorio . Un solucionador SMT respondería sí, con una solución de , , y .x : i n t y: i n t F: i n t → i n t F( x + 2 ) ≠ f( y- 1 ) ∧ x = ( y- 4 ) x = - 2 y= 2 F( 0 ) = 1 F( 1 ) = 3
La unificación es una técnica específica que toma dos términos y encuentra una sustitución que haría que los términos fueran iguales. Por ejemplo, dados los términos y , la unificación produciría la sustitución . La unificación probablemente se usa dentro de los solucionadores SMT.b O O K ( D. ~ Smith , y , 2010 ) { x ↦ D. Smith , y ↦ "Pesca" }b o o k ( x , "Pesca" , 2010 ) b o o k ( D. ~ Smith , y, 2010 ) { x ↦ D. Smith , y↦ "Pesca" }
fuente