叠加与模型演化结合及DPLL(Γ+T)可满足性判定方法

### 叠加与模型演化结合及DPLL(Γ + T )可满足性判定方法 #### 1. 叠加与模型演化结合相关概念 在逻辑推理的领域中，有一些重要的概念和定理对于解决问题起着关键作用。首先是关于极限树和分支的定义。 - **耗尽分支（Exhausted Branch）**：设 $T$ 为极限树，$B = (N_i)_{i<\kappa}$ 是 $T$ 中具有 $\kappa$ 个节点的分支。对于所有 $i < \kappa$，设 $\Lambda_i \vdash \Phi_i$ 是标记节点 $N_i$ 的相继式。分支 $B$ 是耗尽的，当且仅当： - 对于所有 $i < \kappa$，每个以 $\Lambda_i \vdash \Phi_i$ 为前提、具有持久选定子句和持久左前提（在推导情况下）的 $\iota_{ME+Sup}$ 推理，相对于某个 $j < \kappa$ 且 $j \geq i$ 的 $\Lambda_j \vdash \Phi_j$ 是普遍冗余的。 - $\square \cdot \emptyset \notin \Phi_B$。 - **公平极限树与公平推导**：推导的极限树是公平的，当且仅当它是一个反驳树（即所有叶子在相继式的约束子句部分都包含 $\square \cdot \emptyset$ 的有限树），或者它有一个耗尽分支。推导是公平的，当且仅当其极限树是公平的。 这里有一个重要的性质：如果在上述定义的条件（i）中，选定子句或左前提（在推导情况下）相对于 $\Lambda_i \vdash \Phi_i$ 是普遍冗余的，那么 $\iota_{ME+Sup}$ 推理相对于 $\Lambda_i \vdash \Phi_i$ 已经是冗余的。也就是说，具有普遍冗余前提的推理不需要进行。 下面是相关的命题和定理： |命题/定理|内容| | ---- | ---- | |命题 9.2|如果 $B$ 是公平推导的极限树的耗尽分支，那么 $\Lambda_B \vdash \Phi_B$ 是饱和的。| |定理 9.3|设 $\Psi$ 是子句集，$T$ 是 $\Psi$ 的公平推导的极限树。如果 $T$ 不是反驳树，那么 $\Psi$ 是可满足的；更具体地说，对于 $T$ 的每个耗尽分支 $B$，其极限相继式为 $\Lambda_B \vdash \Phi_B$，诱导重写系统为 $R_B = R_{\Lambda_B \vdash \Phi_B}$，有 $\Lambda_B, R_B \models (\Phi_B)_{\Lambda_B}$ 且 $R_B^{\star} \models \Psi$。| 此外，$ME+Sup$ 演算也是可靠的。其可靠性证明的思路是在概念上把所有上下文中每个文字中的每个变量用一个常量（例如 $a$）替换。这样会得到一个反驳树，其中所有分裂都是关于互补命题文字的。对于关闭推理，任何关闭子句在以相同方式实例化其所有变量后仍然是关闭的。而且，$Ref$、$Sup - Neg$、$Sup - Pos$ 和 $Fact$ 推理规则在标准意义上是可靠的，通过考虑前提和结论的子句形式可以看出。对于其余的 $\iota_{Base}$ 推理规则 $U - Sup - Pos$、$U - Sup - Neg$ 和 $Neg - U - Res$ 更是如此，因为结论中的约束包含左前提（它们是强可靠的）。$Simp$ 的可靠性从其条件（ii）得出。通过这种方式，每当存在反驳时，可以识别出一组基实例，证明输入子句集的不可满足性。 #### 2. DPLL(Γ + T )可满足性判定背景 在软件验证的应用中，常常需要确定一阶公式相对于某些背景理论的可满足性。许多验证问题可以归结为确定一组公式 $R \uplus P$ 相对于背景理论 $T$ 的可满足性，其中 $R$ 是不包含 $T$ 符号的非基子句集，$P$ 是可能包含 $T$ 符号的大基公式（或基子句集）。$R$ 可以看作是特定应用理论的公理化，而背景理论 $T$ 是硬件和软件验证中常用的通用理论的组合，如线性算术和位向量。 目前有两种主要的推理方法： |方法|特点| | ---- | ---- | |可满足性模理论（SMT）求解器|高度可扩展、高效，适合集成理论推理。大多数 SMT 求解器限于基公式，将 Davis - Putnam - Logemann - Loveland 过程（DPLL）与用于特殊理论 $T_i$ 基可满足性问题的卫星 $T_i$ 求解器集成，使得 $T = \bigcup_{i = 1}^{n} T_i$。| |基于叠加的推理系统（SP）|擅长处理等式、全称量化变量和 Horn 子句。并且，SP 已被证明对于几种数据结构理论可以终止，因此是可满足性判定过程。| $DPLL(\Gamma + T )$ 演算将 SMT 求解器与对于带等式的一阶逻辑是可靠且反驳完全的推理系统 $\Gamma$ 集成。然而，当 $T$ 不为空时，$DPLL(\Gamma + T )$ 演算通常不是反驳完全的。例如，假设 $R = \{x = a \vee x = b\}$，$P = \emptyset$，背景理论 $T$ 是算术。子句 $\{x = a \vee x = b\}$ 意味着任何模型最多有两个元素，这显然与算术的任何模型不兼容。 #### 3. DPLL(Γ + T )中的变量不活动性 在 $DPLL(\Gamma + T )$ 中，需要将内置理论 $T$ 和公理化理论 $R$ 结合起来。之前从基于重写的可满足性判定方法中得到的结果可以应用到 $DPLL(\Gamma + T )$ 框架中。 - **变量不活动子句和理论**： - **变量不活动子句**：子句 $C$ 是变量不活动的，如果 $C$ 中没有最大文字是等式 $t \simeq x$ 且 $x \notin Var(t)$。一组子句是变量不活动的，如果其所有子句都是变量不活动的。 - **变量不活动理论**：理论表示 $R$ 对于推理系统 $\Gamma$ 是变量不活动的，如果从 $S_0 = R \uplus S$（$S$ 是一组基单位 $R$ 子句）的公平 $\Gamma$ 推导的极限 $S_{\infty}$ 是变量不活动的。 变量不活动性有重要的性质：如果 $R$ 是变量不活动的，那么它是稳定无限的。这意味着在 $DPLL(\Gamma + T )$ 中，对于 $R$ 的稳定无限性，可以通过检测变量不活动子句（即基数约束）的生成来判断。在新的 $Z3(SP)$ 版本中，$SP$ 引擎配备了这样的测试，以发现 $R$ 是否不是稳定无限的。 在 $DPLL(\Gamma + T )$ 应用于 $R \uplus P$ 模 $T$ 的问题时，$\Gamma$ 只处理非基子句和基单位子句。因此，将基于重写方法的结果应用于作为 $R$ 求解器的 $\Gamma$ 是合理的。$DPLL(\Gamma + T )$ 需要在 Nelson - Oppen 方案中结合 $T_1, \ldots, T_n$ 和 $R$，这要求理论不共享函数符号、是稳定无限的，并且每个求解器能生成所有蕴含的常量之间的等式（析取）。 对于地面子句可能包含 $T$ 符号以及 $R$ 可能引入除等式之外的谓词符号的问题，有相应的处理方法： - **处理 $T$ 符号**：通过纯化，这是 Nelson - Oppen 方法中的标准步骤，通过引入新的常量符号来分离不同签名的函数符号的出现。例如，$f(g(a)) \simeq b$（其中 $f$ 和 $g$ 属于不同签名）变为 $f(c) \simeq b \wedge g(a) \simeq c$（$c$ 是新的）。初始的基子句集 $P$ 被转换为两个不相交的集合 $P_1$ 和 $P_2$，其中 $P_1$ 只包含 $R$ 符号，$P_2$ 只包含 $T$ 符号。 - **处理其他谓词符号**：将 $R$ 原子 $p(t_1, \ldots, t_n)$ 表示为 $f_p(t_1, \ldots, t_n) = \top$，其中 $f_p$ 是新的函数符号，$\top$ 是特殊常量。 下面是一个简单的流程图，展示了变量不活动性在 $DPLL(\Ga