计算机研究与发展 ›› 2017, Vol. 54 ›› Issue (3): 502-513.doi: 10.7544/issn1000-1239.2017.20150952
欧阳丹彤1,2,3,周建华1,3,刘伯文2,3,张立明1,2,3
Ouyang Dantong1,2,3, Zhou Jianhua1,3, Liu Bowen2,3, Zhang Liming1,2,3
摘要: 基于模型诊断一直是人工智能领域中热门的研究问题.近些年来,随着SAT求解器效率的逐渐提高,基于模型的诊断也被转换成SAT问题进行求解.在对基于模型诊断求解方法CSSE-tree深入研究基础上,结合诊断问题和SAT求解过程的特征,给出先对包含组件个数较多的候选诊断进行求解的方法,进而减小SAT求解问题的规模;在对极小诊断解和非极小诊断解剪枝方法的基础上,首次提出非诊断解定理及非诊断解空间的剪枝方法,有效地实现了对诊断的无解空间进行剪枝.根据组件个数较多的候选诊断先求解及有解无解剪枝方法特征,构建基于反向搜索的LLBRS-tree方法.实验结果表明:与CSSE-tree算法相比,LLBRS-tree算法减少了SAT求解次数、减小了求解问题规模,效率较好,尤其是求解多诊断时效率提高更为显著.
中图分类号: