基本术语

正式地来讲，一个SMT实例是在一阶逻辑中的一个公式，其中一些函数和谓词符号具有另外的解释，并且SMT是确定这样的公式是否是可满足的问题。换句话说，想象一个布尔可满足性问题，在一组合适的非二元变量上一些二元变量被替换为谓词。谓词是非二元变量的二元值函数。示例谓词包括线性不等式(例如， )或涉及到未解释术语和函数符号的等式(例如， 其中 是两个参数的某种未指定的函数)。这些谓词根据各自分配的理论进行分类。例如，实变量上的线性不等式是用线性实数演算理论的规则来评估的，而涉及未解释术语和函数符号的谓词是使用带有等式的未解释函数的理论(有时被称为空理论)。其他理论包括数组和列表结构的理论(用于建模和验证计算机程序)，和位向量理论(用于建模和验证硬件设计)。子理论也是可能的：例如，逻辑差是线性演算的子理论，其中对于变量 和 和常数 ，每个不等式被限制为具有以下形式 。

大多数SMT求解器仅支持它们逻辑中的无量词片段。

表达能力

SMT实例是布尔SAT实例的一个泛化形式，在布尔SAT中各种变量集被替换为来自各种潜在的理论的谓词。SMT公式提供了比布尔SAT公式更丰富的模型化语言。例如，SMT公式允许我们对微处理器的数据路径的操作在字级而不是位级进行建模。

相比之下，回答集编程也是基于谓词的(更准确地说，基于创建自原子公式的原子语句)。与SMT不同，回答集程序没有量词，也不容易表达约束条件，例如线性演算或者逻辑差—ASP最适合于布尔问题，这些问题可以简化为未解释函数的自由理论。在ASP中实现32位整数作为位向量遇到了与大多数早期SMT求解器面临的相同的问题:“明显的”恒等式，例如x+y=y+x很难推断。

约束逻辑编程虽然支持线性演算约束，但其是在完全不同的理论框架内。

求解器方法

早期解决SMT实例的尝试包括将它们转换成布尔SAT实例(例如，32位整数变量将由具有适当权重的32位变量编码，并且诸如“加号”的字级操作将被位上的低级逻辑操作代替)，并将该公式传递给布尔SAT求解器。这种方法被称为惰性方法，它的优点是：通过将SMT公式预处理成等效的布尔SAT公式，我们可以使用现有的“原样”布尔SAT求解器，并利用它们随着时间的推移而提高的性能和容量这一特征。另一方面，底层理论的高级语义的丧失意味着布尔SAT求解器为了找到“明显”的事实不得不进行超出必要的工作。(例如 整数加法。)这一观测带动了许多SMT求解器的发展，这些求解器将DPLL-风格搜索的布尔推理与理论的求解器（T-solvers）紧密集成，这些求解器能处理来自给定理论中的谓词的连词（ANDs）。这种方法被称为惰性方法。

被称为DPLL的体系结构将布尔推理的职责交给了基于DPLL的SAT求解器，该求解器通过一个定义明确的接口与理论T的求解器交互。理论求解器在探索公式的布尔搜索空间时，只需要担心检查从SAT求解器传递给它的理论谓词的连词的可行性。然而，为了使这种集成能良好工作，理论求解器必须能够参与传播和冲突分析，例如，它必须能够从已经建立的事实中推断出新的事实，并且能够在理论冲突出现时提供不可行性的简洁解释。换句话说，理论求解器必须是增量的，并且可回溯的。

不确定理论的SMT

大多数常见的SMT方法都支持可判定理论。然而，许多现实世界的系统只能通过非线性算法对实数进行建模，其中包括超越函数，例如飞机及其行为。这一事实促使SMT问题扩展到非线性理论，例如确定

其中

是否是可以满足的。然后，在多数情况下这样的问题就变成了不可判定的。(然而，需要注意的是实封闭域和实数的一阶完全理论使用量词消去的话是可判定的。这个要归功于AlfredTarski。)带有加法的自然数的一阶理论(但不包括乘法)称为Presburger算法，也是可以判定的。由于常数乘法可以被实现为嵌套加法，所以许多计算机程序中的算法可以用Presburger算法来表示，从而得到可判定的公式。

SMT求解器中可以从实数上的不可判定算术理论中解决理论原子布尔组合的例子有ABsolver，它采用经典的DPLL(T)体系结构和非线性优化包作为(必然不完整的)从属理论求解器，以及另一个例子iSAT，建立在DPLL SAT求解和区间约束传播的统一上，称为iSAT算法。

求解器

下表总结了许多可用的SMT求解器的一些功能。“SMT-LIB”列表示与SMT-LIB语言兼容；许多标有“是”的系统可能只支持SMT-LIB的旧版本，或者只提供对该语言的部分支持。“CVC”一栏表示支持CVC语言。“DIMACS”列表示支持DIMACS格式。

这些项目不仅在特性和性能上不同，在周边社区的耐用性、项目本身的热门程度以及贡献文档、修复、测试和增强的能力上也不同。