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

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

∈ f}是不一致. 若 f 的任意真子集都不是冲突集, 则称 f 为极小冲突集.
Comps, {SD ∧ Obs ∧ {¬A(c)|c
定义 3. 极小碰集 (minimal hitting set, MHS) . 冲突集合簇 F={f 1 , f 2 ,…, f n }, 集合 S 是 F 的一个碰集, 当且仅当
[1]
,
S ∩ , ∅ ∀ ∈ F. 如果 S 的任意真子集都不是 F 的碰集, 那么 S 是 F 的一个极小碰集.
f i
f i
下面通过例 1 对以上 3 个定义进一步说明.
例 1: 图 2 描述了一个乘法加法器实例, M 1 –M 3 和 A 1 –A 2 分别代表乘法器和加法器. i 1 –i 6 、o 1 和 o 2 分别代表系
统的输入和输出.

2 i 1
M 1
3 i 2
o 1 10
A 1
2 i 3
M 2
3 i 4
o 2 12
A 2
2 i 5
M 3
3 i 6
图 2 乘法加法器电路实例

假设通过观测, 输入值 i 1 –i 6 是{2, 3, 2, 3, 2, 3}, 输出值 o 1 、o 2 是{10, 12}. 通过加法和乘法的原则, 若 M 1 –M 3 、
A 1 和 A 2 都正常工作, 则 o 1 和 o 2 的输出值应都为 12, 然而 o 1 的输出值却为 10, 通过一致性原理 [1] , 显然至少有一
个组件出现故障. 基于当前的观测和模型理论, 调用 MCS 求解算法 [11] , 我们能够得到{M 1 , M 2 , A 1 }和{M 1 , M 3 , A 1 ,
A 2 }这两个极小冲突集, 即每个冲突集合中的所有组件都正常工作是不可能的. 对于每一个 MCS 里面的组件, 至少
有一个出现故障, 计算所有极小冲突集的所有极小碰集, 就能够解释观测情况. 根据定义 3, 我们能够找到所有的
极小碰集是{M 1 }, {A 1 }, {M 2 , M 3 }, {M 2 , A 2 }. 例如: {M 1 }是一个候选诊断, 假设 M 1 出现故障 (输出值是 4), 其余组件
都正常, 则 o 1 的输出值可以是 10. 可见计算所有冲突集的极小碰集是获得故障诊断的重要步骤, 故提高极小冲突
集和极小碰集的求解效率能够快速定位诊断.
1.2 基于冲突集计算诊断
定义 4. 文字 (literal) . 给定布尔变量集合 X={x 1 , x 2 ,…, x n }, 文字 l i 是变量 x i 或变量 x i 的否定–x i , 二者互为补集.
[11]
定义 5. 子句 (clause) [11] . 子句 C 是若干个文字的析取组成, C = l 1 ∨l 2 ∨...∨l m .
定义 6. 合取范式 (conjunctive normal form, CNF) [11] . 由多个不同子句合取所组成的公式称为合取范式, F = C 1
∧C 2 ∧...∧C m .
定义 7. 命题可满足性问题 SAT [11] . 给定一组布尔变量, 若能找到一组对变量的真值指派, 使得给定命题公式
中的每一个子句都为真, 则称该问题是可满足的; 反之, 若不存在这样的真值指派, 则称该问题是不可满足的.
例 2: 给定一个与非门, 假设有两个输入 x 1 , x 2 , 一个输出 o 1 , 一组输入输出观测 Obs 1 ={x 1 , −x 2 , o 1 }, 用 CNF 公
式进行描述该组件的逻辑关系, 则公式 F={{−x 1 ∨ −x 2 ∨ −o 1 } ∧ {x 1 ∨ o 1 } ∧ {x 2 ∨ o 1 } ∧ {x 1 } ∧ {−x 2 } ∧ {o 1 }}, 因可以
找到一组赋值{x 1 , −x 2 , o 1 }使得 CNF 中每一个子句都为真, 故该 SAT 问题是可满足的. 若再给定一组观测
Obs 2 ={−x 1 , −x 2 , −o 1 }, 则此时的 F={{−x 1 ∨ −x 2 ∨ −o 1 } ∧ {x 1 ∨ o 1 } ∧ {x 2 ∨ o 1 } ∧ {−x 1 } ∧ {−x 2 } ∧ {−o 1 }}, 因无法找到一
组赋值使得所有子句都为真, 故该问题是不可满足的.
已知与非门存在一个低电平的输入, 输出为高电平. Obs 1 ={x 1 , −x 2 , o 1 }, 输入分别是高、低电平, 输出是高电
平, 符合逻辑值, 产生的 CNF 编码是可满足的. 而对于 Obs 2 ={−x 1 , −x 2 , −o 1 }, 输入是两个低电平, 输出却是低电平,
显然逻辑值错误, 对应的 CNF 编码是不可满足的. 也就是说, 若 CNF 编码不可满足, 则对应不满足子句的组件就
是待诊断故障组件. SAT 子句是由布尔变量给出, 布尔变量中含有的是文字, 相当于本文所说的变量.
SAT 求解器的输入是以 CNF 公式形式, 因此组合电路的相应描述需要以子句集形式表示. 根据图 3 中 c17 电
路进行进一步说明基于冲突集求解诊断. 图 3(a) 和图 3(b) 描述了 c17 电路中组件门的性质及连接关系, 图 3(c) 是
c17 电路的 CNF 编码及求诊断算法 [26] . 在国际基准电路 ISCAS-85 中 [24,28,29] , c17 电路的所有组件都是与非门
(N 1 –N 6 ), 系统输入 (i 7 –i 11 ) 和输出 (o 14 、o 15 ) 是可观测的, 其余都是不可观测的. 在编码时用正文字表示高电平, 负
文字表示低电平. 对于组件, 用正文字表示组件故障, 负文字表示组件正常 (使用 1–17 分别表示电路中对应的下标