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

欧阳继红 等: HSDiag: 变种碰集算法求解诊断 5543

不是 F'的极小诊断, 则必存在∆的真子集∆'是 F'的极小诊断, 由上面证明可得∆'也是 F 的极小诊断, 这与假设∆是
F 的极小诊断矛盾, 故∆是 F 的极小诊断, 也是 F'的极小诊断.
证毕.
综上, 含有 e s 的子句为冗余子句可以直接删除.
布尔算法是一种效率比较高的碰集算法, 它在对子句集 F 选取变量 (e) 时, 会按照递归规则分裂成两个分支
F l 和 F r , 其中, MHS(F)=e ∧ MHS(F l ) ∨ MHS(F r ), F l ={S i |S i ∈ ∧ < S i }, F r ={S i −{e}|S i ∈ F} [18] . 我们把该规则应用于求
F
e
解候选诊断, 并基于引理 1 进一步优化.
命题 2. 集合分裂. 利用碰集算法计算候选诊断当选取 e p 时, 那么子句集 F 分裂成两个分支 F l 和 F r , 其中, F l
是删除含有 e p 的子句及–e p , F l ={S i −{ve p }|S i ∈ F ∧ e p < S i }, 右分支是删除含有–e p 的子句及 e p , F r ={S i −{e p }|S i ∈ F ∧
–e p < S i }.
证明: 根据极小碰集算法选取变量的规则, 当选取 e p 时, 能获得 F l ={S i |S i ∈ F ∧ e p < S i }, F r ={S i −{e p }|S i ∈ F}. 对
于 e p ∧ F l , 由于引理 1, 含有–e p 的候选解都是不可满足的, 所以需要删除左分支中–e p , F l ={S i −{–e p }|S i ∈ ∧ e p < S i }.
F
而对于右分支, 此时–e p 相当于单传播变量, 根据引理 1, 可以删除含有−e p 的集合, F r ={S i −{e p }|S i ∈ ∧ −e p < S i }.
F
证毕.
下面用例 4 对命题 2 进一步说明.
例 4: 继续计算图 3(c) 生成的碰集格式的编码 F={{1, −12}, {2, −13, −12}, {2, 13, 12}, {−17, −12}, {17, 12}, {3,
−13}, {4, −13, −17}}.
图 5 中是采用目前求解效率较高的碰集算法生成树 [17,18,22] , 其中右侧树比左侧树多添加了集合分裂策略. 在
图 5(a) 中, 每次选取一个变量时, 左分支删除含有选取变量的集合, 右分支删除选取的变量, 不断地递归, 直到节点
为空或者只剩一个集合. 而对于图 5(b), 虽然也生成两个分支 (存在单集合变量时生成一个分支), 不同的是, 每次
选取变量后, 左分支进行一个判断, 若选取的变量是传播变量, 则需要额外的删除其补集 (单元传播), 这是因为一
个解中含有一对互补变量是不可行的; 而对于右分支, 删除左分支选取的变量后, 需要额外删除含有单传播变量的
集合. 可见右侧树生成的节点明显少于左侧树. 算法 1 的伪代码是添加分裂策略后的变种碰集算法 HSDiag.

{1,−12}, {2,−13,−12}, {2,13,12}, {1 −12},{2,−13 −12},{2,13,12},

{−17,−12},{17,12},{3,−13},{4,−13,−17} F {−17,−12},{17,12},{3,−13},{4,−13,−17}
−12 −12 12
{2,13,12}, 17,12}, {1},{2,−13},{2,13,12}, F 1 F 2
{3,−13},{4,−13,−17} {−17},{17,12},{3,−13},{4,−13,−17} {2, 3},{17},{3,−13},{4,−13,−17} {1},{2,−13},{−17},{3,−13},{4,−13,−17}
12 1,−17 17 1,−17
{3,−13},{4,−13,−17} {2,13},{17},{3,−13},{4,−13,−17} {2,−13},{2,13,12},{17,12},{3,−13} F 11 {2,13},{3,−13},{4,−13} {2,−13},{3 −13} F 21
−13 17 2 −13 13 −13
ø {3},{4,−17} {2,13},{3,−13},{4 −13 −17} {17,12},{3,−13} {−13},{13,12},{17,12},{3,−13} {2} {3},{4} F 112 ø F 211
3 −13 3 −13 111 3
{4,−17} {2,13} ... {17,12} ... ... {4} F 1121
(a) 碰集算法求诊断 (b) 碰集算法添加分裂策略求诊断
图 5 碰集算法及添加分裂策略求诊断

算法 1. HSDiag(F, D).

输入: CNF 编码 F={S 1 , S 2 ,…, S n }, 诊断 D;
输出: 诊断 D.

1. IF (F== ∅) return;
2. IF (F=={S}){ //只有一个集合
3. IF ( ∃ e p (e p ∈ S)) return; //存在传播变量
∈ S}; //返回每一个组件变量
4. return {{e i }|e i
5. }