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.
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.
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).
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