Research On Problems Related To Model-based Diagnosis Combining The Structure Property

Model-based diagnosis(MBD)problem is a NP problem.MBD problem has a very important position in the field of artificial intelligence.At the same time,model-based diagnosis also has important applications in engineering,economics,aerospace and other fields.In the early stage,MBD problem is difficult to solve directly.So its solution is divided into two steps.The first step is to solve all the minimal conflict sets for the entire circuit.The second step is to solve all the minimal hitting sets with the minimal conflict sets.These minimal hitting sets are the minimal diagnoses for MBD problem.SAT problem is a very important research direction in the field of artificial intelligence.It is a NP problem.In the computer field,many problems,such as model-based diagnosis problems and automatic reasoning,can be solved with SAT method.It is an important technique for solving model-based diagnosis problem that converting diagnosis problem to SAT.The CSISE-tree method,combined with a flipping set enumeration tree,solves the minimal collision set using the SAT solver.It further improves the efficiency of solving minimal conflict sets.In this paper,according to the characteristics of the conflict sets,we use the enumeration tree to reconstruct the process of solving conflict sets and then design a reverse depth algorithm based on the previous algorithm CSISE-tree.Firstly,this proposed reverse depth search algorithm can reduce as many memory spaces as possible when obtaining some conflict sets,while CSISE-tree have to expend some unnecessary memory spaces in this case,where the consume of memory spaces exponentially grows with the number of circuit elements.Secondly,compared with CSISE-tree,our algorithm can effectively cut down the number of calling the SAT solver by pruning some non-minimal conflict sets and non-conflict sets.As the SAT solver efficiency increases,transforming the MBD problem into the SAT problem solving has gradually become one of the mainstream methods for solving the MBD problem.The LLBRS-tree method is an efficient way to solve the MBD problem using the SAT solver.This method uses a set enumeration tree to ensure thecompleteness of the algorithm.And it can only solve the diagnoses within the specified length which defined by ourselves.It also proposes the idea of reverse search,and took advantage of the structural features of the enumeration tree to prune the enumeration tree.It also uses the identification-rule,all the minimal diagnoses can be obtained directly after traversing all nodes.Based on the research of LLBRS-tree method,this paper proposes an ACDIAG method.If a circuit has multiple inputs but only one output,the circuit can be considered as a circuit component.ACDIAG method block the circuit,and each sub-circuit structure after the block is a binary tree,it may have multiple inputs,but only one output.Therefore,the ACDIAG method takes each sub-circuit as a component and abstracts the circuit.Then it calls the LLBRS-tree method to solve the abstracted circuit.Finally,based on the structural characteristics of the binary tree and the signal transmission relationship of the circuit component,ACDIAG method extends the diagnoses to obtain all the minimal diagnoses of the entire circuit.The block strategy proposed by the ACDIAG method reduces the size of the circuit from the circuit structure.In the diagnosis of the expansion,it can take advantage of the structural characteristics of the sub-circuit to quickly expand all the minimal diagnoses.The experimental results show that compared with LLBRS-tree method,ACDIAG method has obvious improvement on the efficiency of solving MBD problem.Experimental results show that the ACDIAG method is more efficient than the LLBRS-tree method in solving MBD problems.