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

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

6. ELSE IF ( ∃ e ({e} ∈ F)){ //存在单变量集合
7. IF (e 是 e c ){ //是组件变量
F
8. HSDiag({S i −{e c }|S i ∈ ∧ e c < S i }, D);
9. D ← {d ∪ {e c }|d ∈ D};
10. }
e
F
11. ELSE HSDiag({S i −{–e}|S i ∈ ∧ < S i }, D); //删除含有变量 e 的集合并删除变量–e
12. }
13. ELSE {
( )
∪
14. e ← Select_element S i ; //从子句集中选取变量
S i ∈F
15. IF (e 是 e p ){ //是传播变量
16. IF ( ∃ ∀ S i (S i ∈ → ∈ S i )) return; //所有集合都含有传播变量 e
e
e
F
17. IF (e 不是 e c ) //不是单传播变量
18. HSDiag({S i −{e}|S i ∈ F ∧−e < S i }, RightD); //删除含有变量−e 的集合并删除变量 e
∈ ∧ < S i }, LeftD); //删除含有变量 e 的集合并删除变量−e
19. HSDiag({S i −{–e}|S i F e
20. }
21. ELSE { //是组件变量
∈ ∧ < S i }, LeftD); //把含有变量 e 的集合删除
22. HSDiag({S i |S i F e
∈ F}, RightD); //把变量 e 删除
23. HSDiag({S i −{e}|S i
24. D ← {ld ∪ {e}|ld ∈ LeftD} ∪ RightD;
25. }
26. }

LeftD、RightD 分别存储左分支、右分支中间过程生成的解集, 初始化为空, ld 是 LeftD 的子集.
在求解诊断时, 若编码子句为空, 则直接返回 (第 1 行); 若集合个数为 1 (第 2 行), 判断子句中是否存在传播变
量 e p , 若存在 e p , 说明该子句是可满的则直接返回, 否则返回子句中每个组件变量 e c (第 3, 4 行); 若子句个数大于
1 且存在单变量集合 (第 6 行), 若该单字是单传播变量 e c , 删除含有该单字的集合并继续递归, 候选诊断中的每个
解扩展变量 e (第 7–9 行), 否则删除含有 e p 的集合并且删除该变量的补集 (第 11 行); 若子句个数大于 1 且没有单
变量集合, 从子句集中选择一个变量用来递归 (第 14 行), 若该变量是 e p (第 15 行), 所有子句都含有该 e p , 说明所
有的子句是可满足的, 则直接返回 (第 16 行), 若该变量不是单传播变量, 根据引理 1, 则把子句中所有含有变量–e
的子句删除并删除变量 e, 继续递归 (第 17, 18 行), 之后生成左分支子句集接着递归 (第 19 行). 若选取的变量 e
是 e c , 则生成左右两个分支进行递归, 其中左分支是删除含有变量 e 的集合, 右分支只删除变量 e, 最后左分支解
集扩展变量 e 后合并右分支解集 (第 22–24 行).
算法 1 每次选取变量的时候调用集合分裂规则, 即删除选取的含有变量的集合并删除该变量的补集. 对于图 5(b)
右侧树, 根节点用 F 表示, 左右分支分别用下标 1、2 表示, 只有一个分支用 1 表示, 如 F 的左右分支为 F 1 、F 2 , F 1
的左右分支为 F 11 , F 12 , 依次递推. 这里需要注意的是, 为了使算法与枚举树对应, 我们把选取的变量放在路径上
(箭头), 生成的中间集合簇放在节点上.
F 不是一个集合且不存在单变量集合 (第 1–12 行), 从 F 中选取变量–12 进行递归 (第 14 行), 因为是传播变量
且不是单传播变量 (第 17 行), 生成右分支 F 2 和左分支 F 1 (第 18, 19 行), 左分支 F 1 继续算法递归; F 1 存在单变量
集合且不是组件变量 (第 11 行), 生成 F 1 继续算法递归; F 1 选取变量−13 生成左右分支 F 111 , F 112 (第 17–19 行),
1
1
此时 F 11 只有一个集合且是组件变量, 返回组件变量并扩展路径上的组件变量. 其余节点依次递归直到算法截止.
1
2.3 等价类优化
把电路编码成 CNF 公式, 当组件不断增多时, 编码子句成线性增长, 求解诊断难度成指数增长. 若能够缩减子