Efficient zonal diagnosis with maximum satisfiability  

作　　者：Meng LIU Dantong OUYANG Shaowei CAI Liming ZHANG 

机构地区：[1]College of Computer Science and Technology, Jilin University [2]Key Laboratory of Symbolic Computation and Knowledge Engineering, Ministry of Education,Jilin University [3]State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

出　　处：《Science China(Information Sciences)》2018年第11期13-26,共14页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61672261, 61502199, 61402196, 61272208)

摘　　要：Model-based diagnosis(MBD) has been widely acknowledged as an effective diagnosis paradigm.However, for large scale circuits, it is difficult to find all cardinality-minimal diagnoses within a reasonable time. This paper proposes a novel method that takes a significant step in this direction. The idea is to divide a circuit into zones and compute the cardinality-minimal diagnoses by finding subset-minimal diagnoses with cardinality-minimal via a maximum satisfiability(MaxSAT) solver on an abstracted circuit that is composed of these zones instead of all components. We also propose a new propagate-extend method for extending the seed-TLDs to obtain all cardinality-minimal diagnoses efficiently. We implement our method with a state-of-the-art core-guided MaxSAT solver, and present evidence that it significantly improves the diagnosis efficiency on ISCAS-85 circuits. Our method outperforms SATbD, which was recently shown to outperform most complete MBD approaches using satisfiability(SAT).Model-based diagnosis(MBD) has been widely acknowledged as an effective diagnosis paradigm.However, for large scale circuits, it is difficult to find all cardinality-minimal diagnoses within a reasonable time. This paper proposes a novel method that takes a significant step in this direction. The idea is to divide a circuit into zones and compute the cardinality-minimal diagnoses by finding subset-minimal diagnoses with cardinality-minimal via a maximum satisfiability(MaxSAT) solver on an abstracted circuit that is composed of these zones instead of all components. We also propose a new propagate-extend method for extending the seed-TLDs to obtain all cardinality-minimal diagnoses efficiently. We implement our method with a state-of-the-art core-guided MaxSAT solver, and present evidence that it significantly improves the diagnosis efficiency on ISCAS-85 circuits. Our method outperforms SATbD, which was recently shown to outperform most complete MBD approaches using satisfiability(SAT).

关 键 词：model-based diagnosis MaxS AT subset-minimal diagnoses cardinality-minimal diagnoses zone propagate-extend 

分 类 号：N[自然科学总论]