Page 161 - 《软件学报》2025年第12期

5542 软件学报 2025 年第 36 卷第 12 期

传播变量. 为了方便描述, 用 e c 、e p 、e s 分别代表组件变量、传播变量及单传播变量. 利用碰集算法直接计算诊断
时需要返回待诊断的组件, 所以把组件变量放入编码中.
定义 9. 极大可满足子集 (maximal satisfiable subset, MSS) [11] . 给定子句集 U, 若 F ⊆ U, F 称作 U 的极大可满足
子集, 当且仅当 F 是可满足的, F 再添加一个子句是不可满足的.
定义 10. 极小修正集 (minimal correction set, MCS') [11] . 给定子句集 U, 若 F ⊆ U, F 称作 U 的极小修正集, 当且
仅当 U\F 是可满足的, U\F 再添加一个子句是不可满足的.
由图 4 可知, 在基于模型诊断中, 极小不可满足子集和极小冲突集是等价的, 而计算他们的极小碰集, 即极小
修正集和极小碰集也是等价的 [11] . MSS 和极小诊断互为补集, 利用碰集算法, 在不改变碰集算法的规则前, 优先选
取传播变量, 选取所有可以满足的子句 (相当于求解极大可满足子集), 对于不可满足的子句选取组件变量进行碰
集求解 (相当于求解补集), 最终的碰集解只需要保留组件变量.

极小碰集
极小不可 极小修正
满足子集 集
互为补集
极大可满
等价 系统描述 等价
足子集
互为补集
极小冲突 极小诊断
集 极小碰集

图 4 系统描述到候选诊断关系图

命题 1. 碰集算法计算带有组件变量的 CNF 编码可以获得所有极小诊断.
下面分别从正确性和完备性来对命题 1 进行证明.
正确性: 由诊断定义 1 可知, 需要找到一个极小诊断∆ 来满足系统所产生的所有子句. 利用碰集算法首先找到
不含组件的最大可满足的子集 MSS, 剩余不可满足的子句 (MSS 的补集) 用组件变量代替, 即极小诊断.
完备性: MCS'的补集是 MSS (具有一一对应关系), 根据已有算法可知 MCS'是完备性的, 那么可以推出 MSS
的完备性, 故 MSS 的补集也是完备的.
证毕.
例 3: 利用碰集计算图 3(c) 中 F={{1, −12}, {2, −13, −12}, {2, 13, 12}, {6, −17, −12}, {6, 17, 12}, {3, −13}, {4,
−13, −17}}的极小诊断.
假设利用碰集算法, 在不选取组件变量的前提下, 碰集 HS={12, −13, −17}对应的一个 MSS(F)={{2, −13, −12},
{2, 13, 12}, {6, −17, −12}, {6, 17, 12}, {3, −13}, {4, −13, −17}}, 则剩下一个集合{1, −12}, 需要选取组件变量 1 (选
取变量−12 会形成不可行解), 因碰集中只需要保留组件变, 故碰集 HS 只需要返回诊断解{1}.
直接调用碰集算法得到的解中含有大量的非组件变量. 为了避免产生过多的冗余解, 在变量选取的时候, 优先
选取传播变量, 并删除含有单传播变量的子句. 我们提出一种集合分裂策略, 该策略结合碰集算法, 大幅度减少左
右分支的冗余子句.
2.2 集合分裂
在求解诊断时, 因获得的解是极小的, 故可以删除含有单传播变量 e s 的子句. 我们用引理 1 给出, 并用碰集知
识进行证明.
引理 1. F 和 F'有相同的极小诊断, 其中 F'={F−{S}|S ∈ ∧ e s ∈ S}.
F
证明: 首先证明∆是 F'的极小诊断也是 F 的极小诊断. 因 e s 可以满足子句集 S, 当∆对 e s 进行传播时, e s 已经
与 S 有交集, 不会改变∆的值, 故∆也是 F 的极小诊断. 下面证明∆是 F 的极小诊断解也是 F'的极小组件诊断解.
反证法: 若∆是 F 的极小诊断, 因 F'是 F 的真子集, 故∆也是 F'的诊断. 接着证明极小性, 根据极小性原理, 若∆