DPLL(Γ+T)在可满足性判定中的应用与理论分析

### DPLL(Γ + T )在可满足性判定中的应用与理论分析 #### 1. DPLL(Γ + T )中的冲突检测与处理 在DPLL(Γ + T )的过程中，会出现冲突检测与处理的情况。例如，在线性算术求解器维护的模型model(M)中，若model(M)(b1) = model(M)(b2)，PropagateEq会猜测方程b1 ≃ b2。假设b2 ≻ b1，简化操作会将b2 ⊑ c重写为b1 ⊑ c，通过超消解（Hyperresolution）从a ⊑ b1、b1 ⊑ c和传递性可推出a ⊑ c，从而检测到不一致性。此时，DPLL(Γ + T )会回溯并将¬(b1 ≃ b2)添加到M中，T - Conflict会检测到该文字与{b1 ≤ b2, b1 > b2 - 1}之间的不一致性，再次应用冲突解决规则后会产生空子句。 #### 2. 本质有限理论 - **定义**： - 若对于所有的结构Φ，当Φ关于函数符号f的范围（range(Φ(f))）是有限的时，称结构Φ关于函数符号f是本质有限的。本质有限性比有限性稍弱，因为它允许域是无限的，只要函数的范围是有限的。 - 对于理论R，有以下两个重要性质： - **有限模型性质**：对于所有的基础R - 子句集P，若R ⊎ P是可满足的，则R ⊎ P有一个模型Φ，且|Φ|是有限的。 - **本质有限性**：设R的签名包含一个单目函数符号f，对于所有的基础R - 子句集P，若R ⊎ P是可满足的，则R ⊎ P有一个模型Φ，使得range(Φ(f))是有限的。 - **定理3**：若Φ是关于单目函数符号f的本质有限结构，则存在k1, k2（k1 ≠ k2），使得Φ |= f k1(x) ≃ f k2(x)。 - **证明思路**：对于任意v ∈ |Φ|，定义从v开始的f - 链为v = Φ(f)0(v), Φ(f)1(v), Φ(f)2(v), ...。由于Φ(f)的范围有限，存在q1, q2（q1 ≠ q2）使得Φ(f)q1(v) = Φ(f)q2(v)。定义f - 链的大小sz(Φ, f, v)和前缀pr(Φ, f, v)分别为满足Φ(f)q1(v) = Φ(f)q2(v)且q1 > q2的最小q1和q2，套索ls(Φ, f, v)为sz(Φ, f, v) - pr(Φ, f, v)。当n ≥ pr(Φ, f, v)时，称Φ(f)n(v)在f - 链的套索中。对于套索中的元素u，当m = ls(Φ, f, v)时，Φ(f)m(u) = u；对于套索的所有倍数l = h · ls(Φ, f, v)（h > 0），Φ(f)l(u) = u。设p = max{pr(Φ, f, v) | v ∈ range(Φ(f))} + 1，l = lcm{ls(Φ, f, v) | v ∈ range(Φ(f))}，通过反证法可证明Φ |= f p + l(x) ≃ f p(x)，即k1 = p + l，k2 = p。 - **示例3**：设Φ是一个结构，|Φ| = {v0, v1, v2, ..., v9, ...}，Φ(f)由映射{v0 → v1, v1 → v2, v2 → v3, v3 → v4, v4 → v2, v5 → v6, v6 → v7, v7 → v8, v8 → v5, * → v9}定义。从v0开始的f - 链的pr(Φ, f, v0) = 2，sz(Φ, f, v0) = 5，ls(Φ, f, v0) = 3；从v5开始的f - 链的pr(Φ, f, v5) = 0，sz(Φ, f, v5) = 4，ls(Φ, f, v5) = 4。则p = 2 + 1 = 3，l = 12，k1 = p + l = 15，k2 = p = 3，且Φ |= f 15(x) ≃ f 3(x)。 #### 3. DPLL(Γ + T )作为决策过程 - **定理4**：设R是本质有限理论，P是基础子句集，Γ是基于重写的推理系统。考虑一个DPLL(Γ + T )过程，其中UnsoundIntro逐步添加所有形式为f j(x) ≃ f k(x)（j > k）的方程。若存在n使得创建的子句中包含的文字不超过n个，则DPLL(Γ + T )是判断R ⊎ P形式的平滑问题关于T的可满足性的决策过程。 - **证明思路**：若R ⊎ P不可满足，根据完备性，当kd足够大时，DPLL(Γ + T )会生成空子句；若R ⊎ P可满足，选择足够大的ku以包含定理3中的公理f k1(x) ≃ f k2(x)。将该公理定向为重写规则f k1(x) → f k2(x)，保证不会保留k > k1的项f k(t)。由于子句中文字数量不超过n，对于无界的kd，只会生成有限数量的子句。 - **不同理论下的情况**： - 若Γ是带有负选择的叠加（Superposition）加上超消解（Hyperresolution）： - 当R是Horn理论时，叠加是单位叠加，不会增加子句长度，超消解只生成正单位子句，不会产生包含超过n个文字的子句。 - 当R是每个子句不超过两个文字的非等式子句集，且Γ是消解（Resolution）加上简化（应用f k1(x) → f k2(x)）时，所