软件学报

作者：欧阳继红，黄森

单位：欧阳继红，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,黄森，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001202

关键词：基于模型诊断;系统描述;极小冲突集;极小碰集;等价类

基金：吉林省煤炭洁净燃烧技术的环境保护装备项目(3D516L921421)

在基于模型诊断领域中, 首先对系统描述进行编码, 利用成熟的SAT求解器获得所有极小冲突集, 最后计算极小冲突集的极小碰集, 即待诊断设备的候选诊断. 然而这种策略花费大量的时间, 相当于计算两个NP-hard问题, 即计算极小冲突集和极小碰集. 对电路系统描述重新编码, 提出一种变种碰集算法HSDiag, 该算法可以直接对编码进行计算来获得诊断. 在与目前最先进的求解冲突集再求解碰集的诊断算法相比, 效率最高提升5–100倍. 随着电路组件的增多, 编码子句呈线性增加, 诊断数量呈指数级增加. 因为求解大规模电路(ISCAS-85)的所有冲突集不切实际, 所以在设置相同的截止时间内, 提出的HSDiag算法与基于冲突集的诊断算法相比多求出1倍以上的解集. 除此之外, 提出一种专属求解诊断的等价类优化策略, 就算在初始冲突集不可分割的情况下, 利用新提出的集合分裂规则能够对冲突集进一步分解. 在标准的Polybox和Fulladder电路中, 使用等价类优化后的HSDiag算法, 效率进一步提升2倍以上.

来源：2025年第12期

《软件学报》期刊编辑部

查看软件学报杂志2025年第12期