布尔子句集与最小不可满足子集的关联探究

### 布尔子句集与最小不可满足子集的关联探究 在布尔可满足性问题（SAT）的研究中，确定一组子句是否与至少一个最小不可满足子集（MUS）重叠是一个重要的问题。本文将深入探讨相关概念、方法和算法，旨在解决这一问题并提高计算效率。 #### 1. MUS的基本概念 在一个不可满足的SAT实例Σ中，MUS是Σ的一个不可满足子句集，且不能在不恢复其可满足性的情况下使其更小。MUS代表了不一致性的最小原因，通过冲突子句来表达。 **定义1**：一组子句Γ是Σ的最小不可满足子集（MUS），当且仅当： 1. Γ ⊆ Σ 2. Γ 不可满足 3. ∀Δ ⊂ Γ，Δ 可满足 **示例1**：设Σ = {¬d ∨ e, b ∨ ¬c, ¬d, ¬a ∨ b, a, a ∨ ¬c ∨ ¬e, ¬a ∨ c ∨ d, ¬b}。Σ 不可满足，包含2个MUS，分别是 {a, ¬a ∨ b, ¬b} 和 {b ∨ ¬c, ¬d, a, ¬a ∨ c ∨ d, ¬b}。 在这个示例中，子句“a”和“¬b”对于Σ的不一致性是必要的，“¬d ∨ e”和“a ∨ ¬c ∨ ¬e”是从不必要的，而其他子句是潜在必要的。 | 子句类型 | 子句示例 | | ---- | ---- | | 必要子句 | a, ¬b | | 潜在必要子句 | ¬d, ¬a ∨ b, b ∨ ¬c, ¬a ∨ c ∨ d | | 从不必要子句 | ¬d ∨ e, a ∨ ¬c ∨ ¬e | #### 2. Shapley不一致性度量 Shapley不一致性度量用于衡量一个子句α在SAT实例Σ中的不一致性得分。该度量考虑了包含α的MUS的数量以及每个MUS的大小，从而能够考虑每个不一致源中子句的参与度或“重要性”。 **定义2**：设Σ是一个SAT实例，α ∈ Σ。设∪MUS Σ是Σ的所有MUS的集合。α在Σ中的不一致性度量MI，记为MI(Σ, α)，定义为： \[MI(Σ, α) = \sum_{\{\Delta | \Delta \in \cup MUS_{\Sigma} \text{ 且 } \alpha \in \Delta\}} \frac{1}{|\Delta|}\] **示例2**：考虑示例1中的CNF Σ，我们有： - MI(Σ, ¬a ∨ b) = 1/3 - MI(Σ, b ∨ ¬c) = 1/5 - MI(Σ, ¬d ∨ e) = 0 - MI(Σ, a) = MI(Σ, ¬b) = 1/3 + 1/5 = 8/15 #### 3. 问题定义 一组布尔子句Γ实际上参与SAT实例Σ的不一致性，当且仅当Γ包含至少一个属于Σ的至少一个MUS的子句，即一个对于Σ的不一致性是必要或潜在必要的子句。 **定义3**：设∪MUSΣ是一组布尔子句Σ的MUS集合，Γ也是一组布尔子句。Γ参与Σ的不一致性，当且仅当∃α ∈ Γ，∃Δ ∈ ∪MUSΣ 使得 α ∈ Δ。 #### 4. 使用聚类简化问题 为了在一定程度上规避问题的高计算复杂度，我们采用将Σ划分为预先设定数量m的子句子集（称为聚类）的策略。 **定义4**：设Σ是一个SAT实例。Σ的子句m - 聚类Π是将Σ划分为m个子集Πj，其中j ∈ [1..m]。Πj称为Σ的第j个聚类（相对于Σ的聚类Π）。 所有聚类内的子句被视为合取式，以提供一个在Σ内被解释为不可分割的交互实体的公式。Γ的子句也以同样的方式处理，形成一个额外的合取式。此时，初始问题被转化为一个更粗粒度的问题，即检查作为一个整体的Γ的合取式如何参与由m个单独子公式组成的新Σ表示的不一致性。 #### 5. 从MUS到MUSC 随着问题转移到使用聚类作为基本交互实体来分析不一致性的框架中，MUS概念需要相应地进行调整，从而产生了Σ的聚类Π的最小不可满足聚类集（MUSCΠ）的概念。 **定义5**：设Σ是一个SAT实例，Π是Σ的子句m - 聚类。Σ的Π的最小不可满足聚类集（MUSCΠ）MΠ是一组聚类，使得： 1. MΠ ⊆ Π 2. MΠ 不可满足 3. ∀Φ ∈ MΠ，MΠ \ {Φ} 可满足 标准的MUS概念是MUSC概念的一个特殊实例，其中每个聚类实际上是一个子句。因此，MUS代表了通过矛盾子句解释Σ不一致性的最细粒度抽象级别。 **命题1**：设Σ是一个SAT实例，Π是Σ的m - 聚类，MΠ是Σ的MUSCΠ。如果Πi ∈ MΠ，则∃α ∈ Πi，∃Ψ ∈ ∪MUSΣ 使得 α ∈ Ψ。 **示例3**：设Σ由14个子句组成，形成9个MUS。当需要检查子句“¬a”和“c ∨ ¬d”是否参与Σ的不一致性，并在肯定情况下提取相应的MUS时，在最坏情况下可能需要计算所有MUS。将子句聚类后，得到5个聚类，在这个抽象级别上，只剩下3个MUSCΠ，分别是 M1 = {➊, ➌}，M2 = {➋, ➌, ➍} 和 M3 = {➋, ➍, ➎}。 ```mermaid graph LR classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; A(原始子句集Σ):::process --> B(聚类):::process B --> C(MUSC计算):::process C --> D{MUSC结果}:::process D -->|有重叠| E(找到重叠MUS):::process D -->|无重叠| F(细化聚类):::process F --> B ``` 这个示例说明了聚类子句的好处，即可以避免提取所有MUS来回答是否存在重叠MUS的问题。然而，如果子句被聚类后没有出现在MUSC中，并不意味着它们在子句级别上不参与公式的不一致性。 **命题2**：设Σ是一个SAT实例，Π是Σ的m - 聚类，Πi ∈ Π。命题1确保了：如果 (∃MΠ ∈ ∪MUSCΠ 使得 Πi ∈ MΠ)，那么 (∃α ∈ Πi，∃Ψ ∈ ∪MUSΣ 使得 α ∈ Ψ)，但反之不成立。 #### 6. 测量MUSC之间的冲突 不一致性度量基于Shapley值的一种形式，需要进行调整以将聚类视为基本交互实体。 **定义6**：设Σ是一个SAT实例，Π是Σ的m - 聚类。聚类Πi的不一致性度量MI定义为： \[M