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

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

变量). 如: 变量 9 表示 i 9 为高电平, −9 表示 i 9 为低电平, 变量 1 表示组件 N 1 故障. 假设观测到系统的输入 i 7 –i 1 的
1
值分别是{−7, 8, 9, 10, 11}, 系统的输出 o 1 和 4 o 1 值是{14, 15}. 显然, 如果组件都正常工作, 得到的理论值应为
5
{−14, −15}, 故该电路必然存在故障组件. 基于冲突集求诊断主要分为两个阶段, 计算冲突集和计算极小碰集.

1-12-9-10 1 -12 1 3 6 1 2 3
i 16 MCS 基
i 7 o 14 1 12 9 2 -13 -12 1 3 7 1 2 4
N 5
N 3 计算冲突集 于
1 12 10 2 13 12 冲突集 对应
i 13 数据格式 极小不 碰集 冲
i 8 2-13-8-12 6 -17 -12 算法 组件
N 2 可满足 算法
2 13 8 6 17 12 突
i 9 子集
i 12 2 13 12 3 -13 集
i N 1 1 -12 1 求
10 5-16-7-9 4 -13 -17
2 -13 -12 2
5 16 7 −7 诊
i 17 N o 15 5 16 9 2 13 12 3 4 断
i 11 N 6 4 8 单 6 -17 -12
6-17-12-11 9
6 17 12 10 元 6 17 12 1 -12 1 12 -13 -17
(a) c17电路 传 3 -13 基
6 17 11 11 2 -13 -12 2 -12 -13 17 于
3-14-16-13 14 播 4 -13 -17 2 13 12 碰集 3 4 -12 13 17
∧
￢ N 1 →(i 12 ⇔ (i 9 i 10 )) 3 14 16 15 6 -17 -12 算法 获得 变
￢
种
∧
￢ N 2 →(i 13 ⇔ (i 8 i 12 )) 3 14 13 Obs 6 17 12 诊断 碰
￢
￢ 13 i 16 ))
￢ N 3 →(i 14 ⇔ (i ∧ 4-15-13-17 计算碰集 3 -13 集
￢ 13 i 17 ))
￢ N 4 →(i 15 ⇔ (i ∧ 4 15 13 数据格式 4 -13 -17 1 2 求
4 15 17
￢ 7 ∧
￢ N 5 →(i 16 ⇔ (i i 9 )) 3 4 诊
∧ i CNF 编码 断
￢
￢ N 6 →(i 17 ⇔ (i 11 12 ))
(b) 系统描述 (c) 诊断算法
图 3 两种算法计算 c17 电路的候选诊断

第 1 阶段: 计算冲突集. 该阶段一般是基于哈斯图, 首先对编码中的子句生成一个序列, 根据哈斯图中的节点
顺序调用 SAT 求解器判断组成的编码是否可满足, 若不满足则生成一个冲突集合, 通过修剪规则遍历所有的节点
后, 就能够得到所有极小冲突集.
对于图 3(c), 首先对观测值 Obs 进行单元传播, 转化成计算冲突集数据格式的合取范式编码, 白色字体变量在
编码中不会出现, 它对应不可满足子句的组件. 假设调用 SAT 求解器, 获得两个极小冲突集{1, 3, 6}, {1, 3, 7}, 它
们对应的组件分别是{1, 2, 3}, {1, 2, 4}.
第 2 阶段: 计算诊断. 调用碰集算法对第 1 阶段获得的极小冲突集进行求解. 一共获得 3 个极小碰集{1}, {2},
{3, 4}.
可见, 最终得到的极小碰集就是待诊断的故障组件. 在模型诊断中, 部分解的丢失很有可能由于最后一步的故
障检测, 而错过最有可能的故障位置 [25] , 然而要得到所有的极小碰集需要先计算所有的极小冲突集, 否则求出的
解集可能不完备或者不是诊断解. 如图 3, 若调用 SAT 求解器只得到一个极小冲突集{1, 2, 3}, 则极小碰集{3}就不
是一个诊断解, 因为就算组件 N 3 故障也不能解释系统观测.
2 基于变种碰集直接求诊断
基于冲突集计算诊断, 在检查子句可满足时, 实际上就是在对子句集进行碰集求解. 基于冲突集计算诊断在编
码生成方面时, 组件变量不出现在编码中. 在图 3(c) 中, 首先对所有子句进行一个排序, 计算出不可满足子句{1, 3,
6}, {1, 3, 7}后, 需要对组件进行一个映射, 对应的组件变量才是模型诊断中需要的极小冲突集{1, 2, 3}, {1, 2, 4}.
若组件变量出现在编码中, 则所有的子句都是可满足的, 如一个可满足解{1, 2, 3, 4, 6}.
2.1 碰集算法求解诊断

为了保证所提出策略的正确性, 我们对编码中的变量进行定义.
定义 8. 组件变量和 (单) 传播变量 (component variable and (single) propagation variable). 在编码中, 诊断解中
的变量为组件变量, 其余变量为传播变量. 若编码中传播变量不存在补集, 则为单传播变量.
在图 3(c) 的 CNF 编码中, 变量 7–17 是传播变量, 1–6 是组件变量. 如编码中仅存在 9 而不存在−9, 则 9 为单