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

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

conflict set is inseparable. The efficiency of the HSDiag algorithm optimized by equivalence class is improved by more than 2 times in
standard Polybox and Fulladder circuits.
Key words: model-based diagnosis (MBD); system description; minimal conflict set (MCS); minimal hitting set (MHS); equivalence class

基于模型诊断 (model-based diagnosis, MBD) 是人工智能的一个重要领域, MBD 专家 Reiter 提出的开创性工
作是根据系统描述利用基于推理的方法来解释系统观测产生不一致的原因 [1] . MBD 被广泛应用于芯片检测 [2] 、
国家配电网 [3,4] 、软件故障定位 [5] 等众多领域 [6,7] . 图 1 是模型诊断框架, 首先对真实的环境系统进行建模编码, 然
后通过系统观测对实际值和理论值进行一致性检测, 若不一致则产生冲突, 利用 SAT/ATMS 求解器找到所有的极
小冲突集 [8,9] . 最后计算极小冲突集的极小碰集就是待诊断系统的故障元件. 这里需要注意的是, 因为极小冲突集
和极小不可满足子集在模型诊断中是相同的概念, 所以本文统一称为极小冲突集 [10,11] .

Real system System model System encoding
p wcnf 6 17 25
o-7 8 9 10 11 14 15
1-12-9-10
1 12 9
1 12 10
2-13-8-12
2 13 8 1 2 3
2 13 12
5-16-7-9 1, 2 1, 3 2, 3
5 16 7 1, 2, 3
5 16 9 MHS
6-17-12-11
6 17 12
6 17 11
3-14-16-13 Candidate
3 14 16 diagnosis
3 14 13
···
Monitoring Predicting
a i 1, 2, 3
b j
? 1, 2 1, 3 2, 3
c m Inconsistent SAT/ATMS
1 2 3
d n
MCS
System observation Consistency checking
图 1 MBD 框架

计算极小冲突集主要基于枚举树和哈斯图 [12] . 2009 年赵相福等人 [13] 提出了 CSISE 算法, 该算法首先将待诊
断系统描述及观测用合取范式编码给出, 最后调用成熟的 SAT 求解器判断组件子集是否是冲突集 [14] , 然而该算法
需要遍历枚举树中大部分节点, 求解花费往往较高. 2013 年 Liffiton 等人 [15] 结合哈斯图提出了 MARCO 算法, 该
算法是求解极大化模型中枚举极小冲突集效率较高的算法, 但是它没有进一步对有解空间进行剪枝. 2016 年
Liffiton 等人 [16] 结合 eMUS 对该算法进行了优化, 在哈斯图未求解的空间中利用启发式策略优先选取极大节点, 进
而快速得到一个极小冲突集. 2019 年欧阳丹彤等人 [12] 在极大化模型 MARCO 算法基础上增加了中间模型, 利用中
间节点对冗余解进行剪枝, 缩小了求解范围. 2024 年蒋璐宇等人 [11] 提出了 MARCO-ABC 算法, 有效地利用极小冲
突集和极小碰集二元性关系, 大幅度减少了求解时间, 是目前求解极小冲突集最快的算法.
计算碰集方法主要是基于树, 2003 年姜云飞等人 [17] 提出 Boolean 算法, 通过深度优先规则, 把冲突集递归的
分成左右分支, 很多情况下都优于其他集中式算法, 后续有很多基于 Boolean 算法的优化策略被提出 [18] . 2015 年
Zhao 等人 [19] 提出了等价类概念, 通过连接关系把冲突集分成若干等价类, 缩减了问题规模的同时也省去了解集合
并时间. 同年 Jannach 等人 [20] 利用分布式思想把碰集算法并行化, 提高了求解效率. 2018 年刘思光等人 [21] 提出了
布尔结合增量独立覆盖策略 (Boolean with increment independent coverage checking, BWIICC) 算法, 利用独立覆盖
策略保证生成解的都是极小的, 大幅度减少解集极小化的时间. 2022 年赵相福等人 [22] 结合独立覆盖及增量策略提