Research On Model-based Diagnosis Method Based On Reverse Search Of Structural Features

Model-based diagnosis,an intelligent diagnosis reasoning technology is proposed to solve the major defect of the first-generation expert diagnosis system,which has been a popular research problem in the field of artificial intelligence.Model-based diagnosis using equipment internal topology structure and the circuit of the observed behavior knowledge to diagnosis,is called another revolution by the experts in the field of artificial intelligence,which plays an irreplaceable role in promoting the development of the entire artificial intelligence.After several decades of theoretical development,model-based diagnosis is becoming more and more widely used in practical applications.Such as medical system diagnosis,circuit fault diagnosis,automobile fault diagnosis,large-scale VHDL program fault diagnosis,network communication fault diagnosis.The classical method to solve the problem of model-based diagnosis involves a two-stage process to obtain the final diagnostic result.In the first step,conflict identification is generated for all the minimal hitting sets.In the second step,solve the minimal hitting sets according to the minimal conflict sets.These two steps play an important role in the process of obtaining diagnostic results.For the hitting set problem,the main solving methods are enumeration-based completeness algorithm and local search-based non-completeness algorithm.As more and more scholars have devoted themselves to model-based diagnosis,many new methods have emerged.The satisfiability problem(SAT)is also a very active branch of artificial intelligence.The SAT problem is the NP-complete problem,and it is already a common method to encode many NP-complete problems in artificial intelligence into SAT problem.In recent years,as the efficiency of the SAT solver has increased,model-based diagnostic problems have also been converted to SAT problem to solve.The SAT problem mainly uses the Conjunctive Normal Form(CNF)to represent the circuit.Therefore,when the problem of model-based diagnosis is converted to SAT problem,the logic gate is converted into a CNF file.In the process of using SAT problem to solve the problem of model-based diagnosis,how to combine the logical structure of the problem and how to reduce the number of calls to the SAT solver has become a hotspot of scholars at home and abroad.when determining whether a set of components in the diagnostic system is a diagnostic of the system,the main idea of CSSE-Tree algorithm proposed by Zhao Xiangfu is to describe the normal behavior of all the components in the complement of a given set of components,system description and observation as a CNF file,and then call the SAT solver to solve.On this basis,in order to get all the diagnostic solutions of the system,the CSSE-Tree algorithm combined with the set enumeration tree model,according to the number of components in the diagnostic system,enumerate all the power set of the component set and solve it one by one to get minimal diagnostic sets.However,when the number of components in the system is too large,the number of power sets will become very large,so the CSSE-Tree algorithm prunes the set enumeration tree with the true superset of the minimal diagnostic set must not be a minimal diagnostic set.However,after a deep study of the CSSE-Tree algorithm,we find that only a few nodes are pruned.In the set enumeration tree,a large number of nodes that are not diagnostic solutions still need to call the SAT solver for judgment.In order to solve the problem of pruning only nodes that are diagnostic solutions,combining the diagnostic problem and the characteristics of the SAT solution process,a new method is proposed by us in this paper to judge the candidate diagnosis in the set of enumerated trees,which can reduce the scale of the problem.According to the theory that the true subset of the non-diagnostic solution is not a diagnostic solution,we first propose the pruning strategy for the non-diagnostic solution space,and have achieved the pruning of the non-solution space.Based on SAT solver,combined with the set enumeration tree,using the reverse search and the non-solution space pruning strategy,we present a LLBRS-Tree(Last Level Based Reverse Search Tree,LLBRS-Tree)method in this paper.Experiment results show that compared with the algorithm of CSSE-Tree,the algorithm of LLBRS-Tree has less number of SAT solving,has smaller scale of the problem,better efficiency.Especially in solving multiple diagnostic examples,the effect of LLBRS-Tree is more significant.