Boosting MCSes Enumeration#

背景与动机#

MCS 枚举的重要性#

计算不可满足 CNF 公式 的所有 MCS（Minimal Correction Subset，极小修正子集）或等价地计算所有 MSS（Maximal Satisfiable Subset，极大可满足子集）是许多 AI 任务的基本操作，包括：

• 基于模型的诊断（Model-Based Diagnosis）
• 信念修正（Belief Change）中的怀疑论推理（Skeptical Reasoning）
• 不可满足性分析：因为 MUS（极小不可满足子集）的枚举可以通过先枚举所有 MCS 再利用 hitting set 对偶关系来完成

虽然 MCS 的数量在最坏情况下是指数级的，但在许多实际问题中，MCS 的数量是较低的，因此尝试枚举所有 MCS 在这些情况下是可行的。

预备知识#

基本定义#

给定一个 CNF 公式 ，我们定义以下概念：

也就是说，MSS 和 MCS 是互补的：，删去 MCS 中的子句后，剩下的就是一个极大可满足子集。

Partial-MSS 与 Partial-MCS#

当 分为硬子句 和软子句 时：

• Partial-MSS：必须包含所有硬子句 ，在此基础上关于集合包含极大化包含的软子句
• Partial-MCS：只从软子句 中选取，删去后使得 与剩余的软子句可满足

单个 MCS 的线性搜索#

子句选择器（Clause Selectors）#

对 中的每条子句 ，引入一个新的文字 （选择器），构成松弛公式：

\Sigma^S = \{\alpha \vee \neg s_\alpha \mid \alpha \in \Sigma\}

当 时，子句 被激活（必须满足）；当 时，子句被去激活（自动满足）

转移子句（Transition Clause, TC）#

换言之，TC 就是一个单元素 MCS。同时，TC 也属于 的每一个 MUS。

ExtractPartialMCS：基本线性搜索（BLS）#

ExtractPartialMCS(Σ₁, Σ₂) 是整个枚举框架的基本子程序，其任务是：给定硬子句 和软子句 ，找出一个 Partial-MCS。

基本版本（BLS, Basic Linear Search）的流程如下：

1. 初始化：（硬子句全部放入 MSS），
2. 对 中的每条软子句 （通过选择器逐一激活）：
   • 令 ，调用 SAT 求解器检查 是否可满足
   • 若可满足：将 加入 MSS（）
   • 若不可满足： 此时是一个转移子句（TC），将 加入 MCS（）
3. 返回 MCS

增强线性搜索（ELS）#

ELS（Enhanced Linear Search）是 BLS 的改进版，通过以下技巧减少 SAT 调用次数：

• 已计算模型的利用（Computed Models）：当 SAT 求解器返回 SAT 时，会附带一个模型 。此模型满足当前所有已激活的子句。如果 同时也满足某些尚未考虑的子句 ，那么可以直接将 加入 MSS 而无需额外 SAT 调用（因为 就是 的一个模型）
• 不相交核的利用（Disjoint Cores）：当 SAT 求解器返回 UNSAT 时，会附带一个核（一组导致 UNSAT 的假设/选择器）。核中的每条子句都属于某个 MUS，因此可以一次性识别多个需要放入 MCS 的子句
• 骨架文字（Backbone Literals）：某些文字在所有模型中取值相同（称为骨架文字），利用骨架信息可以提前判断某些子句必然可/不可满足
• MCS 析取：将当前 MCS 中所有子句的析取作为额外约束加入，这可以加速后续的 SAT 调用

基本 MCS 枚举算法#

Enum-ELS（算法 1）#

基本枚举框架如下：

1. 对 构造松弛公式
2. 初始化阻塞子句集
3. 循环：当 可满足时
   • 调用 ExtractPartialMCS 提取一个 Partial-MCS
   • 输出
   • 添加阻塞子句 到 （防止同一 MCS 再次被计算）

枚举顺序与完备性#

一个自然的问题是：BLS/ELS 每次只找到一个 MCS，而且找到哪个取决于子句的考虑顺序。不同的顺序会产出不同的 MCS/MSS 对。那么外层循环如何保证找到所有 MCS？

答案在于阻塞子句 与终止条件的配合。我们分两步论证：

不重复性：每发现一个 MCS ，就添加阻塞子句 。这条子句要求 中至少有一条子句被激活（留在 MSS 中）。因此任何后续发现的 MCS 都不能完全包含 中的所有子句。又因为 本身是极小的（不能移除任何子句），所以 不可能等于 。

完备性（不遗漏）：假设算法终止时（ 不可满足），存在某个 MCS 未被发现。考虑如下赋值：对所有 令 ，对所有 令 。

• 此赋值满足 ：因为 是一个 MSS（可满足的），激活这些子句不产生矛盾
• 此赋值满足 中的每一条阻塞子句：对于任何已发现的 ，由于两者都是极小修正子集，不可能 （否则由 的极小性得 ，矛盾）。因此存在 ，此 的选择器 ，从而阻塞子句 被满足

于是 在此赋值下可满足，这与终止条件矛盾。因此不存在未被发现的 MCS。

基于转移子句的加速枚举#

本文的核心贡献在于：利用转移子句的性质，从一次搜索中递归地构造多个不同的 MCS，从而减少 SAT 调用次数。

关键性质#

性质 1#

设 是不可满足的 CNF， 且 包含至少一个 TC 。对于所有能从 构建的 Partial-MCS ， 是 的一个 MCS。

推论 1（Partial 版本）#

设 ， 可满足， 不可满足。若 使得 含有 TC ，则对所有能从 构建的 Partial-MCS ， 是 的一个 Partial-MCS。

性质 2（不同 TC 产生不同 MCS）#

如果 有两个不同的 TC ，则从 和 分别递归产生的 Partial-MCS 一定不同。

TC-MCS 算法（算法 2）#

输入：，其中 是尚未分配给 MCS 或 MSS 的选择器集合。

算法流程：

1. 若 ，返回空集（递归终止条件）
2. 初始化 （已计算的 Partial-MCS 集合），（已激活的选择器）
3. 增量构造循环：从 中逐个取选择器 加入 ，直到 变为不可满足
   • 此时 就是一个 TC（因为加入它之前公式是可满足的，加入后变为不可满足）
4. 提取核：从 SAT 求解器获取当前不可满足公式的一个核
5. 寻找更多 TC：调用 Find-TC（基于模型旋转）在核 中寻找更多 TC
6. 递归构造：对每个找到的 TC ，递归调用 TC-MCS： 将递归结果中的每个 Partial-MCS 加上 得到一个完整的 Partial-MCS

Enum-ELS-RMR（算法 3）#

在基本枚举框架（算法 1）中，将 ExtractPartialMCS 替换为 TC-MCS：

1. 构造 ，初始化
2. 循环：当 可满足时
   • 调用
   • 对 中的每个 ：输出并添加阻塞子句

递归模型旋转（Recursive Model Rotation, rmr）#

上述算法的关键子程序 Find-TC 使用了递归模型旋转（rmr）来高效地发现额外的 TC。

rmr 的原理#

基于此，rmr 的工作方式如下：

1. 给定 的一个模型 （此模型不满足 ）
2. 从 中选取一个文字，翻转对应变量的值，得到新赋值
3. 检查 是否满足 中除了某条子句 以外的所有子句
4. 如果是，则 也是一个 TC（前提是它之前未被标记为 TC）
5. 对 和 递归地重复这个过程

rmr 在 MCS 枚举中的应用#

在 TC-MCS 算法中，当增量构造到 不可满足时：

• 我们已有 的一个模型 （上一轮 SAT 调用的副产品）
• 是一个 TC
• 使用 rmr 从 出发，通过翻转变量来寻找核 中的其他 TC
• 重要限制：不翻转选择器变量本身，只翻转子句中的原始变量；只保留属于 的 TC

处理阻塞子句 的问题#

性质 3（可分离性）#

与 不共享文字： 中全是选择器的正文字组成的正子句，而 中选择器以负文字出现。因此 的可满足性可以被分解为两个独立的子问题：

\Sigma^S \cup \Delta \cup \bigwedge_{s \in P} s \cup \bigwedge_{s \in N} \neg s \text{ 可满足} \iff \Sigma^S \cup \bigwedge_{s \in P} s \text{ 可满足且 } \Delta \cup \bigwedge_{s \in N} \neg s \text{ 可满足}

其中 是选择器 集合 的一个划分。