可满足模理论

正式地来讲，一个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问题扩展到非线性理论，例如确定

其中

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

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

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

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

SMT求解器对于验证、证明程序的正确性、基于符号执行的软件测试以及通过搜索可能的程序空间合成和生成程序片段都很有用。

6.1 验证

计算机辅助的计算机程序的验证经常使用SMT求解器。一种常见的技术是将先验条件、后验条件、循环条件和断言转换成SMT公式，以确定是否所有属性都可以成立。

有许多验证器是建立在Z3SMT求解器上的。Boogie是一种中间验证语言，使用Z3自动检查简单的命令程序。并发C的VCC验证器使用了Boogie，以及对于强制性的基于对象的程序使用了Dafny，对于并发程序使用了Chalice，以及对于C#使用了Spec#。F*是一种依赖类型的语言，使用Z3来查找证据；编译器通过这些证明以产生携带证据的字节码。Viper verification in frastructure将验证条件编码为Z3。sbv库提供基于SMT的Haskell程序验证，并允许用户在许多求解器例如Z3、ABC、Boolector、CVC4、MathSAT和Yices中进行选择。

此外，还有许多建立在Alt-ErgoSMT求解器以上的验证器。以下是成熟应用程序的列表:

• Why3，演绎程序的验证平台，使用了Alt-Ergo作为它的主要证明器；
• CAVEAT，一个由CEA开发并由Airbus使用的验证器；Alt-Ergo被列入其最近的一架飞机的DO-178C鉴定中；
• Frama-C，一个分析C代码的框架，在Jessie和WP插件中使用了Alt-Ergo(专用于“演绎程序验证”)；
• SPARK，使用CVC4和Alt-Ergo(在GNATprove后面)来自动验证SPARK2014中的一些断言；
• Atelier-B可以使用Alt-Ergo代替它的主证明器(在ANR Bware project benchmarks上的成功率从84%增加到了98%)；
• Rodin，由Systerel开发的B方法框架，可以使用Alt-Ergo作为后端；
• Cubicle，用于验证基于阵列的转换系统的安全属性的开源模型检查器。
• EasyCrypt，一个用于推理带有对抗性代码的概率计算的关系属性的工具集。

许多SMT求解器实现了一种称为SMTLIB2的通用接口格式(此类文件通常具有“.smt2”扩展名)。LiquidHaskell 工具为Haskell实现了一个基于改良类型的验证器，该验证器可以使用任何符合SMTLIB2的求解器，例如CVC4、MathSat或Z3。

6.2 基于符号执行的分析和测试

SMT求解器的一个重要应用是对于程序的分析和测试(例如concolic测试)的符号执行，尤其注重发现安全漏洞。这一类别中重要的主动维护工具包括微软研究院的SAGE，KLEE，S2E，和Triton。对符号执行应用特别有用的SMT求解器包括Z3，STP，Z3str2，和Boolector。