命题可满足问题(propositional satisfiability problem,SAT)是人工智能领域的研究热点,也是数理逻辑及计算机研究中的核心问题,对人工智能发展起到了非常重要的推动作用。命题可满足问题擅长将一些艰难的故障求解转化为问题系统中命题公式是否存在可满足赋值的问题,并给出故障识别。极小不可满足集(minimal unsatisfiable subset,MUS)问题是命题可满足问题的扩展问题。在求解极小不可满足解时,通常将不可满足性问题转换为命题可满足问题,利用SAT求解器来给出是否一致可满足的判定。目前求解极小不可满足集效率较高的两种遍历结构为哈斯图和枚举树。哈斯图结构主要是利用图的逻辑结构构建节点之间的联系,适用于广泛的约束关系处理。图结构主要应用于关系规范调试、不一致检测、模型验证等问题中。极小冲突问题是极小不可满足问题在基于模型诊断上的应用,主要采用枚举树结构,利用树的特性对电路系统中元件集的全枚举进行遍历。相对于图结构遍历,树结构遍历求解极小冲突问题节点跳转方便,配合剪枝策略剪去枚举树中不需要遍历的节点使求解效率更快。在基于图结构求解方法中,MARCO方法是目前采用极大化模型求解MUS效率最高的方法,但此方法未对求解空间进行进一步有效剪枝。针对MARCO方法的不足,结合可满足问题求解复杂度低于不可满足问题的特征,提出基于双模型即极大-中间化模型的MARCO-MAM方法求解MUS。此方法对中间模型求解若得到极大可满足子集,则缩减MUS的无解空间,进而缩减未探索空间来提高MUS求解效率;如果中间模型求解得到不可满足集合,则减少了单一MUS的不可满足迭代求解次数。此方法避免了MARCO方法单一极大化模型求解MUS时未有效利用其他优化技术对求解空间进行剪枝的问题。实验结果表明,与MARCO方法相比MARCO-MAM方法效率较高,尤其在大规模问题或较大搜索空间时效率提高更为明显。在基于树结构求解极小冲突集问题中,MCS-SFFO方法以反向深度的方式遍历集合枚举树(Set Enumeration Tree,SE-Tree),然后针对故障输出无关元件的组合进行剪枝。本文在MCS-SFFO方法的基础上,结合电路的故障逻辑关系提出求解极小冲突集的进一步剪枝方法MCS-FLR,首先提出单元件非冲突集定理,对单元件集合进行剪枝,避免了对无解空间中单元件节点的访问;其次,提出非极小冲突集定理,推证得出故障输出相关元件集的超集都是冲突集,故对有解空间中的非极小解进行剪枝。MCS-FLR方法在MCS-SFFO方法基础上减少了大量有解空间和部分无解空间调用SAT求解器的次数,节省了求解时间。实验结果表明,相比于MCS-SFFO方法,MCS-FLR方法求解效率有显著提高。