O problema da satisfatibilidade booleana (SAT), no qual busca-se determinar se existe uma atribuição de valores a variáveis que torna verdadeira uma dada formula em logica proposicional, é crucial para a ciência da computação, pois foi o primeiro a ser mostrado NP-completo, por Stephen A. Cook e, de forma independente, Leonid A. Levin. Essa conclusão implica que qualquer problema que pertence à classe NP – que inclui uma serie de problemas relevantes, como o numero cromatico de um grafo, o problema do caixeiro viajante e o problema da mochila – pode ser reduzido a ele. Ainda mais, essa importância extrapola a teoria: os diversos avanços em resolvedores SAT nos últimos 25 anos ocasionaram um grande interesse por parte de áreas como teoria dos grafos, projeto de hardware, verificação formal e pesquisa operacional em converter, total ou parcialmente, certos problemas em problemas de satisfatibilidade.
A aplicação de logica proposicional é, contudo, em muitos contextos, insuficiente, pois é incapaz de expressar propriedades de objetos ou relações entre eles. Para isso, pode ser utilizada a logica de primeira ordem (bem como as de ordem superior), em que são adicionados predicados, funções e quantificadores. Nesse sentido, diversas aplicações requerem a habilidade de raciocinar a respeito de alguma teoria, que fixa a interpretação de certos predicados e funções. Alguns exemplos de teorias bem estabelecidas são as de aritmetica linear, strings, arrays e bit-vectors – ou ate mesmo combinações delas. Em geral, resolvedores que checam a satisfatibilidade de formulas com respeito a uma teoria implementam procedimentos de decisão específicos para essa teoria acerca da validade de certos modelos construídos de forma independente a partir da formula. Em outras palavras, os módulos referentes a cada teoria são independentes do fluxo principal do resolvedor e podem ser instanciados a depender do problema que sera resolvido. A esses resolvedores, damos o nome resolvedores SMT e, ao campo de estudo que abrange essa classe de problemas, satisfatibilidade modulo teorias (SMT).