基于模型诊断是一种智能诊断推理技术,旨在解决第一代专家诊断系统的重大缺陷,在人工智能领域内一直是热门研究课题之一。基于模型诊断利用设备的内部拓扑结构与观测行为知识进行诊断,被人工智能领域专家称为诊断理论和技术上面的又一革命,对整个人工智能的发展起着不可替代的推动作用。经过几十年的理论发展,基于模型诊断在实际的应用领域也越来越广泛。例如医学系统诊断、电路故障诊断、汽车故障诊断、大型VHDL程序的故障诊断、网络通讯故障诊断等。基于模型诊断问题的经典求解方法包括两阶段求解过程,得到最后的诊断结果。第一步,计算极小冲突集合;第二步,根据极小冲突集求解得到极小碰集。这两个步骤在得到诊断结果的过程中扮演中重要的作用。对于碰集问题,主要的求解方法有基于枚举的完备性算法和基于局部搜索的非完备性算法。随着越来越多的学者投入到基于模型诊断问题中,许多新的求解方法也涌现出来。可满足性问题(SAT问题)也是人工智能领域中很活跃的一个分支。SAT问题是NP-Complete问题,将人工智能领域中许多NP-Complete问题编码成SAT问题进行求解是常见的方法。近些年以来,随着SAT求解器效率的逐渐提高,基于模型诊断问题也被编码成SAT问题求解。SAT问题使用合取范式(CNF)表示电路,所以在将基于模型诊断问题编码成SAT问题的过程中,主要将逻辑门电路转换成CNF形式的文件。在使用SAT问题求解基于模型诊断问题时,如何结合问题的逻辑结构特征,给出更好的方法减少调用SAT求解器的次数成为了现在国内外学者的研究热点。在判断诊断系统中的一个组件集合是否是系统的诊断时,赵相福等学者提出的CSSE-Tree算法主要思想是将给定组件集合的补集中所有组件正常行为描述、观测描述和系统描述构造成一个CNF形式文件,然后调用SAT求解器进行求解。在此基础上,为了得到系统所有诊断解,CSSE-Tree算法结合集合枚举树模型,根据诊断系统中组件的个数,枚举出组件集合的所有幂集合,然后对幂集合进行逐个判断,求解最后的极小诊断解。但是,当系统中组件个数过多的时候,组件集合的幂集合个数会变得十分庞大,因此CSSE-Tree算法利用了极小诊断解的真超集一定不是极小诊断解的剪枝策略对集合枚举树进行剪枝。然而对CSSE-Tree算法进行深入研究后,本文发现只对极小诊断解的子孙结点进行剪枝剪掉的仅仅是少数结点。而在集合枚举树中,大量不是诊断解的结点仍然需要调用SAT求解器进行判断。针对仅对诊断解结点进行剪枝的不足,本文结合诊断问题和SAT求解过程的特征,提出了先对集合枚举树中包含组件个数较多的候选诊断进行判断的方法,从而减少求解问题的规模。根据非诊断解的真子集一定不是诊断解的理论基础,首次提出了对不是诊断解的空间也进行剪枝的策略,达到了对诊断的无解空间进行剪枝的优化。基于SAT求解器,结合集合枚举树模型,利用反向搜索以及有解无解空间剪枝策略,本文提出了基于反向搜索的有解无解空间剪枝方法LLBRS-Tree(Last Level Based Reverse Search Tree,LLBRS-Tree)。通过多方面的实验结果对比表明,算法LLBRS-Tree相比于算法CSSE-Tree,经过有解无解空间剪枝,有效减少了调用SAT求解器的次数,很大程度上减小了求解问题的规模,效率得到提高。尤其在求解多诊断实例时,算法LLBRS-Tree效果更加的显著。