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.