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

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

作　　者：欧阳丹彤[1,2,3] 周建华[1,3] 刘伯文[2,3] 张立明[1,2,3] 

机构地区：[1]吉林大学软件学院,长春130012 [2]吉林大学计算机科学与技术学院,长春130012 [3]符号计算与知识工程教育部重点实验室(吉林大学),长春130012

出　　处：《计算机研究与发展》2017年第3期502-513,共12页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61672261;61502199;61402196;61272208);浙江省自然科学基金项目(LY16F020004)~~

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

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

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]