ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2017, Vol. 54 ›› Issue (3): 502-513.doi: 10.7544/issn1000-1239.2017.20150952

Previous Articles     Next Articles

A New Algorithm Combining with the Characteristic of the Problem for Model-Based Diagnosis

Ouyang Dantong1,2,3, Zhou Jianhua1,3, Liu Bowen2,3, Zhang Liming1,2,3   

  1. 1(College of Software, Jilin University, Changchun 130012); 2(College of Computer Science and Technology, Jilin University, Changchun 130012); 3(Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012)
  • Online:2017-03-01

Abstract: Model-based diagnosis has been popular in the field of artificial intelligence. In recent years, with a gradual increase of the efficiency of SAT solvers, model-based diagnosis is converted into SAT problem. After deeply studying CSSE-tree algorithm—a method for solving model-based diagnosis, combining with the characteristics of diagnose problem and SAT solving process, we solve the problem by diagnosing the candidate solutions which contain more elements first, thereby reducing the scale of SAT problem. Based on the minimal diagnostic solutions and non-minimal pruning methods on diagnostic solutions, we firstly propose a non-diagnostic solution theorem and a non-solution space pruning algorithm, which implements the non-solution space pruning effectively. We first solve the candidate solutions which contain more elements. According to the features of solution and non-solution method, we construct LLBRS-tree method based on reverse search. Experimental 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 when solving multiple diagnose problems its efficiency is more significant.

Key words: model-based diagnosis, non-solution space pruning, conjunctive normal form, SAT solver, set-enumeration-tree

CLC Number: