论文部分内容阅读
基于模型诊断问题是NP难度的问题,在人工智能领域内有着十分重要的地位。同时,在工程医学、经济、航天等领域内,基于模型诊断问题也有着重要的应用。在早期提出基于模型诊断问题时,很难对其直接进行求解,于是将其求解分为了两步,第一步是对整个电路求解所有极小冲突集,第二步是对已经求得的所有极小冲突集求解所有极小碰集,这些极小碰集就是基于模型诊断问题的所有极小诊断解。SAT(Satisfiable)问题是人工智能领域内一个十分重要的研究方向,是一个NP问题。在计算机领域内,诸如基于模型诊断问题和自动推理等都能够转化为SAT问题后进行求解。CSISE-tree方法结合翻转的集合枚举树,使用SAT求解器求解极小冲突集,提高了求解效率。本文在CSISE-tree求解冲突集方法深入研究的基础上,根据冲突集求解特征重构了结合枚举树的计算冲突集的过程,提出基于深度优先反向搜索求解冲突集的方法。针对CSISE-tree方法求解时占用内存空间与元件总数指数级相关的缺点,构建反向深度搜索方法减小求解时所占用内存空间;针对CSISE-tree方法不能对部分非极小的冲突集进行剪枝的问题,给出对非冲突集和更多非极小的冲突集进行剪枝的CSRDSE(CS Reverse Depth SE-tree)方法,有效减少了求解时调用SAT(Boolean SATisfiability problem)求解器的次数。随着SAT求解器效率的不断提高,把基于模型诊断问题转化为SAT问题求解的方法已经逐渐成为求解基于模型诊断问题的主流方法之一。LLBRS-tree方法是使用SAT求解器求解基于模型诊断问题效率较高的一种方法。此方法使用集合枚举树作为辅助求解工具,保证了算法的完备性,并且能够自定义极小诊断解的最大长度,不必对长度过大的诊断进行求解。此方法还提出了反向搜索的思想,并利用了集合枚举树的结构特征,对枚举树进行剪枝。同时,此方法还采用了标识规则,在对所有节点遍历完毕后能够直接得到所有极小诊断解。基于LLBRS-tree方法的研究,本文提出电路分块诊断方法ACDIAG(Abstract Circuit Diagnosis)方法。若一个电路有多个输入,但只有一个输出,则可以将这个电路看作一个电路元件。ACDIAG方法对电路进行分块,分块后每一个子电路的结构都是二叉树。每个子电路可能存在多个输入,但输出只有一个。因此,ACDIAG方法是将每个子电路看成一个元件对电路进行抽象,并调用LLBRS-tree方法对抽象后的电路进行求解。最后根据二叉树的结构特点和逻辑电路元件的信号传递关系,对已经求得的诊断解快速扩展,得到整个电路的所有极小诊断解。ACDIAG方法提出的分块策略,从电路结构上缩减了电路的规模。同时在对诊断解扩展方面,其能够利用子电路的结构特点,在短时间内快速扩展出所有极小诊断解。实验结果表明,ACDIAG方法比LLBRS-tree方法求解MBD问题的效率更高。