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

来源：计算机研究与发展杂志2017年第3期北京时间：

作者：欧阳丹彤,周建华,刘伯文,张立明,

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

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