Satisfacibilidad módulo teorías

En informática y lógica matemática , la satisfacibilidad módulo teorías ( SMT ) es el problema de determinar si una fórmula matemática es satisfacible . Generaliza el problema de satisfacibilidad booleana (SAT) a fórmulas más complejas que involucran números reales , enteros y/o diversas estructuras de datos como listas , matrices , vectores de bits y cadenas . El nombre deriva del hecho de que estas expresiones se interpretan dentro ("módulo") de una teoría formal determinada en lógica de primer orden con igualdad (que a menudo no permite cuantificadores ). Los solucionadores de SMT son herramientas que buscan resolver el problema SMT para un subconjunto práctico de entradas. Solucionadores de SMT como Z3 y cvc5 se han utilizado como un componente básico para una amplia gama de aplicaciones en informática, incluyendo la demostración automática de teoremas , el análisis de programas , la verificación de programas y las pruebas de software .

Dado que la satisfacibilidad booleana ya es NP-completa , el problema SMT suele ser NP-difícil , y para muchas teorías es indecidible . Los investigadores estudian qué teorías o subconjuntos de teorías dan lugar a un problema SMT decidible y la complejidad computacional de los casos decidibles. Los procedimientos de decisión resultantes se implementan a menudo directamente en solucionadores SMT; véase, por ejemplo, la decidibilidad de la aritmética de Presburger . SMT puede considerarse un problema de satisfacción de restricciones y, por lo tanto, un enfoque formalizado para la programación con restricciones .

Formalmente hablando, una instancia de SMT es una fórmula en lógica de primer orden , donde algunos símbolos de función y predicado tienen interpretaciones adicionales, y SMT es el problema de determinar si dicha fórmula es satisfacible. En otras palabras, imagine una instancia del problema de satisfacibilidad booleana (SAT) en la que algunas de las variables binarias se reemplazan por predicados sobre un conjunto adecuado de variables no binarias. Un predicado es una función con valor binario de variables no binarias. Ejemplos de predicados incluyen desigualdades lineales (por ejemplo,${\displaystyle 3x+2y-z\geq 4}$) o igualdades que involucran términos no interpretados y símbolos de función (por ejemplo,${\displaystyle f(f(u,v),v)=f(u,v)}$dónde${\displaystyle f}$es alguna función no especificada de dos argumentos). Estos predicados se clasifican según la teoría asignada. Por ejemplo, las desigualdades lineales sobre variables reales se evalúan utilizando las reglas de la teoría de la aritmética lineal real , mientras que los predicados que involucran términos no interpretados y símbolos de función se evalúan utilizando las reglas de la teoría de funciones no interpretadas con igualdad (a veces denominada teoría vacía ). Otras teorías incluyen las teorías de arreglos y estructuras de listas (útiles para modelar y verificar programas informáticos ) y la teoría de vectores de bits (útil para modelar y verificar diseños de hardware ). También son posibles subteorías: por ejemplo, la lógica de diferencias es una subteoría de la aritmética lineal en la que cada desigualdad está restringida a tener la forma${\displaystyle xy>c}$para variables${\displaystyle x}$y${\displaystyle y}$y constante${\displaystyle c}$.

Los ejemplos anteriores muestran el uso de la aritmética lineal entera sobre desigualdades. Otros ejemplos incluyen:

• Satisfacibilidad: Determinar si${\displaystyle x\vee (y\wedge \neg z)}$es satisfactorio.
• Acceso a la matriz: Encuentra un valor para la matriz A tal que A [0]  =  5.
• Aritmética de vectores de bits: Determinar si x e y son números de 3 bits distintos.
• Funciones sin interpretar: Encuentra valores para x e y tales que${\displaystyle f(x)=2}$y${\displaystyle g(x)=3}$.

La mayoría de los solucionadores SMT solo admiten fragmentos de sus lógicas que no contengan cuantificadores .

Existe una superposición sustancial entre la resolución de SMT y la demostración automática de teoremas (ATP). Generalmente, los demostradores automáticos de teoremas se centran en admitir lógica de primer orden completa con cuantificadores, mientras que los solucionadores de SMT se centran más en admitir diversas teorías (símbolos de predicado interpretados). Los ATP sobresalen en problemas con muchos cuantificadores, mientras que los solucionadores de SMT funcionan bien en problemas grandes sin cuantificadores. ^{[ 1 ]} La línea divisoria es lo suficientemente difusa como para que algunos ATP participen en SMT-COMP, mientras que algunos solucionadores de SMT participan en CASC . ^{[ 2 ]}

Una instancia SMT es una generalización de una instancia SAT booleana en la que diversos conjuntos de variables se reemplazan por predicados de diferentes teorías subyacentes. Las fórmulas SMT proporcionan un lenguaje de modelado mucho más rico que el que ofrecen las fórmulas SAT booleanas. Por ejemplo, una fórmula SMT permite modelar las operaciones de la ruta de datos de un microprocesador a nivel de palabra, en lugar de a nivel de bit.

En comparación, la programación de conjuntos de respuestas también se basa en predicados (más precisamente, en sentencias atómicas creadas a partir de fórmulas atómicas ). A diferencia de SMT, los programas de conjuntos de respuestas no tienen cuantificadores y no pueden expresar fácilmente restricciones como la aritmética lineal o la lógica de diferencias ; la programación de conjuntos de respuestas es más adecuada para problemas booleanos que se reducen a la teoría libre de funciones no interpretadas. La implementación de enteros de 32 bits como vectores de bits en la programación de conjuntos de respuestas sufre de la mayoría de los mismos problemas que enfrentaron los primeros solucionadores de SMT: las identidades "obvias" como x  + y = y + x son difíciles de deducir.     

La programación lógica con restricciones sí ofrece soporte para restricciones aritméticas lineales, pero dentro de un marco teórico completamente diferente. Los solucionadores SMT también se han extendido para resolver fórmulas en lógica de orden superior . ^{[ 3 ]}

Los primeros intentos de resolver instancias SMT implicaron traducirlas a instancias SAT booleanas (por ejemplo, una variable entera de 32 bits se codificaría mediante 32 variables de un solo bit con pesos apropiados y las operaciones a nivel de palabra, como 'más', se reemplazarían por operaciones lógicas de nivel inferior en los bits) y pasar esta fórmula a un solucionador SAT booleano. Este enfoque, que se conoce como enfoque ansioso (o bitblasting ), tiene sus méritos: al preprocesar la fórmula SMT en una fórmula SAT booleana equivalente , los solucionadores SAT booleanos existentes se pueden usar "tal cual" y sus mejoras de rendimiento y capacidad se pueden aprovechar con el tiempo. Por otro lado, la pérdida de la semántica de alto nivel de las teorías subyacentes significa que el solucionador SAT booleano tiene que trabajar mucho más de lo necesario para descubrir hechos "obvios" (como${\displaystyle x+y=y+x}$(para la suma de enteros). Esta observación condujo al desarrollo de varios solucionadores SMT que integran estrechamente el razonamiento booleano de una búsqueda de estilo DPLL con solucionadores específicos de la teoría ( T-solucionadores ) que manejan conjunciones (AND) de predicados de una teoría dada. Este enfoque se conoce como el enfoque perezoso . ^{[ 4 ]}

Denominada DPLL(T) [ ^{5 ] ,} esta arquitectura otorga la responsabilidad del razonamiento booleano al solucionador SAT basado en DPLL, el cual, a su vez, interactúa con un solucionador para la teoría T a través de una interfaz bien definida. El solucionador de teoría solo necesita preocuparse por verificar la factibilidad de las conjunciones de predicados de teoría que le pasa el solucionador SAT mientras explora el espacio de búsqueda booleano de la fórmula. Sin embargo, para que esta integración funcione bien, el solucionador de teoría debe poder participar en la propagación y el análisis de conflictos, es decir, debe poder inferir nuevos hechos a partir de hechos ya establecidos, así como proporcionar explicaciones concisas de infactibilidad cuando surgen conflictos de teoría. En otras palabras, el solucionador de teoría debe ser incremental y con capacidad de retroceso .

Los investigadores estudian qué teorías o subconjuntos de teorías conducen a un problema SMT decidible y la complejidad computacional de los casos decidibles. Dado que la lógica de primer orden completa es solo semidecidible , una línea de investigación intenta encontrar procedimientos de decisión eficientes para fragmentos de lógica de primer orden, como la lógica proposicional efectiva . ^{[ 6 ]}

Otra línea de investigación implica el desarrollo de teorías decidibles especializadas , incluyendo aritmética lineal sobre racionales y enteros , vectores de bits de ancho fijo, ^{[ 7 ]} aritmética de punto flotante (a menudo implementada en solucionadores SMT a través de explosión de bits , es decir, reducción a vectores de bits), ^{[ 8 ] [ 9 ]} cadenas , ^{[ 10 ]} (co)tipos de datos , ^{[ 11 ]} secuencias (utilizadas para modelar matrices dinámicas ), ^{[ 12 ]} conjuntos y relaciones finitos , ^{[ 13 ] [ 14 ]} lógica de separación , ^{[ 15 ]} campos finitos , ^{[ 16 ]} y funciones no interpretadas, entre otras.

Las teorías monótonas booleanas son una clase de teoría que admite la propagación eficiente de teorías y el análisis de conflictos, lo que permite su uso práctico dentro de los solucionadores DPLL(T). ^{[ 17 ]} Las teorías monótonas solo admiten variables booleanas (Booleano es el único tipo ), y todas sus funciones y predicados p obedecen el axioma

${\displaystyle p(\ldots ,b_{i-1},0,b_{i+1},\ldots )\implies p(\ldots ,b_{i-1},1,b_{i+1},\ldots )}$

Ejemplos de teorías monótonas incluyen la alcanzabilidad de grafos , la detección de colisiones para envolventes convexas , los cortes mínimos y la lógica de árboles de computación . ^{[ 18 ]} Todo programa Datalog puede interpretarse como una teoría monótona. ^{[ 19 ]}

La mayoría de los enfoques SMT comunes admiten teorías decidibles . Sin embargo, muchos sistemas del mundo real, como una aeronave y su comportamiento, solo pueden modelarse mediante aritmética no lineal sobre los números reales que involucran funciones trascendentales . Este hecho motiva una extensión del problema SMT a teorías no lineales, como determinar si la siguiente ecuación es satisfacible:

${\displaystyle {\begin{array}{lr}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\vee b\vee -x^{2}\geq 2.3y)\wedge \left(\neg b\vee y<-34.4\vee \exp(x)>{y \over x}\right)\end{array}}}$

dónde

${\displaystyle b\in {\mathbb {B} },x,y\in {\mathbb {R} }.}$

Sin embargo, tales problemas son, en general, indecidibles . (Por otro lado, la teoría de los cuerpos reales cerrados , y por ende la teoría completa de primer orden de los números reales , son decidibles mediante la eliminación de cuantificadores . Esto se debe a Alfred Tarski ). La teoría de primer orden de los números naturales con suma (pero no con multiplicación), llamada aritmética de Presburger , también es decidible. Dado que la multiplicación por constantes puede implementarse como sumas anidadas, la aritmética en muchos programas informáticos puede expresarse utilizando la aritmética de Presburger, lo que da como resultado fórmulas decidibles.

Ejemplos de solucionadores SMT que abordan combinaciones booleanas de átomos de teoría de teorías aritméticas indecidibles sobre los reales son ABsolver, ^{[ 20 ]} que emplea una arquitectura DPLL(T) clásica con un paquete de optimización no lineal como solucionador de teoría subordinada (necesariamente incompleta), iSAT , que se basa en una unificación de la resolución SAT de DPLL y la propagación de restricciones de intervalo llamada algoritmo iSAT, ^{[ 21 ]} y cvc5 . ^{[ 22 ]}

La tabla siguiente resume algunas de las características de los numerosos solucionadores SMT disponibles. La columna "SMT-LIB" indica compatibilidad con el lenguaje SMT-LIB; muchos sistemas marcados con "sí" pueden admitir solo versiones anteriores de SMT-LIB u ofrecer solo compatibilidad parcial con el lenguaje. La columna "CVC" indica compatibilidad con el lenguaje CVC . La columna "DIMACS" indica compatibilidad con el formato DIMACS .

Los proyectos difieren no solo en sus características y rendimiento, sino también en la viabilidad de la comunidad que los rodea, su interés continuo en el proyecto y su capacidad para contribuir con documentación, correcciones, pruebas y mejoras.

Los solucionadores SMT son útiles tanto para la verificación, demostrando la corrección de los programas (pruebas de software basadas en la ejecución simbólica) , como para la síntesis , generando fragmentos de programas mediante la búsqueda en el espacio de programas posibles. Fuera de la verificación de software, los solucionadores SMT también se han utilizado para la inferencia de tipos ^{[ 26 ] [ 27 ]} y para modelar escenarios teóricos, incluyendo el modelado de las creencias de los actores en el control de armas nucleares . ^{[ 28 ]}

• Programación de conjuntos de respuestas
• Demostración automatizada de teoremas
• solucionador SAT
• Lógica de primer orden
• Teoría de la igualdad pura

• Este artículo fue adaptado originalmente de una columna publicada en el boletín electrónico de ACM SIGDA por Karem A. Sakallah . El texto original está disponible aquí .