融合基数约束与单次入队的基于模型诊断方法  

A Model-Based Diagnosis Method for Integrating Cardinality Constraints and Enqueueing at Once

作　　者：青杨 欧阳丹彤[1,2] 周慧思 张立明[1,2] Qing Yang;Ouyang Dantong;Zhou Huisi;Zhang Liming(College of Computer Science and Technology,Jilin University,Changchun 130012;Key Laboratory of Symbol Computation and Knowledge Engineering(Jilin University),Ministry of Education,Changchun 130012)

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]符号计算与知识工程教育部重点实验室(吉林大学),长春130012

出　　处：《计算机研究与发展》2025年第2期408-417,共10页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(62076108,61872159);吉林省教育厅项目(JJKH20211106,JJKH20211103KJ)。

摘　　要：基于模型诊断(MBD)方法在不同的环境中有越来越多的用途,包括软件故障定位、电子表格的调试、Web服务和硬件设计,以及生物系统的分析等.受这些不同用途的启发,近年来MBD算法改进成效显著.然而,对体系庞大、结构复杂的系统,需要对现有方法进一步改进.由于求解诊断解在计算上具有挑战性,因此相继提出了一些通过压缩模型的MBD算法来提高诊断效率,如基于统治的多观测压缩模型(dominated-based compacted model with multiple observations,D-CMMO)算法.对于给定多个观测值且注入1个以上错误需要大量时间的诊断问题,提出了一个新的诊断模型CCM(cardinality-constrained compacted model)来解决.基于基数约束的压缩模型算法使用2种方法对求解过程进行优化:首先,利用系统观测的故障输出和故障组件数量之间的约束关系来限制目标解的范围;其次,通过对假设集采用单次入队方法,进而有效提升MaxSAT(maximum satisfiability)求解器的性能.此外,在ISCAS85和ITC99基准测试用例上的实验结果表明,与目前最新的MBD求解方法D-CMMO相比,上述2种优化方法有效缩小了MBD问题的求解范围,降低MaxSAT求解器搜索目标解的难度,进而能在更短的时间内返回一个诊断解.在平均状况下,CCM方法相比D-CMMO方法求解效率分别提升64.5%和92.8%.Model-based diagnosis(MBD)finds a growing number of uses in different settings.It includes software fault localization,debugging of spread sheets,Web services,and hardware designs,and also the analysis of biological systems,among many others.Motivated by these different uses,there have been significant improvements made to MBD algorithms in recent years.Nevertheless,the analysis of larger and more complex systems motivates further improvements to existing approaches.Since computing diagnosis is computationally challenging,some MBD algorithms by compacting the model are presented successively,such as dominated-based compacted model with multiple observations(D-CMMO)approach.In this paper,we propose one new diagnosis model,namely,cardinalityconstrained compacted(CCM)model,to solve the problem in which a considerable amount of time is needed when multiple observations are given and more than one fault is injected.CCM uses two methods to optimize the process of solving MBD.Firstly,we propose to utilize relationship of faulty system-outs and faulty components to limit the scope of target solution.Secondly,the performance of the MaxSAT(maximum satisfiability)solver is effectively improved by enqueueing all assumptions at once.Furthermore,experiment evaluations on ISCAS85 and ITC99 benchmarks show that compared with D-CMMO,the latest encoding algorithms for MBD,the above two optimization methods effectively reduce the scope of MBD problem,reduce the difficulty of searching for the target solution by the MaxSAT solver,and thus return diagnostic solution in a shorter time.On average,the solving efficiency of CCM method is improved by 64.5%and 92.8%compared with D-CMMO method respectively.

关 键 词：基于模型诊断 压缩模型 基于基数约束的算法 顶层诊断解 单次入队 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]