首先，SAT（Satisfiability）问题讨论命题逻辑公式的可满足性。即给定一个命题逻辑公式（一般是CNF形式），回答该公式是否存在一组可满足的赋值（一般称为model）。倘若存在，一般还需要构造出这一组赋值。对于SAT问题，已有较为高效的算法（比如DPLL）来进行求解。
很明显，命题逻辑的描述能力有限，远不如谓词逻辑（一阶逻辑）。那么，我们可以将可满足性问题扩展到谓词逻辑上。然而，这样的扩展过于宽泛，以至于难以提出有效的算法来对该问题进行求解。于是，我们需要将可满足性问题研究的对象再适当收缩一下。例如，将讨论的谓词逻辑公式限制在某一（或者某些）背景理论下（Theories）。即仅允许公式中出现这些背景理论下定义的谓词和函数。于是，SMT（Satisfiability Modulo Theories）便出现了。
在背景理论的限制下，我们可以针对不同的理论，提出各种有效的理论公式求解算法。例如，对于等式和未解释函数理论（EUF），可以通过构造等价类来进行求解（算法是并查集hah）；再比如线性实数运算理论（LRA），也有一套自己的求解算法。SMT将各种理论公式求解算法融合起来，从而实现一个有效的SMT求解算法（一般为DPLL(T)）。具体的算法可以参考任意介绍SMT的课程讲义。[DPLL 算法 ，全称为 Davis-Putnam-Logemann-Loveland（戴维斯-普特南-洛吉曼-洛夫兰德）算法，是一种完备的，基于 回溯 （backtracking）的搜索算法，用于判定命题逻辑公式（为合取范式形式）的 可满足性 ，也就是求解 SAT（布尔可满足性问题）的一种（或者一类）算法]
最后，个人认为，在SMT这个名词中，最容易让人困惑的当属Modulo一词。它是取模的意思（还是不知所云hah）。目前，国内学术界对SMT一致认可的中文翻译为可满足性模理论（有中文翻译也同样不知所云hah）。我尝试按照以下的描述来解释一下，之前所介绍的这一套方法，为何被称为SMT。对于取模，大家最熟悉的应该是编程语言中整数的取模运算（10 % 3 == 1）。取模运算有一个特点，以正整数为例，不管多大的正整数，在对另一个正整数进行取模运算后，得到的值都在这个模数（所模的那个数）的范围内。类比于此，就可以好好理解SMT中的Modulo了。所谓SMT就是，将一个范围很大（一阶逻辑）的可满足性问题（Satisfiability，类比很大的正整数），对某一个或多个理论（Theories，类比模数）取模（Modulo，类比取模运算）。得到的结果当然是在这些理论范围内的可满足性问题。（这也正是我们之前所介绍的内容）
综上，SMT就是将逻辑公式限制在某些理论下来判定其可满足性的问题。