逻辑程序求解中的证明理论与扩展表格演算

### 逻辑程序求解中的证明理论与扩展表格演算 在逻辑程序求解领域，尤其是答案集编程（ASP）和命题可满足性（SAT）方面，证明理论和求解效率一直是重要的研究方向。本文将深入探讨ASP中的表格演算、证明复杂度，以及扩展ASP表格演算的相关内容。 #### 1. 析取程序与表格演算 在析取程序中，`disj (Π)` 表示程序 `Π` 中出现的析取式集合。为处理析取式，有额外的表格规则，其目的是确保 `T {l1; ... ; ln} ∈ A` 当且仅当 `(AT ∩ P) |= (τ[l1] ∨ ... ∨ τ[ln])`。通过将处理析取式的规则添加到已有的规则中，可得到析取程序的表格演算，定理1也能扩展到析取程序。 #### 2. 证明复杂度 为比较不同的表格演算，我们引入证明复杂度的概念。直观上，证明复杂度关注的是独立于启发式影响的证明查找算法运行时间的下限。我们通过比较不可满足逻辑程序（即没有答案集的程序）的最小反驳大小来进行评估。表格的大小由其包含的节点数决定。 如果存在一个无限的不可满足程序族 `{Πn}`，使得另一个表格演算 `T ′` 对 `Π` 的最小反驳在 `T` 对 `Π` 的最小反驳大小上是渐近指数级的，那么表格演算 `T` 不能被 `T ′` 多项式模拟。如果 `T` 能多项式模拟 `T ′`，但反之不成立，则 `T` 比 `T ′` 指数级更强。 对于正常逻辑程序，`C[atom(Π)]` 和 `C[conj (Π)]` 都能产生可靠且完整的表格演算，但 `C[atom(Π) ∪ conj (Π)]` 得到的演算比它们指数级更强。这引发了一个有趣的问题：对其他复合结构（如基数约束和析取式）进行切割是否会产生更强的演算。 #### 3. 基数程序的表格演算 考虑基数程序 `Π`，定义两个表格演算： - `Tc = {(a - f), (h - r), C[atom(Π) ∪ conj(Π) ∪ card(Π)]}` - `Tc = {(a - f), (h - r), C[atom(Π) ∪ conj (Π)]}` 这两个演算都包含处理基数程序的所有确定性表格规则，区别在于 `Tc` 允许对基数约束进行切割，而 `Tc` 不允许。显然，`Tc` 能多项式模拟 `Tc`，但反之不成立，即 `Tc` 比 `Tc` 指数级更强。 以不可满足的基数程序 `Πn c` 为例： ```plaintext Πn c = { x ← 1{a1, b1}2, ..., 1{an, bn}2, not x ai ← not bi bi ← not ai i = 1..n } ``` 对于 `1 ≤ i ≤ n`，包含 `F (1{ai, bi}2)` 的分支会立即产生矛盾。`Tc` 的无限制切割规则允许对 `1{ai, bi}2` 进行切割，得到的最小反驳在 `n` 上是线性大小；而 `Tc` 必须对原子 `ai` 或 `bi` 进行切割，会生成一个大小在 `n` 上是指数级的完全二叉树。 这一结果的实际意义在于，处理基数约束的ASP求解器通过对基数约束进行分支可以显著提高速度。例如，`lparse` 将基数约束编译为“基本约束规则”，引入辅助原子来缩写基数约束，使得 `smodels` 可以隐式地对基数约束进行分支。 #### 4. 析取程序的表格演算 对于析取程序，验证处理无基集的表格规则 `U ↑` 和 `U ↓` 的不可适用性是coNP难的。因此，除非 `P = NP`，析取程序的表格通常不是多项式可验证的。析取程序的语法通常将析取式限制在规则头中。如果取消这一限制，程序 `Πn c` 可以用析取式 `{ai; bi}` 重写，会得到与基数约束类似的切割规则的指数级分离。 当析取式限制在规则头时，在 `T {l1; ... ; ln}` 分支中获得的信息较弱。我们推测，在这种情况下，对析取式进行分支可能不会带来指数级的改进，但应用切割规则仍然是方便的。 #### 5. 无基集处理的不对称性 在现有ASP求解器的推理中，无基集处理存在不对称性。非基于SAT的ASP求解器可以进行用表格规则 `U ↑` 描述的推理，但没有求解器实现 `U ↓`。这