ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2017, Vol. 54 ›› Issue (3): 502-513.doi: 10.7544/issn1000-1239.2017.20150952

• 人工智能 • 上一篇    下一篇

基于模型诊断中结合问题特征的新方法

欧阳丹彤1,2,3,周建华1,3,刘伯文2,3,张立明1,2,3   

  1. 1(吉林大学软件学院 长春 130012); 2(吉林大学计算机科学与技术学院 长春 130012); 3(符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (15943054244@163.com)
  • 出版日期: 2017-03-01
  • 基金资助: 
    国家自然科学基金项目(61672261,61502199,61402196,61272208);浙江省自然科学基金项目(LY16F020004)

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

摘要: 基于模型诊断一直是人工智能领域中热门的研究问题.近些年来,随着SAT求解器效率的逐渐提高,基于模型的诊断也被转换成SAT问题进行求解.在对基于模型诊断求解方法CSSE-tree深入研究基础上,结合诊断问题和SAT求解过程的特征,给出先对包含组件个数较多的候选诊断进行求解的方法,进而减小SAT求解问题的规模;在对极小诊断解和非极小诊断解剪枝方法的基础上,首次提出非诊断解定理及非诊断解空间的剪枝方法,有效地实现了对诊断的无解空间进行剪枝.根据组件个数较多的候选诊断先求解及有解无解剪枝方法特征,构建基于反向搜索的LLBRS-tree方法.实验结果表明:与CSSE-tree算法相比,LLBRS-tree算法减少了SAT求解次数、减小了求解问题规模,效率较好,尤其是求解多诊断时效率提高更为显著.

关键词: 基于模型的诊断, 无解空间剪枝, 合取范式, SAT求解器, 枚举树

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

中图分类号: