En informática y lógica matemática , el problema de las teorías de módulo de satisfacibilidad ( SMT ) 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. Algunos ejemplos de teorías que se utilizan normalmente en informática son 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. SMT se puede considerar como una forma deproblema de satisfacción de restricciones y, por lo tanto, un cierto enfoque formalizado de la programación de restricciones .
Terminología básica
Hablando formalmente, 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 satisfactoria. En otras palabras, imagine una instancia del problema de satisfacibilidad booleano (SAT) en el que algunas de las variables binarias se reemplazan por predicados sobre un conjunto adecuado de variables no binarias. Un predicado es una función de valores binarios de variables no binarias. Los predicados de ejemplo incluyen desigualdades lineales (p. Ej.,) o igualdades que involucran términos no interpretados y símbolos de función (p. ej., dónde es una función no especificada de dos argumentos). Estos predicados se clasifican de acuerdo con cada teoría respectiva asignada. Por ejemplo, las desigualdades lineales sobre variables reales se evalúan usando las reglas de la teoría de la aritmética real lineal , mientras que los predicados que involucran términos no interpretados y símbolos de función se evalúan usando 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 matrices y estructuras de listas (útiles para modelar y verificar programas de computadora ) y la teoría de vectores de bits (útil para modelar y verificar diseños de hardware ). Las subteorías también son posibles: por ejemplo, la lógica de diferencias es una subteoría de la aritmética lineal en la que cada desigualdad está restringida para tener la forma para variables y y constante .
La mayoría de los solucionadores SMT solo admiten fragmentos libres de cuantificadores de sus lógicas.
Poder expresivo
Una instancia de SMT es una generalización de una instancia de SAT booleana en la que varios conjuntos de variables se reemplazan por predicados de una variedad de teorías subyacentes. Las fórmulas SMT proporcionan un lenguaje de modelado mucho más rico de lo que es posible con las fórmulas booleanas SAT. Por ejemplo, una fórmula SMT nos permite modelar las operaciones de la ruta de datos de un microprocesador a nivel de palabra en lugar de bit.
En comparación, la programación de conjuntos de respuestas también se basa en predicados (más precisamente, en oraciones 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 ; en el mejor de los casos, ASP es adecuado 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 ASP sufre la mayoría de los mismos problemas que enfrentaron los primeros solucionadores de SMT: identidades "obvias" como x + y = y + x son difíciles de deducir.
La programación de lógica de restricciones proporciona soporte para restricciones aritméticas lineales, pero dentro de un marco teórico completamente diferente. [ cita requerida ] Los solucionadores SMT también se han extendido para resolver fórmulas en lógica de orden superior . [1]
Enfoques del solucionador
Los primeros intentos para resolver instancias SMT implicaron traducirlas a instancias SAT booleanas (por ejemplo, una variable entera de 32 bits estaría codificada por 32 variables de un solo bit con pesos apropiados y operaciones a nivel de palabra como 'más' serían reemplazadas por menores operaciones lógicas de nivel en los bits) y pasar esta fórmula a un solucionador booleano SAT. Este enfoque, que se conoce como el enfoque ansioso , 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 aprovechan 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 de SAT booleano tiene que trabajar mucho más duro de lo necesario para descubrir hechos "obvios" (comopara la suma de enteros.) Esta observación condujo al desarrollo de una serie de solucionadores SMT que integran estrechamente el razonamiento booleano de una búsqueda de estilo DPLL con solucionadores específicos de teoría ( T-solvers ) que manejan conjunciones (AND) de predicados de un determinado teoría. Este enfoque se conoce como el vago enfoque .
Apodado DPLL (T) , [2] esta arquitectura da la responsabilidad del razonamiento booleano al solucionador SAT basado en DPLL que, 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ías solo necesita preocuparse por comprobar la viabilidad de las conjunciones de los predicados teóricos que se le transmiten desde el solucionador SAT mientras explora el espacio de búsqueda booleana de la fórmula. Sin embargo, para que esta integración funcione bien, el solucionador de teorías debe poder participar en la propagación y el análisis de conflictos, es decir, debe poder inferir hechos nuevos a partir de hechos ya establecidos, así como proporcionar explicaciones sucintas de la inviabilidad cuando la teoría entra en conflicto. aumentar. En otras palabras, el solucionador de teorías debe ser incremental y rastreable .
SMT para teorías indecidibles
La mayoría de los enfoques SMT comunes apoyan teorías decidibles . Sin embargo, muchos sistemas del mundo real solo pueden modelarse mediante aritmética no lineal sobre los números reales que involucran funciones trascendentales , por ejemplo, un avión y su comportamiento. Este hecho motiva una extensión del problema SMT a teorías no lineales, por ejemplo, determinar si
dónde
es satisfactorio. Entonces, estos problemas se vuelven indecidibles en general. (La teoría de los campos cerrados reales , y por lo tanto la teoría completa de primer orden de los números reales , sin embargo, se pueden decidir usando la eliminación del cuantificador . Esto se debe a Alfred Tarski ). La teoría de primer orden de los números naturales con suma (pero no multiplicación) , llamada aritmética de Presburger , también es decidible. Dado que la multiplicación por constantes se puede implementar como sumas anidadas, la aritmética en muchos programas de computadora se puede expresar usando la aritmética de Presburger, lo que resulta en fórmulas decidibles.
Ejemplos de solucionadores SMT que abordan combinaciones booleanas de átomos teóricos a partir de teorías aritméticas indecidibles sobre los reales son ABsolver, [3] que emplea una arquitectura DPLL (T) clásica con un paquete de optimización no lineal como solucionador teórico subordinado (necesariamente incompleto) e iSAT , basado en una unificación de la resolución DPLL SAT y la propagación de restricciones de intervalo llamada algoritmo iSAT. [4]
Solucionadores
La siguiente tabla resume algunas de las características de los muchos 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 soporte parcial para el idioma. La columna "CVC" indica soporte para el lenguaje CVC. La columna "DIMACS" indica la compatibilidad con el formato DIMACS .
Los proyectos difieren no solo en características y rendimiento, sino también en la viabilidad de la comunidad circundante, su interés continuo en un proyecto y su capacidad para contribuir con documentación, correcciones, pruebas y mejoras.
Plataforma | Características | Notas | |||||||
---|---|---|---|---|---|---|---|---|---|
Nombre | SO | Licencia | SMT-LIB | CVC | DIMACS | Teorías integradas | API | SMT-COMP [1] | |
ABsolver | Linux | CPL | v1.2 | No | sí | aritmética lineal, aritmética no lineal | C ++ | No | Basado en DPLL |
Alt-Ergo | Linux , Mac OS , Windows | CeCILL-C (aproximadamente equivalente a LGPL ) | parcial v1.2 y v2.0 | No | No | teoría vacía , aritmética lineal y aritmética racional, aritmética no lineal, matrices polimórficas , tipos de datos enumerados , símbolos AC , vectores de bits , tipos de datos de registros , cuantificadores | OCaml | 2008 | El lenguaje de entrada polimórfico de primer orden à la ML, basado en SAT-solver, combina enfoques similares a Shostak y Nelson-Oppen para razonar teorías de módulo |
Barcelogic | Linux | Propiedad | v1.2 | teoría vacía , lógica de la diferencia | C ++ | 2009 | Cierre de congruencia basado en DPLL | ||
Castor | Linux , Windows | BSD | v1.2 | No | No | bitvectors | OCaml | 2009 | Basado en solucionador SAT |
Boolector | Linux | MIT | v1.2 | No | No | vectores de bits , matrices | C | 2009 | Basado en solucionador SAT |
CVC3 | Linux | BSD | v1.2 | sí | teoría vacía , aritmética lineal, matrices, tuplas, tipos, registros, vectores de bits, cuantificadores | C / C ++ | 2010 | salida de prueba a HOL | |
CVC4 | Linux , Mac OS , Windows , FreeBSD | BSD | sí | sí | aritmética lineal racional y entera, matrices, tuplas, registros, tipos de datos inductivos, vectores de bits, cadenas e igualdad sobre símbolos de función no interpretados | C ++ | 2010 | versión 1.5 publicada en julio de 2017 | |
Kit de herramientas de procedimiento de decisión (DPT) | Linux | apache | No | OCaml | No | Basado en DPLL | |||
Me senté | Linux | Propiedad | No | aritmética no lineal | No | Basado en DPLL | |||
MathSAT | Linux , Mac OS , Windows | Propiedad | sí | sí | teoría vacía , aritmética lineal, aritmética no lineal, vectores de bits, matrices | C / C ++ , Python , Java | 2010 | Basado en DPLL | |
MiniSmt | Linux | LGPL | parcial v2.0 | aritmética no lineal | 2010 | Basado en SAT-solver, basado en Yices | |||
Norn | Solucionador de SMT para restricciones de cadena | ||||||||
OpenCog | Linux | AGPL | No | No | No | lógica probabilística , aritmética. modelos relacionales | C ++ , esquema , Python | No | isomorfismo de subgrafo |
OpenSMT | Linux , Mac OS , Windows | GPLv3 | parcial v2.0 | sí | teoría vacía , diferencias, aritmética lineal, vectores de bits | C ++ | 2011 | solucionador SMT perezoso | |
raSAT | Linux | GPLv3 | v2.0 | aritmética no lineal real y entera | 2014, 2015 | extensión de la propagación de restricción de intervalo con pruebas y el teorema del valor intermedio | |||
Satén | ? | Propiedad | v1.2 | aritmética lineal, lógica de diferencias | ninguno | 2009 | |||
SMTInterpol | Linux , Mac OS , Windows | LGPLv3 | v2.5 | funciones no interpretadas, aritmética real lineal y aritmética de enteros lineales | Java | 2012 | Se centra en generar interpolantes compactos de alta calidad. | ||
SMCHR | Linux , Mac OS , Windows | GPLv3 | No | No | No | aritmética lineal, aritmética no lineal, montones | C | No | Puede implementar nuevas teorías usando reglas de manejo de restricciones . |
SMT-RAT | Linux , Mac OS | MIT | v2.0 | No | No | aritmética lineal, aritmética no lineal | C ++ | 2015 | Caja de herramientas para resolución SMT estratégica y paralela que consta de una colección de implementaciones compatibles con SMT. |
SONOLAR | Linux , Windows | Propiedad | parcial v2.0 | bitvectors | C | 2010 | Basado en solucionador SAT | ||
Lanza | Linux , Mac OS , Windows | Propiedad | v1.2 | bitvectors | 2008 | ||||
STP | Linux , OpenBSD , Windows , Mac OS | MIT | parcial v2.0 | sí | No | vectores de bits, matrices | C , C ++ , Python , OCaml , Java | 2011 | Basado en solucionador SAT |
ESPADA | Linux | Propiedad | v1.2 | bitvectors | 2009 | ||||
UCLID | Linux | BSD | No | No | No | teoría vacía , aritmética lineal, vectores de bits y lambda restringida (matrices, memorias, caché, etc.) | No | Basado en SAT-solver, escrito en Moscow ML . El idioma de entrada es el verificador de modelos SMV. ¡Bien documentado! | |
veriT | Linux , OS X | BSD | parcial v2.0 | teoría vacía , aritmética lineal racional y entera, cuantificadores e igualdad sobre símbolos de función no interpretados | C / C ++ | 2010 | Basado en solucionador SAT | ||
Yices | Linux , Mac OS , Windows , FreeBSD | GPLv3 | v2.0 | No | sí | aritmética lineal racional y entera, vectores de bits, matrices e igualdad sobre símbolos de función no interpretados | C | 2014 | El código fuente está disponible en línea |
Demostrador del teorema Z3 | Linux , Mac OS , Windows , FreeBSD | MIT | v2.0 | sí | teoría vacía , aritmética lineal, aritmética no lineal, vectores de bits, matrices, tipos de datos, cuantificadores , cadenas | C / C ++ , .NET , OCaml , Python , Java , Haskell | 2011 | El código fuente está disponible en línea |
Estandarización y la competencia de solucionadores SMT-COMP
Hay varios intentos de describir una interfaz estandarizada para los solucionadores SMT (y probadores automatizados de teoremas , un término que a menudo se usa como sinónimo). El más destacado es el estándar SMT-LIB, [ cita requerida ] que proporciona un lenguaje basado en expresiones-S . Otros formatos estandarizados comúnmente soportados son el formato DIMACS [ cita requerida ] soportado por muchos solucionadores SAT booleanos, y el formato CVC [ cita requerida ] usado por el demostrador automatizado de teoremas CVC.
El formato SMT-LIB también viene con una serie de puntos de referencia estandarizados y ha permitido una competencia anual entre solucionadores SMT llamada SMT-COMP. Inicialmente, la competencia tuvo lugar durante la conferencia de verificación asistida por computadora (CAV), [5] [6] pero a partir de 2020 la competencia se organiza como parte del taller SMT, que está afiliado a la Conferencia conjunta internacional sobre razonamiento automatizado (IJCAR ). [7]
Aplicaciones
Los solucionadores SMT son útiles tanto para verificación, probando la corrección de programas, pruebas de software basadas en ejecución simbólica , como para síntesis , generando fragmentos de programa buscando en el espacio de posibles programas. Fuera de la verificación de software, los solucionadores SMT también se han utilizado para la inferencia de tipos [8] [9] y para modelar escenarios teóricos, incluido el modelado de las creencias de los actores en el control de armas nucleares . [10]
Verificación
La verificación asistida por computadora de programas de computadora a menudo usa solucionadores SMT. Una técnica común es traducir las condiciones previas, las condiciones posteriores, las condiciones de bucle y las afirmaciones en fórmulas SMT para determinar si todas las propiedades pueden cumplirse.
Hay muchos verificadores construidos sobre el solucionador Z3 SMT . Boogie es un lenguaje de verificación intermedio que usa Z3 para verificar automáticamente programas imperativos simples. El verificador VCC para C concurrente usa Boogie, así como Dafny para programas imperativos basados en objetos, Chalice para programas concurrentes y Spec # para C #. F * es un lenguaje de escritura dependiente que usa Z3 para encontrar pruebas; el compilador lleva estas pruebas para producir un código de bytes portador de pruebas. La infraestructura de verificación Viper codifica las condiciones de verificación en Z3. La biblioteca sbv proporciona verificación basada en SMT de los programas Haskell y permite al usuario elegir entre varios solucionadores como Z3, ABC, Boolector, CVC4 , MathSAT y Yices.
También hay muchos verificadores construidos sobre el solucionador Alt-Ergo SMT. Aquí hay una lista de aplicaciones para adultos:
- Why3 , una plataforma para la verificación de programas deductivos, utiliza Alt-Ergo como su principal comprobador;
- CAVEAT, un verificador C desarrollado por CEA y utilizado por Airbus; Alt-Ergo fue incluido en la calificación DO-178C de uno de sus aviones recientes;
- Frama-C , un marco para analizar código C, usa Alt-Ergo en los complementos de Jessie y WP (dedicados a la "verificación deductiva del programa");
- SPARK usa CVC4 y Alt-Ergo (detrás de GNATprove) para automatizar la verificación de algunas afirmaciones en SPARK 2014;
- Atelier-B puede usar Alt-Ergo en lugar de su principal probador (aumentando el éxito del 84% al 98% en los puntos de referencia del proyecto ANR Bware );
- Rodin , un marco del método B desarrollado por Systerel, puede utilizar Alt-Ergo como back-end;
- Cubicle , un verificador de modelos de código abierto para verificar las propiedades de seguridad de los sistemas de transición basados en arreglos.
- EasyCrypt , un conjunto de herramientas para razonar sobre propiedades relacionales de cálculos probabilísticos con código adversario.
Muchos solucionadores SMT implementan un formato de interfaz común llamado SMTLIB2 (estos archivos suelen tener la extensión " .smt2 "). La herramienta LiquidHaskell implementa un verificador basado en tipos de refinamiento para Haskell que puede usar cualquier solucionador compatible con SMTLIB2, por ejemplo, CVC4, MathSat o Z3.
Análisis y pruebas basados en ejecución simbólica
Una aplicación importante de los solucionadores de SMT es la ejecución simbólica para el análisis y la prueba de programas (por ejemplo, pruebas concólicas ), especialmente para encontrar vulnerabilidades de seguridad. Las herramientas importantes que se mantienen activamente en esta categoría incluyen SAGE de Microsoft Research , KLEE , S2E y Triton . Los solucionadores SMT que son particularmente útiles para aplicaciones de ejecución simbólica incluyen Z3 , STP , Z3str2 y Boolector .
Ver también
- Programación del conjunto de respuestas
- Demostración automatizada de teoremas
Notas
- ^ Barbosa, Haniel, et al. " Ampliación de los solucionadores SMT a la lógica de orden superior ". Congreso Internacional de Deducción Automatizada. Springer, Cham, 2019.
- ^ Nieuwenhuis, R .; Oliveras, A .; Tinelli, C. (2006), "Resolver las teorías del módulo SAT y SAT: de un procedimiento abstracto de Davis-Putnam-Logemann-Loveland a DPLL (T)", Journal of the ACM (PDF) , 53 , pp. 937–977
- ^ Bauer, A .; Pister, M .; Tautschnig, M. (2007), "Soporte de herramientas para el análisis de sistemas y modelos híbridos", Actas de la Conferencia de 2007 sobre Diseño, Automatización y Pruebas en Europa (DATE'07) , IEEE Computer Society, p. 1, CiteSeerX 10.1.1.323.6807 , doi : 10.1109 / DATE.2007.364411 , ISBN 978-3-9810801-2-4, S2CID 9159847
- ^ Fränzle, M .; Herde, C .; Ratschan, S .; Schubert, T .; Teige, T. (2007), "Resolución eficiente de grandes sistemas de restricción aritmética no lineal con estructura booleana compleja", Número especial de JSAT sobre integración SAT / CP (PDF) , 1 , págs. 209-236
- ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "SMT-COMP: Concurso de teorías de módulo de satisfacción" . Verificación asistida por computadora . Apuntes de conferencias en informática. Berlín, Heidelberg: Springer: 20-23. doi : 10.1007 / 11513988_4 . ISBN 978-3-540-31686-2.
- ^ Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). "La iniciativa SMT-LIB y el auge de SMT" . Hardware y software: verificación y pruebas . Apuntes de conferencias en informática. Berlín, Heidelberg: Springer: 3–3. doi : 10.1007 / 978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.
- ^ "SMT-COMP 2020" . SMT-COMP . Consultado el 19 de octubre de 2020 .
- ^ Hassan, Mostafa, et al. "Inferencia de tipo basada en maxsmt para python 3". Conferencia Internacional sobre Verificación Asistida por Computadora. Springer, Cham, 2018.
- ^ Loncaric, Calvin, et al. "Un marco práctico para la explicación de errores de inferencia de tipos". Avisos ACM SIGPLAN 51.10 (2016): 781-799.
- ^ Beaumont, Paul; Evans, Neil; Huth, Michael; Planta, Tom (2015). Pernul, Günther; YA Ryan, Peter; Weippl, Edgar (eds.). "Análisis de confianza para el control de armas nucleares: abstracciones SMT de redes de creencias bayesianas" . Seguridad informática - ESORICS 2015 . Apuntes de conferencias en informática. Cham: Springer International Publishing: 521–540. doi : 10.1007 / 978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.
Referencias
- C Barrett, R Sebastiani, S Seshia y C Tinelli, " Satisfiability Modulo Theories ". En Handbook of Satisfiability, vol. 185 de Frontiers in Artificial Intelligence and Applications, (A Biere, MJH Heule, H van Maaren y T Walsh, eds.), IOS Press, febrero de 2009, págs. 825–885.
- Vijay Ganesh (Tesis doctoral 2007), Procedimientos de decisión para vectores de bits, matrices y enteros , Departamento de Ciencias de la Computación, Universidad de Stanford, Stanford, CA, EE. UU., Septiembre de 2007
- Susmit Jha, Rhishikesh Limaye y Sanjit A. Seshia. Beaver: Ingeniería de un solucionador SMT eficiente para aritmética de vectores de bits. En Actas de la 21ª Conferencia Internacional sobre Verificación Asistida por Computadora, págs. 668–674, 2009.
- RE Bryant, SM German y MN Velev, " Verificación de microprocesadores mediante procedimientos de decisión eficientes para una lógica de igualdad con funciones no interpretadas ", en Analytic Tableaux and Related Methods, págs. 1-13, 1999.
- M. Davis y H. Putnam, Un procedimiento informático para la teoría de la cuantificación , Revista de la Asociación de Maquinaria Informática, vol. 7, núm., Págs. 201–215, 1960.
- M. Davis, G. Logemann y D. Loveland, Un programa de máquina para la demostración de teoremas , Comunicaciones del ACM, vol. 5, no. 7, págs. 394–397, 1962.
- D. Kroening y O. Strichman, Procedimientos de decisión: un punto de vista algorítmico (2008), Springer (serie de informática teórica) ISBN 978-3-540-74104-6 .
- G.-J. Nam, KA Sakallah y R. Rutenbar, Un nuevo enfoque de enrutamiento detallado de FPGA a través de la satisfacción booleana basada en búsquedas , Transacciones IEEE sobre diseño asistido por computadora de circuitos y sistemas integrados, vol. 21, no. 6, págs. 674–684, 2002.
- SMT-LIB: La biblioteca de teorías del módulo de satisfacción
- SMT-COMP: el concurso de teorías de módulo de satisfacción
- Procedimientos de decisión: un punto de vista algorítmico
- R. Sebastiani, Lazy Satisfiability Modulo Theories , Dipartimento di Ingegneria e Scienza dell'Informazione, Universita di Trento, Italia, diciembre de 2007
- D.Yurichev, introducción rápida a solucionadores SAT / SMT y ejecución simbólica
Este artículo es una adaptación de una columna del boletín electrónico ACM SIGDA del Prof. Karem Sakallah . El texto original está disponible aquí