可满足性模数理论

在计算机科学和数理逻辑中，可满足性模数理论（SMT）是确定一个数学公式是否可满足的问题。它将布尔可满足性问题（SAT）概括为涉及实数、整数和/或各种数据结构（如列表、数组、位向量和字符串）的更复杂的公式。

这个名字来源于这样一个事实，即这些表达式是在一阶逻辑的某个形式化理论中以平等（通常不允许量词）来解释的（模子）。SMT求解器是旨在解决实际输入子集的SMT问题的工具。

像Z3和cvc5这样的SMT求解器已经被用作整个计算机科学中广泛的应用的构件，包括在自动定理证明、程序分析、程序验证和软件测试中。

由于布尔可满足性已经是NP-完备的，所以SMT问题通常是NP-困难的，而且对于许多理论来说，它是不可判定的。

研究人员研究哪些理论或理论的子集会导致可判定的SMT问题，以及可判定案例的计算复杂性。由此产生的决策程序常常直接在SMT求解器中实现；例如，请看Presburger算术的可解性。

SMT可以被认为是一个约束满足问题，因此是约束编程的某种形式化的方法。

从形式上讲，SMT实例是一阶逻辑中的一个公式，其中一些函数和谓词符号有额外的解释，而SMT是确定这样一个公式是否可满足的问题。

换句话说，设想一个布尔可满足性问题（SAT）的实例，其中一些二元变量被合适的非二元变量集上的谓词所取代。谓词是一个非二元变量的二元值函数。谓词的例子包括线性不等式（例如。是两个参数的一些未指定的函数）。

这些谓词根据各自分配的理论进行分类。例如，实数变量上的线性不等式使用线性实数算术理论的规则进行评估，而涉及未解释的术语和函数符号的谓词则使用未解释的平等函数理论（有时被称为空理论）的规则进行评估。

其他理论包括数组和列表结构的理论（对建模和验证计算机程序有用），以及位向量的理论（对建模和验证硬件设计有用）。子理论也是可能的：例如，差分逻辑是线性算术的一个子理论，其中每个不等式被限制为具有以下形式

一个SMT实例是布尔SAT实例的泛化，其中各种变量集被各种基础理论的谓词所取代。SMT公式提供了一个比布尔SAT公式更丰富的建模语言。

例如，SMT公式允许我们在字级而不是位级上对微处理器的数据通路操作进行建模。相比之下，答案集编程也是基于谓词（更确切地说，是基于由原子公式创建的原子句）。

与SMT不同，答案集程序没有量词，不能轻易地表达诸如线性算术或差分逻辑等约束条件--ASP最多适合于还原为未解释函数的自由理论的布尔问题。

在ASP中把32位整数作为位向量来实现，会受到早期SMT求解器所面临的大多数问题的影响：诸如x+y=y+x这样明显的相同点是很难推导出来的。

约束逻辑编程确实提供了对线性算术约束的支持，但是在一个完全不同的理论框架内。SMT求解器也被扩展到解决高阶逻辑的公式。

早期解决SMT实例的尝试是将它们转化为布尔SAT实例（例如，一个32位的整数变量将由32个具有适当权重的单位变量来编码，字级操作如"加"将由位上的低级逻辑操作来代替），并将这个公式传递给布尔SAT解算器。