组合理论的判定
1. 简介
之前我们一直讨论的是关于特定理论的判定过程, 比如命题逻辑, 等式逻辑, 量化公式等. 但在实践中, 多数情况是几种理论的组合, 所以要讨论关于组合理论的判定过程. 我们主要介绍熟知的Nelson-Oppen组合方法. 该方法假设我们对每种涉及的理论都有一个判定过程. Nelson-Oppen组合方法允许判定过程彼此通信, 以确保组合理论可靠且完备的判定过程.
首先说明几个组合理论中的重要概念.
组合理论(theory combination): 分别给出符合签名(signature) \(\Sigma_1,\Sigma_2\)的两个理论 \(T_1,T_2\). 组合理论 \(T_1\oplus T_2\) 是定义在公理集合 \(T_1 \cup T_2\) 上的 \((\Sigma_1\cup\Sigma_2)\)-理论.
组合理论问题(the theory combination problem): 令 \(\varphi\) 是定义在签名 \(\Sigma_1\cup\Sigma_2\) 上的组合理论公式. 组合理论问题是判定组合理论 \(T_1\oplus T_2\) 的有效性. 等价地, 这类问题是判断下式是否成立: \[ T_1\oplus T_2 \models \varphi. \] 尽管理论 \(T_1,T_2\) 它们自身是可判定的, 但是它们的组合理论未必是可判定的. 在一些特定的限制下, 组合理论就会是可判定的. 其中很重要的一个限制是, 所涉及的理论是凸理论(convex theory).
凸理论: \(\Sigma\)-理论 \(T\) 是凸理论, 如果对于 \(\Sigma\)-公式 \(\varphi\) 中的所有合取式公式都有 \[ \begin{aligned} &(\varphi\Longrightarrow \bigvee_{i=1}^nx_i=y_i)\ is\ T-valid\ for\ some\ finite\ n\gt1\Longrightarrow\\ &(\varphi\Longrightarrow x_i=y_i)\ is\ T-valid\ for\ some\ i\in\{1,...,n\} \end{aligned} \] 其中, \(x_i,y_i\) 为变量.
换句话说, 在一个凸理论 \(T\) 中, 如果一个公式 \(T-\)蕴含 等式的析取, 那么它也分别 \(T-\)蕴含这些等式中的至少一项.
一下用两个例子来说明凸理论和非凸理论.
在实数集 \(\mathbb{R}\) 上的线性演算是凸的. 线性算术谓词的合取定义了一组值, 这些值可以为空, 单例, 如 \[ x\le 3\land x\ge 3\Longrightarrow x=3, \] 或无限大, 因此它意味着无限的析取. 在所有三种情况下, 它都符合凸理论的定义.
在整数集 \(\mathbb{Z}\) 上的线性演算是非凸的. 比如说, 当如下式子成立时 \[ x_1=1\land x_2=2\land 1\le x_3\land x_3\le2\Longrightarrow (x_3=x_1\lor x_3=x_2). \] 以下两个式子都不成立: \[ \begin{align*} x_1=1\land x_2=2\land 1\le x_3\land x_3\le2\Longrightarrow x_3=x_1.\\ x_1=1\land x_2=2\land 1\le x_3\land x_3\le2\Longrightarrow x_3=x_2. \end{align*} \]
2. Nelson-Oppen 组合过程
Nelson-Oppen组合过程为符合某些规定的理论提供了解决理论组合问题的方法. 组合过程可以分为凸理论组合和非凸理论的组合.
2.1 凸理论组合
Nelson-Oppen 约束(Nelson-Oppen restrictions). 为了能够应用Nelson-Oppen过程, 理论 \(T_1,...,T_n\) 需要满足如下约束:
- \(T_1,...,T_n\) 是具有等式的无量词一阶理论.
- 每一个理论 \(T_1,...,T_n\) 都有自己的判定过程.
- 签名是不相交的, 也即, 对于所有的 \(1\le i\lt j\le n\), \(\Sigma_i\cap \Sigma_j=\emptyset\).
- \(T_1,...,T_n\) 是解释在无穷域上的理论, 例如, 定义在实数集 \(\mathbb{R}\) 上的线性演算, 有限长度的位向量理论就不符合要求.
如下所示的算法1 是组合凸理论的Nelson-Oppen过程. 算法接收一个公式 \(\varphi\) 作为输入, 该公式必须是文字的合取式. 通常来说, 向一个凸理论中添加析取式子会导致其成为非凸理论. 具有析取关系的凸理论的扩展可以由我们稍后将介绍的非凸理论的扩展来支持, 或者也可以通过无量词理论章节中介绍的方法来提供支持, 这是基于将理论的判定过程与SAT求解器组合在一起.
\[ \begin{align*} &\mathbf{Algorithm\;1:}\; \text{NELSON-OPPEN-FOR-CONVEX-THEORIES}\\ \\ &\mathbf{Input:}\; \text{A convex formula }\varphi\;\text{that mixes convex theories, with}\\ &\quad\quad\quad\quad\text{restrictions as specified in Nelson-Oppen restrictions}\\ &\mathbf{Output:}\; \text{``Satisfiable'' if }\varphi\;\text{is satisfiable, and ''Unsatisfiable'' otherwise}\\ \\ &\;1.\; \it{Purification:}\;\text{Purify }\varphi\;\text{into }F_1,...,F_n.\\ &\;2.\; \text{Apply the decision procedure for }T_i\;\text{to }F_i.\; \text{If there exists }i\;\text{such that}\\ &\quad\; F_i\;\text{is unsatisfiable in }T_i,\;\text{return ''Unsatisfiable''.}\\ &\;3.\; \it{Equality\ propagation:}\;\text{If there exist }i,j\;\text{such that }F_i\;T_i\mbox{-}\text{implies an equality}\\ &\quad\; \text{between variables of }\varphi\;\text{that is not }T_j\mbox{-}\text{implied by }F_j,\; \text{add this equality to }\\ &\quad\; F_j\;\text{and go to step 2}.\\ &\;4.\; \text{Return ''Satisfiable''}. \end{align*} \]
算法1 的第一步依赖于纯化(purification)的思想. 纯化是公式的保持可满足性的一种转化, 此后每个原子都来自特定的理论. 在这种情况下, 我们说所有原子都是纯净(pure)的. 更具体地讲, 给定一个公式 \(\varphi\), 纯化产生如下等价的可满足公式 \(\varphi'\):
令 \(\varphi'=\varphi\).
对于 \(\varphi'\) 中的每一个子表达式 \(\phi\):
用新的辅助变量 \(a_{\phi}\) 替换 \(\phi\)
用 \(a_{\phi}=\phi\) 对 \(\varphi'\) 进行约束.
例子1, 给定一个混合了线性演算和未解释函数的公式 \[ \varphi:=x_1\le f(x_1), \] 纯化的结果为 \[ \varphi':=x_1\le a\land a=f(x_1). \] 公式 \(\varphi'\) 中的所有原子都是纯的: \(x_1\le a\) 是一个线性演算的式子, \(a=f(x_1)\) 属于具有未解释函数的等式理论.
纯化之后, 剩下一组纯表达式 \(F_1,...,F_n\):
- 所有的 \(i\), \(F_i\) 属于理论 \(T_i\), 且是 \(T_i\)-文字的合取式.
- 允许共享变量, 比如说, 存在 \(i,j,1\le i\lt j\le n, var(F_i)\cap var(F_j)\ne\emptyset\).
- 当且仅当 \(\bigwedge_{i=1}^nF_i\) 在组合理论中是可满足的时候, 组合理论中的公式 \(\varphi\) 是可满足的.
例子2, 给定如下混合线性演算和未解释函数的式子 \[ (f(x_1,0)\ge x_3)\land (f(x_2,0)\le x_3)\land\\ (x_1\ge x_2)\land (x_2\ge x_1)\land\\ (x_3-f(x_1,0)\ge 1), \] 纯化之后得到公式 \[ \begin{aligned} &(a_1\ge x_3)\land(a_2\le x_3)\land(x_1\ge x_2)\land (x_2\ge x_1)\land (x_3-a_1\ge 1)\land\\ &(a_0=0)\land\\ &(a_1=f(x_1,a_0))\land\\ &(a_2=f(x_2,a_0)). \end{aligned}\tag{1} \] 如下表所示, 我们可以得到基于上面公式的判定过程:
表1.
| \(F_1(\mathbb{R}\ 上的线性演算)\) | \(F_2(\rm EUF)\) |
|---|---|
| \(a_1\ge
x_3\) \(a_2\le x_3\) \(x_1\ge x_2\) \(x_2\ge x_1\) \(x_3-a_1\ge 1\) \(a_0=0\) |
\(a_1=f(x_1,a_0)\) \(a_2=f(x_2,a_0)\) |
| \(\star\
x_1=x_2\) \(\ \ a_1=a_2\) \(\star a_1=x_3\) \(\star\ \rm FALSE\) |
\(x_1=x_2\) \(\star\ a_1=a_2\) |
表1 显示了将公式(1)分为了两个纯公式 \(F_1\) 和 \(F_2\). 第一个公式是一个线性演算式子, 第二个公式是一个具有未解释函数的等式理论公式(EUF). \(F_1\) 和 \(F_2\) 都不是独立矛盾的, 因此, 我们继续执行算法步骤3. 通过对实数进行线性算术的判定过程, 我们从\(F_1\) 推断出 \(x_1 = x_2\), 并将这一事实传播到另一个理论(即, 我们添加此等式至 \(F_2\)). 现在我们可以推导 \(T_2\) 中的 \(a_1 = a_2\) , 并将该等式传播到 \(F_1\). 从这个等式中, 我们得出 \(T1\) 中的 \(a_1 = x_3\), 这与 \(T_1\)中的 \(x_3-a_1\ge 1\) 矛盾. 所以原公式为假.
2.2 非凸理论组合
接下来讨论非凸理论的组合(或者凸理论和非凸理论的组合). 首先, 考虑如下的例子, 该例表明了在凸理论组合算法处理的公式中如果其中有理论不是凸的, 可能导致算法失效: \[ (1\le x)\land (x\le 2)\land p(x)\land \neg p(1)\land \neg p(2),\tag{2} \] 其中 \(x\in \mathbb{Z}\). 上述表达式混合了整数的线性演算和未解释函数谓词. 正如前面所描述的, 针对整数的线性演算不是凸的. 纯化之后的结果得到 \[ \begin{aligned} &1\le x\land x\le 2\land p(x)\land \neg p(a_1)\land\neg p(a_2)\land\\ &a_1=1\land\\ &a_2=2 \end{aligned} \] 下表展示了上面非凸理论公式谓词分为两个纯公式 \(F_1\) 和 \(F_2\). 应当注意到 \(F_1\) 和 \(F_2\) 各自都是可满足的, 但是在各自的理论中不能推出任何等式. 因此, 尽管该凸理论原公式是不可满足的, 凸理论组合算法仍然返回的是 "Satisfiable".
该判定过程中所存在的问题, 不仅仅要关注蕴含等式, 还要注意蕴含等式的析取. 回想一下, 变量是有限的, 因此存在相等性和相等性的析取关系, 这意味着计算这些含义是可行的. 给定这样的析取关系, 将问题分解为与析取关系一样多的部分, 然后以递归方式调用该过程. 以公式(2) 的例子来说, \(F_1\) 能够蕴含 \(x=1\lor x=2\). 因此, 我们可以把问题一分为二, 分别考虑 \(x=1\) 和 \(x=2\) 的情况. 算法2 在算法1 中添加了一个步骤: 该步骤就是实现该分割的.
\[ \begin{align*} &\mathbf{Algorithm\;2:}\; \text{NELSON-OPPEN}\\ \\ &\mathbf{Input:}\;\;\; \text{A formula }\varphi\;\text{that mixes theories, with restrictions as specified}\\ &\quad\quad\quad\quad\text{in Nelson-Oppen restrictions}\\ &\mathbf{Output:}\; \text{''Satisfiable'' if }\varphi\;\text{is satisfiable, and ''Unsatisfiable'' otherwise}\\ \\ &\;1.\; \it{Purification:}\;\text{Purify }\varphi\;\text{into }\varphi'=F_1,...,F_n.\\ &\;2.\; \text{Apply the decision procedure for }T_i\;\text{to }F_i.\; \text{If there exists }i\;\text{such that}\\ &\quad\; F_i\;\text{is unsatisfiable},\;\text{return ``Unsatisfiable''.}\\ &\;3.\; \it{Equality\ propagation:}\;\text{If there exist }i,j\;\text{such that }F_i\;T_i\mbox{-}\text{implies an equality}\\ &\quad\; \text{between variables of }\varphi\;\text{that is not }T_j\mbox{-}\text{implied by }F_j,\; \text{add this equality to }\\ &\quad\; F_j\;\text{and go to step 2}.\\ &\;4.\; \it{Splitting:}\;\text{If there exists }i\;\text{such that}\\ &\quad\;\; \bullet \quad\quad F_i\Longrightarrow(x_1=y_1\vee \cdots\vee x_k=y_k)\;\text{and}\\ &\quad\;\; \bullet \quad\quad \forall j\in\{1,...,k\}.\; F_i\nRightarrow x_j=y_j,\\ &\quad\;\; \text{then apply NELSON-OPPEN recursively to}\\ &\hspace{50mm} \varphi'\wedge x_1=y_1,...,\varphi'\wedge x_k=y_k.\\ &\quad\;\; \text{If and of these subproblems is satisfiable, return ''Satisfiable''. Otherwise,}\\ &\quad\;\; \text{return ''Unsatisfiable''}.\\ &\;5.\; \text{Return ''Satisfiable''}. \end{align*} \]
例子3, 继续考虑公式(2.1). 算法2 从 \(F_1\) 中推出 \(x=1\lor x=2\), 并将该问题分为两个子问题, 如下面两个表所示.
表2. \(x=a_1\) 的情况
| \(F_1(整数集上的线性运算)\) | \(F_2(\rm EUF)\) |
|---|---|
| \(1\le
x\) \(x\le 2\) \(a_1=1\) \(a_2=2\) |
\(p(x)\) \(\neg p(a_1)\) \(\neg p(a_2)\) |
| \(x=1\) \(\star\ x=a_1\) |
\(x=a_1\) \(\rm FALSE\) |
表3. \(x=a_2\) 的情况
| \(F_1(整数集上的线性运算)\) | \(F_2(\rm EUF)\) |
|---|---|
| \(1\le
x\) \(x\le 2\) \(a_1=1\) \(a_2=2\) |
\(p(x)\) \(\neg p(a_1)\) \(\neg p(a_2)\) |
| \(x=2\) \(\star\ x=a_2\) |
\(x=a_2\) \(\rm FALSE\) |
由此, 因为两个子问题为假, 所以原问题不可满足.