摘要：基于模型诊断（model‐baseddiagnosis，MBD）是人工智能领域一个极富有挑战性的问题．近年来，SAT求解器发展十分迅速，且已被应用于求解基于模型诊断问题并取得了显著成果．在对基于模型诊断问题求解方法LLBRS‐Tree深入研究的基础上，根据电路组件的拓扑结构信息、系统的观测行为和预期行为之间的差异以及集合枚举树的特点，首次提出了组件静态伪故障度和动态伪故障度的概念．计算所有组件的静态伪故障度，并根据静态伪故障度从大到小对组件重新排序，生成新的枚举树；并且在遍历到新的极小诊断解时，更新相关组件的动态伪故障度，动态建立新的枚举树，从而能较快地搜索到极小诊断解，删除大量冗余解，较大程度地减少SAT求解器的调用次数．实验结果表明：随着诊断系统中组件个数的增多以及极小诊断解长度的增加，提出的方法较LLBRS‐Tree方法效率提升明显．
关键词：基于模型诊断；静态伪故障度；动态伪故障度；枚举树；极小诊断解
基于模型诊断（model‐baseddiagnosis，MBD）问题对人工智能领域的发展具有十分重要的推动作用［１］．其主要思想是根据设备的内部结构和行为来诊断该设备，从模型和观测出发推理出设备的故障组件，解释预期行为和观测行为之间的差异．基于模型诊断过程主要分为３个步骤：１）诊断产生．已知一个差异，决定可能失灵的组件导致该差异．２）诊断测试．测试诊断过程中产生的所有诊断解，找出能够解释设备所有观测的组件集合．３）诊断辨别．若有多个诊断通过测试，搜集额外信息以得到最后的诊断解．
著名MBD专家Reiter［２］提出了根据极小冲突集求解极小碰集（即系统的极小诊断解）的方法HS‐Tree，但该方法要遍历整棵枚举树，导致诊断空间很大且会因剪枝丢失诊断解．针对这些缺点，Greiner等人［３］提出了改进方法HS‐DAG，解决了HS‐Tree的丢解问题．随着对MBD问题深入的探索和研究，许多新的方法被提出．Stein等人［４］提出的诊断方法允许待诊断系统的组件及其行为有缺省信息，并用合理的假设表示系统的异常行为，有效地提升了该方法对特定问题的求解效率．赵相福等人［５］提出了CSISE‐Tree方法，在对集合枚举树进行剪枝优化的基础上求出诊断系统所有的诊断解．欧阳丹彤等人［６］提出了利用标志传播求解系统所有候选解的方法，通过传播系统的输出标志来判断组件集合是否是诊断解．Schmitz等人［７］利用部分诊断解优化冲突集，并提出了根据极小冲突集求诊断解的时序诊断方法．
近年来，命题可满足问题（propositionalsatis‐fiabilityproblem，SAT）受到国内外学者的广泛关注［８］．Cook［９］于１９７１年首次证明SAT问题是NP完全问题，人工智能领域的很多NP问题都可以转化成SAT问题求解［１０］且研究表明，与直接求解NP问题相比，将其转化成SAT问题后求解更加高效．一些优秀的求解引擎已被广泛应用于布局布线、自动测试矢量、电路等价性验证、智能规划等［１１］领域．随着对MBD问题研究的深入，发现该问题也可以转换成SAT问题求解且已取得显著成果．
基于SAT求解器的发展，国内外许多学者开始投入到结合SAT求解诊断的研究领域中．Feldman等人［１２］提出利用带权重的MaxSat求解MBD，该方法将子句分为hard子句和soft子句，并对子句赋予权重，最终要求满足子句权重乘积之和最大，进而得到所有诊断解．Metodi等人［１３］提出了一种新的编码方式，将MBD编码成布尔可满足问题来求解，并对诊断系统进行了复杂的预处理．Marques‐Silva等人［１４］提出将MBD转成MaxSat问题求解的方法，根据阻塞结点和边、过滤结点和边缩减诊断系统规模，减小诊断系统求解空间．国内学者周建华等人［１５］利用SAT求解器结合LLBRS‐Tree算法求出诊断系统所有的极小诊断解，此方法是目前基于枚举树结构利用SAT求解诊断效率较高的方法．
LLBRS‐Tree方法从叶结点开始向上遍历枚举树直到根结点为止，同时基于非诊断解的祖先结点一定不是诊断解进行无解剪枝［１５］以及诊断解的子孙结点一定不是极小诊断解进行有解剪枝［１５］，通过有解剪枝和无解剪枝剪掉大量结点．本文在LLBRS‐Tree方法的基础上进行了改进，提出了根据组件的静态伪故障度和动态伪故障度生成枚举树，动态更新枚举树遍历顺序进行剪枝的方法DYN‐Tree．该方法计算每个组件发生故障的概率（记为静态伪故障度），根据组件的静态伪故障度生成枚举树，当调用SAT求解器求得一个组件集合是极小诊断解时，更新该集合中组件的动态伪故障度，重新动态生成新的枚举树遍历顺序，对新生成的枚举树进行有解剪枝和无解剪枝，直到求得诊断系统的所有极小诊断解为止．该方法能够较早地发现极小诊断解，裁剪掉大量冗余的诊断解．
1预备知识
本节首先介绍一些基于模型诊断的相关概念，然后介绍如何将基于模型诊断问题转化成SAT问题求解．
立即询价
