Tldr

文章链接

本文提出了一种基于**转移子句（Transition Clause）与递归模型旋转（Recursive Model Rotation, rmr）**的 MCS 枚举加速技术。核心思想是：在枚举过程中，通过识别多个转移子句（TC），从一个 TC 出发递归地构造多个不同的 MCS，从而大幅减少 SAT 求解器的调用次数。实验结果表明，该方法在几乎所有 benchmark 上均优于当时最先进的 mcscache-els。

Boosting MCSes Enumeration

Abstract

The enumeration of all Maximal Satisfiable Subsets (MSSes) or all Minimal Correction Subsets (MCSes) of an unsatisfiable CNF Boolean formula is a useful and sometimes necessary step for solving a variety of important A.I. issues. Although the number of different MCSes of a CNF Boolean formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efficient practical approaches to enumerate MCSes. It implements a model rotation paradigm that allows the set of MCSes to be computed in an heuristically efficient way.

背景与动机

MCS 枚举的重要性

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

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

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

预备知识

基本定义

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

Core（核）

${\Sigma }_0$ 是 $\Sigma$ 的一个核，当且仅当 ${\Sigma }_0\subseteq \Sigma$ 且 ${\Sigma }_0$ 是不可满足的

MUS（极小不可满足子集）

${\rm Y}$ 是 $\Sigma$ 的一个 MUS，当且仅当 ${\rm Y}$ 是 $\Sigma$ 的一个核，且 $\forall \alpha \in {\rm Y},{\rm Y}\setminus \{\alpha \}$ 是可满足的

MSS（极大可满足子集）

$\Phi$ 是 $\Sigma$ 的一个 MSS，当且仅当 $\Phi \subseteq \Sigma$ 是可满足的，且 $\forall \alpha \in \Sigma \setminus \Phi ,\Phi \cup \{\alpha \}$ 是不可满足的

MCS（极小修正子集）

$\Psi$ 是 $\Sigma$ 的一个 MCS（也称 Co-MSS），当且仅当 $\Sigma \setminus \Psi$ 是 $\Sigma$ 的一个 MSS

也就是说，MSS 和 MCS 是互补的：$\Sigma =\text{MSS}\cup \text{MCS}$，删去 MCS 中的子句后，剩下的就是一个极大可满足子集。

极小/极大（集合包含）vs. 最小/最大（基数）

本文中的 “maximal” 和 “minimal” 始终是关于集合包含（set-inclusion） 的，而不是关于集合大小（cardinality）的。两者的区别如下：

• 极大（maximal）：不能再往里加元素了。即 $\Phi$ 是极大可满足子集，意味着再加入 $\Sigma$ 中任何一条不在 $\Phi$ 里的子句都会导致不可满足。但可以存在另一个更大的极大可满足子集 ${\Phi }^{\prime }$，满足 $|{\Phi }^{\prime }|>|\Phi |$，只要 $\Phi ⊈{\Phi }^{\prime }$
• 最大（maximum）：是所有可满足子集中基数最大的那个（唯一，或基数相同的若干个）。最大可满足子集一定是极大可满足子集，但反过来不成立

类似地：

• 极小（minimal）：不能再删元素了。即 $\Psi$ 是极小修正子集，意味着 $\Psi$ 中删去任何一条子句后，$\Sigma \setminus (\Psi \setminus \{\alpha \})$ 就不再可满足了
• 最小（minimum）：是所有修正子集中基数最小的那个

一个公式可以有多个大小不同的极大/极小子集，但最大/最小子集的基数是唯一的。

以下面的例 1 为例：四个 MCS 的大小都是 2，四个 MSS 的大小分别是 $|\Sigma \setminus \{{\alpha }_1,{\alpha }_6\}|=4$, $|\Sigma \setminus \{{\alpha }_2,{\alpha }_6\}|=4$, $|\Sigma \setminus \{{\alpha }_3,{\alpha }_5\}|=4$, $|\Sigma \setminus \{{\alpha }_4,{\alpha }_5\}|=4$。在这个例子中恰好大小一致，但一般情况下不同 MSS 的大小可以不同——Max-SAT 求的就是基数最大的那个 MSS（即最小基数的 MCS），而本文关注的是枚举所有极大/极小子集。

例 1

设不可满足 CNF $\Sigma =\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4,{\alpha }_5,{\alpha }_6\}$，其中：

• ${\alpha }_1=a\vee b$, ${\alpha }_2=\neg a\vee b$, ${\alpha }_3=a\vee \neg b$
• ${\alpha }_4=\neg a\vee \neg b$, ${\alpha }_5=\neg b$, ${\alpha }_6=b$

MCSes: $\{{\alpha }_1,{\alpha }_6\}$, $\{{\alpha }_2,{\alpha }_6\}$, $\{{\alpha }_3,{\alpha }_5\}$, $\{{\alpha }_4,{\alpha }_5\}$

MUSes: $\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4\}$, $\{{\alpha }_1,{\alpha }_2,{\alpha }_5\}$, $\{{\alpha }_3,{\alpha }_4,{\alpha }_6\}$, $\{{\alpha }_5,{\alpha }_6\}$

可以验证，每个 MCS 的补集都是一个 MSS。例如 $\Sigma \setminus \{{\alpha }_1,{\alpha }_6\}=\{{\alpha }_2,{\alpha }_3,{\alpha }_4,{\alpha }_5\}$ 是可满足的（令 $a=0,b=0$）

Partial-MSS 与 Partial-MCS

当 $\Sigma =⟨{\Sigma }_1,{\Sigma }_2⟩$ 分为硬子句 ${\Sigma }_1$ 和软子句 ${\Sigma }_2$ 时：

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

注意

• 如果 ${\Sigma }_1$ 本身不可满足，则 Partial-MSS 不存在
• 每个 $⟨{\Sigma }_1,{\Sigma }_2⟩$ 的 Partial-MCS 也是 ${\Sigma }_1\cup {\Sigma }_2$ 的 MCS
• 但 ${\Sigma }_1\cup {\Sigma }_2$ 的某些 MCS 可能包含硬子句，因此不是 Partial-MCS

单个 MCS 的线性搜索

子句选择器（Clause Selectors）

对 $\Sigma$ 中的每条子句 $\alpha$，引入一个新的文字 $\neg s_{\alpha }$（选择器），构成松弛公式：

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

当 $s_{\alpha }=1$ 时，子句 $\alpha$ 被激活（必须满足）；当 $s_{\alpha }=0$ 时，子句被去激活（自动满足）

选择器的好处

选择器允许在同一次搜索中动态激活/去激活子句，同时 SAT 求解器可以在每一步记录有用的信息。特别是，当某个假设集导致不可满足时，现代 SAT 求解器能够提取导致不可满足的假设子集（即一个核）

转移子句（Transition Clause, TC）

定义：转移子句

子句 $\alpha \in \Sigma$ 是 $\Sigma$ 的一个转移子句（TC），当且仅当 $\Sigma$ 是不可满足的，且 $\Sigma \setminus \{\alpha \}$ 是可满足的

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

ExtractPartialMCS：基本线性搜索（BLS）

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

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

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

BLS 示例

设 ${\Sigma }_1=\varnothing$，${\Sigma }_2=\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4,{\alpha }_5,{\alpha }_6\}$（即例 1 中的公式），按顺序考虑：

步骤	考虑	SAT?	动作	MSS	MCS
1	${\alpha }_1=a\vee b$	$\{{\alpha }_1\}$ SAT	加入 MSS	$\{{\alpha }_1\}$	$\varnothing$
2	${\alpha }_2=\neg a\vee b$	$\{{\alpha }_1,{\alpha }_2\}$ SAT	加入 MSS	$\{{\alpha }_1,{\alpha }_2\}$	$\varnothing$
3	${\alpha }_3=a\vee \neg b$	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$ SAT	加入 MSS	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$	$\varnothing$
4	${\alpha }_4=\neg a\vee \neg b$	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4\}$ UNSAT	TC！加入 MCS	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$	$\{{\alpha }_4\}$
5	${\alpha }_5=\neg b$	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_5\}$ SAT	加入 MSS	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_5\}$	$\{{\alpha }_4\}$
6	${\alpha }_6=b$	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_5,{\alpha }_6\}$ UNSAT	TC！加入 MCS	$\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_5\}$	$\{{\alpha }_4,{\alpha }_5\}$

最终 MCS = $\{{\alpha }_4,{\alpha }_5\}$，MSS = $\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_5\}$。可以验证这确实是例 1 中的一个合法 MCS/MSS 对

为什么 UNSAT 时 α 是 TC

在第 4 步中，$\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$ 是可满足的，但加入 ${\alpha }_4$ 后变为不可满足。这恰好符合 TC 的定义：${\alpha }_4$ 使得公式从可满足”转移”到不可满足。此时 ${\alpha }_4$ 必须被移出（放入 MCS），因为它与当前 MSS 不兼容。

但注意：${\alpha }_4$ 只是关于当前积累的子集 $\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4\}$ 的 TC，而不一定是关于整个 $\Sigma$ 的 TC。BLS 的正确性在于：只要每次 UNSAT 时将 TC 放入 MCS，最终得到的 MCS 是关于整个 $\Sigma$ 的一个合法 Partial-MCS。

BLS 的关键缺陷

BLS 每个软子句都需要一次 SAT 调用。对于 $|{\Sigma }_2|=n$ 条软子句，恰好需要 $n$ 次 SAT 调用来提取一个 MCS。这就是为什么 SAT 调用次数是整个枚举算法的主要瓶颈。

增强线性搜索（ELS）

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

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

已计算模型的威力

继续上面的例子。在第 1 步中，SAT 求解器返回 $\{{\alpha }_1\}$ 可满足，并给出模型 $\mu =\{a=1,b=1\}$。此模型同时满足 ${\alpha }_2=\neg a\vee b$（因为 $b=1$）和 ${\alpha }_3=a\vee \neg b$（因为 $a=1$）。于是，${\alpha }_2,{\alpha }_3$ 可以免费加入 MSS，省去两次 SAT 调用。

这就是为什么 ELS 在实践中比 BLS 快得多——大量子句可以通过模型”批量”加入 MSS。

基本 MCS 枚举算法

Enum-ELS（算法 1）

基本枚举框架如下：

1. 对 $\Sigma$ 构造松弛公式 ${\Sigma }^S$
2. 初始化阻塞子句集 $\Delta =\varnothing$
3. 循环：当 ${\Sigma }^S\cup \Delta$ 可满足时
   • 调用 ExtractPartialMCS 提取一个 Partial-MCS $M^{-}$
   • 输出 $M^{-}$
   • 添加阻塞子句 ${\bigvee }_{s_{\alpha }\in M^{-}}{s}_{\alpha }$ 到 $\Delta$（防止同一 MCS 再次被计算）

阻塞子句的作用

阻塞子句要求至少一个属于已发现 MCS 的子句被激活，从而防止 SAT 求解器再次找到完全相同的 MCS

枚举顺序与完备性

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

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

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

完备性（不遗漏）：假设算法终止时（${\Sigma }^S\cup \Delta$ 不可满足），存在某个 MCS $M^{\ast }$ 未被发现。考虑如下赋值：对所有 $\alpha \in \Sigma \setminus M^{\ast }$ 令 $s_{\alpha }=1$，对所有 $\alpha \in M^{\ast }$ 令 $s_{\alpha }=0$。

• 此赋值满足 ${\Sigma }^S$：因为 $\Sigma \setminus M^{\ast }$ 是一个 MSS（可满足的），激活这些子句不产生矛盾
• 此赋值满足 $\Delta$ 中的每一条阻塞子句：对于任何已发现的 $M_i^{-}\ne M^{\ast }$，由于两者都是极小修正子集，不可能 $M_i^{-}\subseteq M^{\ast }$（否则由 $M^{\ast }$ 的极小性得 $M_i^{-}=M^{\ast }$，矛盾）。因此存在 $\alpha \in M_i^{-}\setminus M^{\ast }$，此 $\alpha$ 的选择器 $s_{\alpha }=1$，从而阻塞子句 ${\bigvee }_{s_{\alpha }\in M_i^{-}}{s}_{\alpha }$ 被满足

于是 ${\Sigma }^S\cup \Delta$ 在此赋值下可满足，这与终止条件矛盾。因此不存在未被发现的 MCS。$\square$

用例 1 跟踪整个枚举过程

回顾例 1：MCSes = $\{{\alpha }_1,{\alpha }_6\}$, $\{{\alpha }_2,{\alpha }_6\}$, $\{{\alpha }_3,{\alpha }_5\}$, $\{{\alpha }_4,{\alpha }_5\}$

轮次	$\Delta$	ExtractPartialMCS 找到	添加的阻塞子句
1	$\varnothing$	$M_1^{-}=\{{\alpha }_4,{\alpha }_5\}$	$s_4\vee s_5$
2	$\{s_4\vee s_5\}$	$M_2^{-}=\{{\alpha }_3,{\alpha }_5\}$	$s_3\vee s_5$
3	$\{s_4\vee s_5,s_3\vee s_5\}$	$M_3^{-}=\{{\alpha }_1,{\alpha }_6\}$	$s_1\vee s_6$
4	$\{s_4\vee s_5,s_3\vee s_5,s_1\vee s_6\}$	$M_4^{-}=\{{\alpha }_2,{\alpha }_6\}$	$s_2\vee s_6$
5	$\{s_4\vee s_5,s_3\vee s_5,s_1\vee s_6,s_2\vee s_6\}$	${\Sigma }^S\cup \Delta$ UNSAT → 终止	—

每一轮中，BLS/ELS 可能因为不同的内部顺序找到不同的 MCS，但阻塞子句确保不重复，终止条件确保不遗漏。具体第几轮找到哪个 MCS 取决于 BLS/ELS 内部的子句考虑顺序，但最终四个 MCS 一定都会被找到。

小结

ExtractPartialMCS（BLS/ELS）只负责找一个 MCS——找到哪个取决于启发式顺序，这无关紧要。完备性由外层循环的阻塞子句机制保证，而不是由 ExtractPartialMCS 本身保证。这也是为什么本文可以将 ExtractPartialMCS 替换为 TC-MCS 而不影响正确性——只要每轮能找到（至少一个）尚未发现的 MCS 即可。

性能瓶颈

此算法的耗时部分在于提取每个 Partial-MCS 时对 SAT 求解器的多次调用。[Previti et al., 2017] 提出了缓存策略（mcscache-els），将搜索过程中发现的核进行缓存，这是当时最高效的 MCS 枚举算法

基于转移子句的加速枚举

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

关键性质

性质 1

设 $\Sigma$ 是不可满足的 CNF，${\Sigma }_0\subseteq \Sigma$ 且 ${\Sigma }_0$ 包含至少一个 TC $\alpha$。对于所有能从 $⟨{\Sigma }_0\setminus \{\alpha \},\Sigma \setminus {\Sigma }_0⟩$ 构建的 Partial-MCS $\Gamma$，$\Gamma \cup \{\alpha \}$ 是 $\Sigma$ 的一个 MCS。

理解这个性质

直觉：如果 $\alpha$ 是不可满足子集 ${\Sigma }_0$ 的一个 TC，那么 ${\Sigma }_0\setminus \{\alpha \}$ 是可满足的。把 ${\Sigma }_0\setminus \{\alpha \}$ 作为硬子句，$\Sigma \setminus {\Sigma }_0$ 作为软子句，找到的任何 Partial-MCS $\Gamma$ 加上 $\{\alpha \}$ 就是 $\Sigma$ 的一个完整 MCS。

证明核心思路（反证法）：假设 $\Gamma \cup \{\alpha \}$ 不是 $\Sigma$ 的 MCS，则要么 $\Sigma \setminus (\Gamma \cup \{\alpha \})$ 不可满足，要么存在 $\beta \in \Gamma \cup \{\alpha \}$ 可以被移除。两种情况都会导致矛盾。

推论 1（Partial 版本）

设 $⟨{\Sigma }_1,{\Sigma }_2⟩$，${\Sigma }_1$ 可满足，${\Sigma }_1\cup {\Sigma }_2$ 不可满足。若 ${\Sigma }_2^{\prime }\subseteq {\Sigma }_2$ 使得 ${\Sigma }_1\cup {\Sigma }_2^{\prime }$ 含有 TC $\alpha \in {\Sigma }_2^{\prime }$，则对所有能从 $⟨{\Sigma }_1\cup {\Sigma }_2^{\prime }\setminus \{\alpha \},{\Sigma }_2\setminus {\Sigma }_2^{\prime }⟩$ 构建的 Partial-MCS $\Gamma$，$\Gamma \cup \{\alpha \}$ 是 $⟨{\Sigma }_1,{\Sigma }_2⟩$ 的一个 Partial-MCS。

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

如果 ${\Sigma }_1\cup {\Sigma }_2^{\prime }$ 有两个不同的 TC ${\alpha }_1,{\alpha }_2\in {\Sigma }_2^{\prime }$，则从 ${\alpha }_1$ 和 ${\alpha }_2$ 分别递归产生的 Partial-MCS 一定不同。

性质 1、推论 1、性质 2 的完整示例

构造一个稍大的不可满足公式来完整展示三个性质如何配合工作。

设 $\Sigma =\{{\alpha }_1,{\alpha }_2,{\alpha }_3,{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$，其中：

${\alpha }_1=a,{\alpha }_2=b,{\alpha }_3=\neg a\vee \neg b,{\alpha }_4=\neg a\vee c,{\alpha }_5=\neg b\vee \neg c,{\alpha }_6=\neg a,{\alpha }_7=\neg b$

可以验证 $\Sigma$ 不可满足（${\alpha }_1$ 要求 $a=1$，${\alpha }_6$ 要求 $a=0$，矛盾就已经出现）。

现在假设在 TC-MCS 的增量构造中，我们按顺序激活 ${\alpha }_1,{\alpha }_2,{\alpha }_3$：

• $\{{\alpha }_1\}$：SAT（$a=1$）✓
• $\{{\alpha }_1,{\alpha }_2\}$：SAT（$a=1,b=1$）✓
• $\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$：UNSAT（${\alpha }_1$ 要求 $a=1$，${\alpha }_2$ 要求 $b=1$，但 ${\alpha }_3=\neg a\vee \neg b$ 要求 $a=0$ 或 $b=0$）

所以 ${\alpha }_3$ 是 ${\Sigma }_0=\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$ 的一个 TC。

---

性质 1 的应用：${\alpha }_3$ 是 ${\Sigma }_0=\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$ 的 TC。令：

• 硬子句：${\Sigma }_0\setminus \{{\alpha }_3\}=\{{\alpha }_1,{\alpha }_2\}$
• 软子句：$\Sigma \setminus {\Sigma }_0=\{{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$

在硬子句 $\{{\alpha }_1,{\alpha }_2\}$（即 $a=1,b=1$）的约束下，对软子句运行 ExtractPartialMCS：

• ${\alpha }_4=\neg a\vee c$：要求 $c=1$（因为 $a=1$），$\{{\alpha }_1,{\alpha }_2,{\alpha }_4\}$ SAT（$a=1,b=1,c=1$）→ 加入 MSS
• ${\alpha }_5=\neg b\vee \neg c$：要求 $b=0$ 或 $c=0$，但 $b=1,c=1$，$\{{\alpha }_1,{\alpha }_2,{\alpha }_4,{\alpha }_5\}$ UNSAT → 加入 MCS
• ${\alpha }_6=\neg a$：$a=1$ 矛盾，$\{{\alpha }_1,{\alpha }_2,{\alpha }_4,{\alpha }_6\}$ UNSAT → 加入 MCS
• ${\alpha }_7=\neg b$：$b=1$ 矛盾，$\{{\alpha }_1,{\alpha }_2,{\alpha }_4,{\alpha }_7\}$ UNSAT → 加入 MCS

得到 $\Gamma =\{{\alpha }_5,{\alpha }_6,{\alpha }_7\}$。根据性质 1，$\Gamma \cup \{{\alpha }_3\}=\{{\alpha }_3,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$ 是 $\Sigma$ 的一个 MCS。

验证：$\Sigma \setminus \{{\alpha }_3,{\alpha }_5,{\alpha }_6,{\alpha }_7\}=\{{\alpha }_1,{\alpha }_2,{\alpha }_4\}$，即 $a\wedge b\wedge (\neg a\vee c)$，令 $a=1,b=1,c=1$ 即可满足。✓

---

但 ${\Sigma }_0$ 中不止一个 TC！ 让我们检查：

• ${\alpha }_1$ 是 TC 吗？${\Sigma }_0\setminus \{{\alpha }_1\}=\{b,\neg a\vee \neg b\}$，令 $a=0,b=1$ 可满足 → 是 TC
• ${\alpha }_2$ 是 TC 吗？${\Sigma }_0\setminus \{{\alpha }_2\}=\{a,\neg a\vee \neg b\}$，令 $a=1,b=0$ 可满足 → 是 TC
• ${\alpha }_3$ 是 TC 吗？${\Sigma }_0\setminus \{{\alpha }_3\}=\{a,b\}$，令 $a=1,b=1$ 可满足 → 是 TC

三条子句都是 ${\Sigma }_0$ 的 TC！（这是因为 ${\Sigma }_0$ 本身恰好是一个 MUS——三条子句中任意删一条都可满足。）

---

推论 1 + 性质 2 的应用：现在令 ${\Sigma }_1=\varnothing$，${\Sigma }_2=\Sigma$，${\Sigma }_2^{\prime }={\Sigma }_0=\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$。三个 TC ${\alpha }_1,{\alpha }_2,{\alpha }_3$ 各自产生一族 MCS：

TC = ${\alpha }_1$：硬子句 ${\Sigma }_0\setminus \{{\alpha }_1\}=\{{\alpha }_2,{\alpha }_3\}$（即 $b=1$ 且 $\neg a\vee \neg b$，因此 $a=0$），软子句 $\{{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$

• ${\alpha }_4=\neg a\vee c$：$a=0$ 下自动满足 → 加入 MSS
• ${\alpha }_5=\neg b\vee \neg c$：$b=1$ 下需 $c=0$ → 加入 MSS（$a=0,b=1,c=0$）
• ${\alpha }_6=\neg a$：$a=0$ 下自动满足 → 加入 MSS
• ${\alpha }_7=\neg b$：$b=1$ 矛盾 → 加入 MCS

${\Gamma }_1=\{{\alpha }_7\}$，最终 MCS = ${\Gamma }_1\cup \{{\alpha }_1\}=\{{\alpha }_1,{\alpha }_7\}$

TC = ${\alpha }_2$：硬子句 ${\Sigma }_0\setminus \{{\alpha }_2\}=\{{\alpha }_1,{\alpha }_3\}$（即 $a=1$ 且 $\neg a\vee \neg b$，因此 $b=0$），软子句 $\{{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$

• ${\alpha }_4=\neg a\vee c$：$a=1$ 下需 $c=1$ → 加入 MSS（$a=1,b=0,c=1$）
• ${\alpha }_5=\neg b\vee \neg c$：$b=0$ 下自动满足 → 加入 MSS
• ${\alpha }_6=\neg a$：$a=1$ 矛盾 → 加入 MCS
• ${\alpha }_7=\neg b$：$b=0$ 下自动满足 → 加入 MSS

${\Gamma }_2=\{{\alpha }_6\}$，最终 MCS = ${\Gamma }_2\cup \{{\alpha }_2\}=\{{\alpha }_2,{\alpha }_6\}$

TC = ${\alpha }_3$：如上面性质 1 所计算，MCS = $\{{\alpha }_3,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$

---

性质 2 的验证：三个 MCS 确实两两不同：

• $\{{\alpha }_1,{\alpha }_7\}$
• $\{{\alpha }_2,{\alpha }_6\}$
• $\{{\alpha }_3,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$

为什么保证不同？以 ${\alpha }_1$ 和 ${\alpha }_2$ 为例：${\Gamma }_1$ 来自软子句 $\Sigma \setminus {\Sigma }_0=\{{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$，因此 ${\Gamma }_1\subseteq \{{\alpha }_4,{\alpha }_5,{\alpha }_6,{\alpha }_7\}$。而 ${\alpha }_2\in {\Sigma }_0$，所以 ${\alpha }_2\notin {\Gamma }_1$。因此 ${\Gamma }_1\cup \{{\alpha }_1\}$ 不包含 ${\alpha }_2$，但 ${\Gamma }_2\cup \{{\alpha }_2\}$ 包含 ${\alpha }_2$，故两者一定不同。

一般地：不同 TC 来自 ${\Sigma }_2^{\prime }$，而对应的 $\Gamma$ 来自 ${\Sigma }_2\setminus {\Sigma }_2^{\prime }$，二者不相交。所以 TC ${\alpha }_i$ 一定不在另一个 TC ${\alpha }_j$ 的 ${\Gamma }_j$ 中，从而 ${\Gamma }_i\cup \{{\alpha }_i\}\ne {\Gamma }_j\cup \{{\alpha }_j\}$。

---

总结：从一次 UNSAT 证明（${\Sigma }_0=\{{\alpha }_1,{\alpha }_2,{\alpha }_3\}$ 不可满足）中，我们发现了 3 个 TC，一次性产出了 3 个不同的 MCS。而传统 Enum-ELS 每次只能产出 1 个 MCS。这就是 TC-MCS 的效率来源。

关键洞察

这意味着我们可以从一次 UNSAT 证明中提取多个 TC，每个 TC 各自递归产生不同的 MCS 族，且保证不重复。这就是本文效率提升的核心来源。

TC-MCS 算法（算法 2）

输入：$⟨{\Sigma }_1\cup {\Sigma }_2^S,U⟩$，其中 $U$ 是尚未分配给 MCS 或 MSS 的选择器集合。

算法流程：

1. 若 $U=\varnothing$，返回空集（递归终止条件）
2. 初始化 $\Theta =\varnothing$（已计算的 Partial-MCS 集合），$M^{+}=\varnothing$（已激活的选择器）
3. 增量构造循环：从 $U$ 中逐个取选择器 $s_{\alpha }$ 加入 $M^{+}$，直到 ${\Sigma }_1\cup {\Sigma }_2^S\cup M^{+}\cup \{s_{\alpha }\}$ 变为不可满足
   • 此时 $s_{\alpha }$ 就是一个 TC（因为加入它之前公式是可满足的，加入后变为不可满足）
4. 提取核：从 SAT 求解器获取当前不可满足公式的一个核 $\Gamma$
5. 寻找更多 TC：调用 Find-TC（基于模型旋转）在核 $\Gamma$ 中寻找更多 TC
6. 递归构造：对每个找到的 TC $s_{\beta }\in T\cap M^{+}$，递归调用 TC-MCS： $\text{TC-MCS}(⟨{\Sigma }_1\cup {\Sigma }_2^S\cup (\Gamma \setminus \{\neg s_{\beta }\}),U\cup (M^{+}\setminus \Gamma )⟩)$ 将递归结果中的每个 Partial-MCS 加上 $\{s_{\beta }\}$ 得到一个完整的 Partial-MCS

理解递归调用的参数

当 $s_{\beta }$ 是核 $\Gamma$ 中的一个 TC 时：

• 将 $\Gamma$ 中除了 $s_{\beta }$ 对应子句以外的部分作为硬约束（因为 $\Gamma \setminus \{\neg s_{\beta }\}$ 激活了这些子句）
• 不在核 $\Gamma$ 中但在 $M^{+}$ 中的选择器，以及原来的 $U$ 中未处理的选择器，作为待分配的软子句
• 这样递归寻找新的 MCS，加上当前 TC $s_{\beta }$，得到原问题的一个 MCS

根据性质 2，不同 TC 产生的 MCS 族一定不重叠

Enum-ELS-RMR（算法 3）

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

1. 构造 ${\Sigma }^S$，初始化 $\Delta =\varnothing$
2. 循环：当 ${\Sigma }^S\cup \Delta$ 可满足时
   • 调用 $\Theta \leftarrow \text{TC-MCS}(⟨{\Sigma }^S\cup \Delta ,S⟩)$
   • 对 $\Theta$ 中的每个 $M^{-}$：输出并添加阻塞子句

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

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

rmr 的原理

TC 的模型论视角

子句 $\alpha \in \Sigma$ 是一个 TC，当且仅当存在一个完全赋值 $\mu$ 满足 $\Sigma \setminus \{\alpha \}$（但不满足 $\alpha$，否则 $\Sigma$ 就可满足了）

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

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

为什么叫"旋转"

从 $\mu$（满足 $\Sigma \setminus \{\alpha \}$）出发，通过翻转一个变量”旋转”到 ${\mu }^{\prime }$（满足 $\Sigma \setminus \{{\alpha }^{\prime }\}$），从一个 TC 转到另一个 TC，这个过程就像在模型空间中旋转。

rmr 在 MCS 枚举中的应用

在 TC-MCS 算法中，当增量构造到 ${\Sigma }_1\cup {\Sigma }_2^S\cup M^{+}\cup \{s_{\alpha }\}$ 不可满足时：

• 我们已有 ${\Sigma }_1\cup {\Sigma }_2^S\cup M^{+}$ 的一个模型 $\mu$（上一轮 SAT 调用的副产品）
• $s_{\alpha }$ 是一个 TC
• 使用 rmr 从 $\mu$ 出发，通过翻转变量来寻找核 $\Gamma$ 中的其他 TC
• 重要限制：不翻转选择器变量本身，只翻转子句中的原始变量；只保留属于 $\{s_{\beta }\in M^{+}\}$ 的 TC

rmr 的特性

• rmr 是多项式时间的（每次翻转只需检查一遍所有子句）
• rmr 是不完备的：它可能无法找到所有 TC，但找到的一定是正确的
• 为确保终止性，直接将 $s_{\alpha }$ 加入 $T$（第 9 行），即使 rmr 没有发现 $s_{\alpha }$ 是 TC

处理阻塞子句 $\Delta$ 的问题

\Delta 在 rmr 中的陷阱

如果 rmr 过程中不考虑阻塞子句 $\Delta$，可能会找到已经被枚举过的 MCS，导致输出重复。

例子：${\Sigma }^S=\{\neg s_1\vee a\vee b,\neg s_2\vee \neg a,\neg s_3\vee \neg b\}$，已发现 MCS $\{s_1\}$，因此 $\Delta =\{s_1\}$。如果不考虑 $\Delta$，在下一轮中 $s_1,s_2,s_3$ 都会被标记为 TC，从而重复计算同一 MCS。

性质 3（可分离性）

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

$${\Sigma }^S\cup \Delta \cup \underset{s\in P}{\bigwedge }s\cup \underset{s\in N}{\bigwedge }\neg s\text{ 可满足}⟺{\Sigma }^S\cup \underset{s\in P}{\bigwedge }s\text{ 可满足且 }\Delta \cup \underset{s\in N}{\bigwedge }\neg s\text{ 可满足}$$

其中 $\{P,N\}$ 是选择器 集合 $S$ 的一个划分。

为什么 \Sigma^S 和 \Delta 不共享文字？

这是由构造方式决定的：

• ${\Sigma }^S$ 通过 $\alpha \vee \neg s_{\alpha }$ 构造——选择器总是以负文字 $\neg s$ 出现
• $\Delta$ 的每条阻塞子句是 ${\bigvee }_{s_{\alpha }\in M^{-}}{s}_{\alpha }$——选择器总是以正文字 $s$ 出现

二者在选择器变量上的极性完全相反，因此对任意一个选择器的赋值决策，它对 ${\Sigma }^S$ 的影响和对 $\Delta$ 的影响是完全独立的。

性质 3 的完整示例

继续使用例 1 的公式 $\Sigma =\{{\alpha }_1,\dots ,{\alpha }_6\}$。

松弛公式：

${\Sigma }^S=\{(a\vee b)\vee \neg s_1,(\neg a\vee b)\vee \neg s_2,(a\vee \neg b)\vee \neg s_3,(\neg a\vee \neg b)\vee \neg s_4,\neg b\vee \neg s_5,b\vee \neg s_6\}$

假设前两轮已发现 $M_1^{-}=\{{\alpha }_4,{\alpha }_5\}$ 和 $M_2^{-}=\{{\alpha }_3,{\alpha }_5\}$，则：

$\Delta =\{s_4\vee s_5,s_3\vee s_5\}$

观察极性：${\Sigma }^S$ 中选择器出现为 $\neg s_1,\neg s_2,\neg s_3,\neg s_4,\neg s_5,\neg s_6$（全部取负）；$\Delta$ 中选择器出现为 $s_3,s_4,s_5$（全部取正）。没有共享文字。

---

构造一个合法划分：取 $P=\{s_1,s_3,s_5\}$（激活 ${\alpha }_1,{\alpha }_3,{\alpha }_5$），$N=\{s_2,s_4,s_6\}$（去激活 ${\alpha }_2,{\alpha }_4,{\alpha }_6$）。

检查 ${\Sigma }^S$ 侧：${\Sigma }^S\cup \{s_1,s_3,s_5\}$ 激活 ${\alpha }_1=a\vee b$，${\alpha }_3=a\vee \neg b$，${\alpha }_5=\neg b$。

• $\neg b$：$b=0$
• $a\vee b=a\vee 0=a$：需 $a=1$
• $a\vee \neg b=1\vee 1=1$ ✓

模型 $\mu =\{a=1,b=0\}$。SAT ✓

检查 $\Delta$ 侧：$\Delta \cup \{\neg s_2,\neg s_4,\neg s_6\}$，即 $s_2=0,s_4=0,s_6=0$，$s_1,s_3,s_5$ 自由。

• $s_4\vee s_5$：$s_4=0$，需 $s_5=1$ → 满足
• $s_3\vee s_5$：$s_5=1$ → 满足

SAT ✓

两侧独立可满足 $⟹$ ${\Sigma }^S\cup \Delta \cup \{s_1,s_3,s_5,\neg s_2,\neg s_4,\neg s_6\}$ 可满足。

---

增量构造：以 $M^{+}=\{s_1,s_3,s_5\}$ 为起点，尝试将 $M^{-}=\{s_2,s_4,s_6\}$ 中的选择器移入 $M^{+}$。

移动 $s_2$ → $M^{+}$：${\Sigma }^S\cup \{s_1,s_2,s_3,s_5\}$，激活 ${\alpha }_2=\neg a\vee b$。 之前的模型 $a=1,b=0$ 下 $\neg a\vee b=0$。UNSAT → $s_2$ 是 TC！

此时 $M^{-}=\{s_4,s_6\}$。我们需要检查 $\Delta$ 侧吗？

$\Delta \cup \{\neg s_4,\neg s_6\}$：$s_4=0,s_6=0$，$s_1,s_2,s_3,s_5$ 自由。

• $s_4\vee s_5=0\vee s_5$：$s_5=1$ → 满足
• $s_3\vee s_5$：满足

仍然 SAT ✓。实际上我们根本不需要做这个检查！因为 $s_2$ 从 $M^{-}$ 移到 $M^{+}$ 意味着 $s_2$ 从 $0$ 变为 $1$。$\Delta$ 中只有正文字的选择器，把一个选择器从 $0$ 变成 $1$ 只会让更多析取项为真，永远不会破坏 $\Delta$ 的可满足性。

这就是性质 3 的核心推论：$\Delta$ 的可满足性关于选择器取正是单调的。

---

rmr 中忽略 $\Delta$：发现 TC $s_2$ 后，运行 rmr。模型 $\mu =\{a=1,b=0\}$（不满足 ${\alpha }_2=\neg a\vee b$）。

翻转 $a\to 0$：${\mu }^{\prime }=\{a=0,b=0\}$。检查所有已激活子句：

• ${\alpha }_1=a\vee b=0\vee 0=0$ → 唯一被破坏的子句
• ${\alpha }_2=\neg a\vee b=1$ ✓（之前的 TC 变为满足）
• ${\alpha }_3=a\vee \neg b=0\vee 1=1$ ✓
• ${\alpha }_5=\neg b=1$ ✓

恰好只有 ${\alpha }_1$ 被破坏 → $s_1$ 也是一个 TC！

$s_1\in M^{+}$（不在 $M^{-}$ 中）→ 接受。

如果翻转后发现被破坏的是 ${\alpha }_6$（$s_6\in M^{-}$），则拒绝——因为 $s_6$ 留在 $M^{-}$ 中是为了保证 $\Delta$ 可满足。虽然此例中 $s_6$ 不出现在 $\Delta$ 里，但算法保守地禁止所有 $M^{-}$ 中的选择器，以避免逐一检查 $\Delta$ 的开销。

---

总结此例：整个增量构造和 rmr 过程中，我们从未检查过 $\Delta$。只在初始阶段做了一次 $\Delta$ 侧的可满足性检查来确定 $M^{-}$，之后所有操作都在 ${\Sigma }^S$ 侧进行。这就是性质 3 带来的效率提升。

利用可分离性

在构造 $M^{+}$ 的过程中，我们隐式地维护了一个划分 $\{M^{+},M^{-}\}$。由于 $\Delta$ 只包含正子句，把一个选择器从 $M^{-}$ 移到 $M^{+}$（赋值为正）不会使 $\Delta$ 变得不可满足。

因此，在 rmr 过程中，可以忽略 $\Delta$，只要禁止 $M^{-}$ 中的选择器被选为 TC。这样就完全避免了 rmr 中检查 $\Delta$ 的开销。

具体做法

1. 先计算一个初始划分 $\{M^{+},M^{-}\}$，使得 ${\Sigma }^S\cup {\bigwedge }_{s\in M^{+}}s$ 和 $\Delta \cup {\bigwedge }_{s\in M^{-}}\neg s$ 同时可满足
2. 将 $M^{+}$ 作为起点进行增量构造
3. $M^{-}$ 中的选择器被标记——rmr 过程中禁止将 $M^{-}$ 中的选择器标记为 TC
4. 增量构造中选择器从 $M^{-}$ 移到 $M^{+}$ 时，$\Delta$ 的可满足性自动保持（单调性），无需检查

对并行化的意义

性质 3 表明 ${\Sigma }^S$ 和 $\Delta$ 是两个解耦的约束系统。这为并行化提供了结构性基础：

1. 计算密集的部分（TC-MCS 搜索、rmr）只操作 ${\Sigma }^S$ 侧——这是可以并行的
2. 簿记部分（阻塞子句 $\Delta$ 的管理）只涉及正文字子句，求解代价极低
3. 多个 worker 可以从不同的初始划分 $\{M^{+},M^{-}\}$ 出发，各自独立地在 ${\Sigma }^S$ 上搜索 TC 和 MCS，而不需要在搜索过程中同步 $\Delta$——只需在每一批搜索结束后，将发现的 MCS 汇总更新到 $\Delta$ 中即可

实验

实验设置

• 实现：C++，使用 Minisat 作为后端 SAT 求解器
• Benchmark：
  • [Previti et al., 2017] 使用的 866 个实例（269 个 Max-SAT + 597 个 Partial-Max-SAT）
  • 额外加入 MUS 竞赛的 plain Max-SAT 实例
  • 共 1090 个实例（493 个 plain Max-SAT + 597 个 Partial-Max-SAT）
• 环境：Intel Xeon E5-2643 (3.30GHz)，64GB 内存，Linux CentOS
• 限制：每个实例 1800 秒超时，8GB 内存限制

实验结果

Enum-ELS-RMR vs. Enum-ELS（不使用 rmr）

rmr 范式在所有 plain Max-SAT 实例上都能计算出更多（或同样多）的 MCS，对大多数 Partial-Max-SAT 实例也是如此。

Enum-ELS-RMR-Cache vs. Enum-ELS-RMR

结合缓存技术后，Enum-ELS-RMR-Cache 在大多数情况下能枚举更多的 MCS。但缓存也有副作用：

• 某些实例上，缓存的内存开销过大导致 memory-out
• 这些实例上 Enum-ELS-Cache 本身就比 Enum-ELS-RMR 差

Enum-ELS-RMR-Cache vs. mcscache-els

核心实验结论

Enum-ELS-RMR-Cache 在几乎所有 benchmark 上优于 mcscache-els（当时最先进的算法），且在 MCS 数量最多的实例上优势最为显著

总结与展望

核心贡献

1. 提出了基于 TC 的递归 MCS 枚举算法 TC-MCS
2. 将 rmr 范式（原用于 MUS 枚举）创新性地应用到 MCS 枚举中
3. 利用性质 3 的可分离性，避免 rmr 中处理阻塞子句的开销
4. 与缓存技术兼容，组合后效果更优

未来方向

• 并行化：性质 3 的可分离性为并行枚举提供了可能
• 局部搜索：用局部搜索来发现更多 TC
• 偏好 MCS：当子句有偏好排序时，枚举所有偏好 MCS
• 怀疑论推理：所有 MSS 的交集可以用于实现怀疑论推理

MUS-MCS 对偶关系

Hitting Set 对偶

MCS 集合与 MUS 集合之间存在 hitting set 对偶关系：每个 MUS 与每个 MCS 至少有一个公共子句。因此，高效的 MCS 枚举直接改善 MUS 枚举的效率（先枚举所有 MCS，再通过 hitting set 计算所有 MUS）