Teorías de satisfacibilidad módulo

En ciencias de la computación y lógica matemática, el problema de las teorías de satisfacibilidad módulo (SMT por sus siglas del inglés satisfiability modulo theories) es un problema de decisión para fórmulas lógicas con respecto a las combinaciones de teorías subyacentes expresadas en la lógica de primer orden clásica con igualdad. Ejemplos de teorías usadas comúnmente en ciencias de la computación son la teoría de los números reales, la teoría de los enteros, y las teorías sobre diversas estructuras de datos como listas, arrays, bit strings y demás. Los SMT se pueden ver como una forma del problema de satisfacción de restricciones (CSP) y por tanto crear una aproximación formalizada hacia la programación con restricciones.

Terminología básica

Formalmente hablando, una instancia del SMT es una fórmula en lógica de primer orden en la que alguna función y símbolos de predicados tienen interpretaciones adicionales, y el problema del SMT reside en determinar si una fórmula es satisfactible. En otras palabras, dada una instancia del problema de satisfacibilidad booleana (SAT) en el que alguna de las variables binarias se reemplazan por predicados sobre un conjunto adecuado de variables no binarias. Un predicado es básicamente una función de dos variables no binarias. Ejemplos de predicados incluyen desigualdades o desigualdades con términos no interpretados y funciones simbólicas (por ejemplo,$f(f(u,v),v)=f(u,v)$ donde $f$ es alguna función no especificada de dos argumentos no especificados). Estos predicados se clasifican según la teoría respectiva que se les asigne. Por ejemplo, las desigualdades lineales sobre variables reales son evaluadas utilizando las reglas de la teoría de la aritmética lineal, mientras que los predicados que incluyan términos no interpretados y funciones simbólicas son evaluadas utilizando las reglas de la teoría de funciones no interpretadas con igualdad (a veces llamada también empty theory). Otras teorías incluyen las teorías sobre arrays y estructuras de listas (útiles para modelar y verificar programas informáticos), y las teorías de vectores de bits (útiles para modelar y verificar diseños hardware). También es posible establecer subteorías: por ejemplo, la lógica de diferencias es una sub-teoría de la aritmética lineal en la que cada desigualdad está restringida a la forma $x-y>c$ para variables $x$ e $y$ y constante $c$.

La mayoría de los solvers matemáticos disponibles únicamente soportan las partes de sus lógicas sin cuantificadores.

Enlaces externos

• Datos: Q2067766