Page 389 - 《软件学报》2024年第4期

蒋璐宇 等: 针对 MUS 求解问题的加强剪枝策略 1967

1.1 SAT 问题相关定义
SAT 问题是理论计算机科学中的重要问题, 同时也是 MUS、MCS 和 MSS 问题的基础. 下面给出 SAT 问题
中相关定义.
定义 1. 文字 (literal) [33] . 给定一个布尔变量集合 X = {x 1 , x 2 ,..., x n } , 文字 l i 是变量 x i 或变量 x i 的否定 ¬x i . 前
者称为正文字, 后者称为负文字.
定义 2. 子句 (clause) [33] . 子句 c i 是若干个文字的析取 c i = l i1 ∨l i2 ∨...∨l i j .
定义 3. 合取范式 (CNF) [33] . 一个 CNF 公式 F 是若干个子句的合取, F = c 1 ∧ c 2 ∧...∧c m .

定义 4. 命题可满足性问题 (SAT) [33] . 对于给定的布尔变量集合, 若能找到一组对变量的真值指派, 使得给定
的命题公式的值为真, 则称该问题是可满足的; 反之, 若不存在这样的真值指派, 则称该问题是不可满足的.
1.2 不可满足问题中的概念及关系
MUS 是 SAT 问题的扩展, 在不可满足问题中, 每个约束描述为一个子句. 通过对不可满足问题中 MUS、MSS
和 MCS 的计算, 可以从繁多的约束中分析出导致问题不可满足的原因. 下面给出 MUS、MSS 和 MCS 的概念以
及三者之间的关系.
定义 5. 极小不可满足子集 (MUS) [24] . 称集合 U 是不可满足问题中子句集 F 的 MUS, 当且仅当 U ⊆ F , 且 U

不可满足, 且 ∀c ∈ U,U\{c} 可满足.
定义 6. 极大可满足子集 (MSS) [24] . 称集合 S 是不可满足问题中子句集 F 的 MSS, 当且仅当 S ⊆ F , 且 S 可满
足, 且 ∀c ∈ F\S,S ∪{c} 不可满足.
定义 7. 极小修正集 (MCS) [24] . 称集合 C 是不可满足问题中子句集 F 的 MCS, 当且仅当 C ⊆ F , 且 F\C 可满
足, 且 ∀c ∈ C,F\(C\{c}) 不可满足.
根据定义 6 和定义 7 可以看出, 每一个 MSS 的补集都是一个 MCS, 反之亦然. 文献 [20] 中详细说明了 MUS
与 MCS 之间存在互为极小碰集的对偶关系. 下面给出极小碰集的概念:
定义 8. 碰集 (hitting set) [16] . 称集合 H 是集合簇 Q 的碰集, 当且仅当 H ⊆ ∪ Q ′ ∈Q Q , ∀Q ϵQ,H ∩ Q , ∅ .
′
′
′
定义 9. 极小碰集 (minimal hitting set) [16] . 称集合 H M 是集合簇 Q 的极小碰集, 当且仅当集合 H M 是集合簇 Q
的碰集且集合 H M 的任意真子集都不是集合簇 Q 的碰集.
例 1: 给定一个布尔变量集合 X = {a,b} 和在其上的子句集 C = {l 1 : (a∨b), l 2 : (¬a), l 3 : (a∨¬b),l 4 : (b)} , 则该
问题所对应的所有 MUS 为 {l 1 ,l 2 ,l 3 } 和 {l 2 ,l 3 ,l 4 } , 所有 MSS 为 {l 1 ,l 3 ,l 4 } 、 {l 1 ,l 2 ,l 4 } 和 {l 2 ,l 3 } , 所有 MCS 为 {l 2 } 、
{l 1 ,l 4 } . 且根据 MCS 与 MSS 互为补集的关系、MCS 与 MUS 互为极小碰集的关系可知, 只要求出其中一
{l 3 } 和
者的全部集合, 其余两者就可以通过这些关系而求解出来.
1.3 哈斯图
在 MUS 枚举问题中, 求解的关键在于对子句集的幂集的探索. 而哈斯图结构能够很好地刻画出整个搜索空
间并能清晰反映出集合间的包含关系. 其形状上中间鼓, 两头尖, 中间层的顶点数量最多, 具有对称性. 一个含有 4
个子句的不可满足问题对应的哈斯图如图 1 所示. 哈斯图在横向和纵向上都具有显著的特点.
(1) 横向: 哈斯图的最顶层节点代表子句集 C, 最底层节点代表空集. 同一水平层的节点所代表的集合具有相
同的基数, 自上而下基数逐层减一. 假设子句集 C 中共包含 n 个子句, 令最底层为第 1 层, 那么第 i 水平层 i ( 从 1
i
开始编号) 含有的节点个数为 C .
n
(2) 纵向: 哈斯图的纵向体现出节点所代表集合的包含关系. 对于哈斯图中的每个节点, 其下一层与之有边相
连的节点代表的是该集合的子集, 其上一层与之有边相连的节点代表的是该集合的超集, 相邻层节点间无边相连
则说明两个节点所代表的集合之间无包含关系. 由此可见, 从一个节点出发, 在向上的路径可到达的所有节点都是
该节点的超集, 在向下的路径可到达的所有节点都是该节点的子集.
公理 1. 一个可满足的子句集的任何一个子集也一定是可满足的, 一个不可满足的子句集的任何一个超集也
一定是不可满足的.