布尔子句集与高阶逻辑自动定理证明进展

### 布尔子句集与高阶逻辑自动定理证明进展 在逻辑推理和自动定理证明领域，有两个重要的研究方向值得关注，一是检查一组子句是否与可满足性问题（SAT）实例中的至少一个极小不可满足子集（MUS）重叠，二是高阶逻辑自动定理证明（ATP）系统的发展。下面将详细介绍这两个方面的相关内容。 #### 检查子句集与MUS重叠的算法 该算法旨在解决检查一组子句是否与SAT实例中的至少一个MUS重叠的问题。它采用了“抽象 - 细化”的技术，以下是具体的步骤和相关函数： 1. **子句评分（scoreClauses）** ```plaintext Function scoreClauses Input: Σ: a CNF Output: A score vector of clauses of Σ begin for each clause c of Σ do SΣ(c) ← 0; I ← a random assignment of each variable of Σ ; while a preset maximum of steps is reached do for each clause c of Σ do if c is critical w.r.t I in Σ then SΣ(c) ++ ; I ← I′ s.t. I and I′ differs exactly by one assignment of a Boolean variable ; return SΣ ; end ``` 此函数通过局部搜索启发式地为子句评分，初始时所有子句的分数都设为0。在局部搜索过程中，对于相对于当前解释为关键的子句，其分数会增加。关键子句是指被当前解释证伪，且任何满足该子句的相邻解释都会证伪之前满足的另一个子句。 2. **子句聚类（clusterClauses）** ```plaintext Function clusterClauses Input: Σ: a CNF, SΣ: a score vector, m: the size of the clustering Output: A m-clustering of Σ begin Π ← ∅; for i ∈ [1..m - 1] do Πi ← the ( |Σ| / m )th clauses with the highest scores in Σ ; Π ← Π ∪ {Πi} ; Σ ← Σ \ Πi ; Π ← Π ∪ {Σ} ; return Π ; end ``` 该函数将子句聚类成`m`个簇。它按照子句的分数从高到低依次选取，形成一个个簇。 3. **选择包含特定子句集的MUSC（selectOneMUSC）** ```plaintext Function selectOneMUSC Input: ∪MUSCΠ : the set of MUSC w.r.t. Π, Γ: a CNF Output: An MUSC of ∪MUSCΠ containing Γ begin MΓ ← Π ; foreach M s.t. M ∈ ∪MUSCΠ do if Γ ⊆ M and |M| < |MΓ | then MΓ ← M ; return MΓ ; end ``` 此函数从所有MUSC中选择包含特定子句集`Γ`且子句数量最少的MUSC。 4. **计算不一致性度量（MI）** ```plaintext Function MI Input: Πi: an element of the clustering Π, ∪MUSCΠ : the set of MUSC Π Output: The measure of inconsistency of Πi w.r.t. Π begin mi ← 0 ; foreach MUSC Π ∈ ∪MUSCΠ do if Πi ∈ MUSC Π then mi ← mi + 1 / |MUSC Π| ; return mi ; end ``` 该函数计算聚类中某个元素相对于整个聚类的不一致性度量。 #### 主算法流程 主算法的输入包括一个CNF公式`Σ`、它的一个子部分`Γ`以及三个正整数参数`m`、`inc`和`s`。具体流程如下： 1. 运行局部搜索为子句评分。 2. 调用`clusterClauses`函数将子句聚类成`m`个簇。 3. 调用修改后的`HYCAM*`版本计算所有MUSC。 4. 根据聚类的一致性情况进行不同处理： - 如果全局不一致，通过递归调用`look4MUS`增加`inc`个簇来细化聚类。 - 如果检测到局部不一致，判断`Γ`是否参与其中： - 如果`Γ`不参与任何局部MUSC，拆分`s`个最冲突的簇以揭示涉及`Γ`的冲突源。 - 如果`Γ`参与局部不一致，选择包含`Γ`且子句数量最少的MUSC，继续计算只考虑该MUSC。 5. 当达到预设的计算时间或聚类达到单条子句时，调用“经典”的`HYCAM`进行计算，输出包含`Γ`信息的MUS或证明不存在这样的MUS。 #### 实验结果 为了验证算法的有效性，进行了实验。实验在