徐旖旎 欧阳丹彤 刘 梦 张立明 张永刚

(吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (jlxuyini@126.com)

基于模型诊断(model-based diagnosis)一直是人工智能领域中的重要研究方向，对人工智能领域的发展起到了至关重要的作用[1].模型诊断方法包括基于冲突的求诊断方法和直接求诊断方法.基于冲突的求诊断方法主要分为2个步骤:1)求出极小冲突集;2)求解极小冲突集的极小碰集，即为诊断解.直接求诊断方法就是利用SAT(satisfiability)求解器直接求出诊断解，而不需要产生极小冲突集[2].

在基于模型诊断问题中，求解极小冲突集是求诊断解的重要步骤之一.Reiter[3]最早采用冲突部件集的概念来计算极小诊断.早期许多专家使用定理证明器的方法求解极小冲突.Genesereth[4]提出用DART(device-independent diagnostic program)方法进行冲突识别.Haenni[5]在计算冲突集时使用归结的方法.但传统定理证明器效率较低，因此这些方法的实际应用并不广泛.

国内学者也对冲突识别做出相关研究，如栾尚敏等人[6]提出利用系统结构信息求解极小冲突集的方法，方敏[7]提出先离线求冲突然后在线求极小冲突的方法.然而，这些算法效率较低且通用性差，因此没有得到广泛应用.20世纪90年代Hou[8]首次提出了利用枚举树求解极小冲突集的CS-Tree算法，但其算法由于剪枝策略会造成丢失解.2006年和2009年赵相福等人在CS-Tree，Inverse CS-Tree，CS-Tree with Mark Set[9]的基础上分别提出2种改进算法CSSE-Tree[10]和CSISE-Tree[11],并首次使用SAT求解器求解冲突集，使得算法效率大大提高.刘伯文等人[12]在CSISE-Tree算法上进行改进，提出利用集合枚举树SE-Tree反向深度求冲突集的算法CSRDSE.CSISE-Tree算法主要针对非冲突集进行剪枝；而CSRDSE算法不仅对非冲突集进行剪枝，且根据冲突集的真超集一定不是极小冲突集的思想对某些能够确定的非极小冲突集进行剪枝，减少了使用SAT求解器的次数，进一步提高了求解极小冲突集的效率.

本文在对CSRDSE算法分析的基础上，提出结合故障输出结构特征的极小冲突求解算法MCS-SFFO(computing minimal conflict sets based on the structural feature of fault output).在MCS-SFFO算法中提出非冲突集定理——故障输出无关元件集的子集不是冲突集，即与异常输出不相关的元件任意组合都不是冲突集.因此，对故障输出无关元件的任意组合都不需调用SAT求解器进行判定.该算法在CSRDSE算法的基础上进一步对集合枚举树进行无解空间的剪枝，从而减小SAT求解问题的规模.

1 预备知识

本节首先介绍基于模型诊断的相关定义和概念，然后介绍SAT问题的基本概念.

1.1 基于模型诊断

定义1. 诊断系统[3].诊断系统是可用三元组(SD，COMPS，OBS)表示，分别是系统描述、元件集、观测集.

定义2. 基于一致性诊断[3].设Δ⊆COMPS，称Δ为关于(SD，COMPS，OBS)的基于一致性诊断，如果SD∪OBS∪{AB(c)|c∈Δ}∪{AB(c)|c∈COMPSΔ}是一致的.

称Δ为极小诊断当且仅当对于Δ的任一真子集Δ′，Δ′都不是一个基于一致性的诊断.

定义3. 冲突集[3].系统(SD，COMPS，OBS)的冲突集CS是一个元件集合{c1，c2，…，ck}⊆COMPS，使得SD∪OBS∪{AB(c1)，AB(c2),…,AB(ck) }不一致.

称某个冲突集为极小冲突集，当且仅当该冲突集的任意真子集都不是冲突集[8].

1.2 SAT问题

我们用xi(i=1,2,…,n)表示布尔变量.xi或xi称作文字，其中，xi称作变量xi的正文字，xi称作变量xi的负文字.X={x1,x2,…,xn}表示变量的集合.Qi(i=1,2,…,m)表示子句，每一个子句是一组文字的析取式.符号Φ代表CNF公式，CNF公式是由子句的合取构成，即合取范式CNF:Φ=Q1∧Q2∧…∧Qr，而SAT问题就是寻找是否存在一组X的赋值，使其满足CNF公式.

定义4. SAT问题[13].SAT问题通常是指合取范式的可满足问题.

2 利用SE-Tree反向深度求解冲突集算法

第1节介绍了冲突集的概念，根据冲突集的定义可以得到2个结论：

推论1. 当元件集C是冲突集时，C的任意严格超集都是非极小冲突集[12].

推论2. 当元件集C不是冲突集时，C的任意真子集都不是冲突集[12].

通过推论可知，对冲突集的所有严格超集以及非冲突集的所有真子集可不必再进行判断.

本节介绍的SE-Tree反向深度求解冲突集算法就是运用了上述2个推论思想对集合枚举树进行剪枝，接下来介绍该算法的相关概念和算法思想.

2.1 相关概念

定义5. 集合枚举树[14].给定集合S，以树结构形式按一定顺序枚举出S中元素的所有组合，称这样的树为集合枚举树.

设节点N为枚举树中要遍历的节点，下面介绍3条剪枝规则和标识规则.

剪枝规则1[12]. 当N是冲突集时，将N加入到冲突集合簇中.

若N是以其父节点为根节点的子树上最左侧分支上的节点，则跳转至其父节点；否则，跳转至以N的下一个兄弟节点为根的子树的最左节点.

若N没有下一个兄弟节点(此时N是叶节点)，则跳转到下一个叶节点.

剪枝规则2[12]. 当N不是冲突集时，将N加入到非冲突集合簇中.

若N是经过下面节点回溯到的节点，则跳转至N的最左侧子节点的下一个兄弟节点为根节点的子树的最左节点；否则，跳转至其下一个兄弟节点.

若N没有下一个兄弟节点(此时N是叶节点)，则跳转到下一个叶节点.

剪枝规则3[12]. 当对N调用SAT求解器前，首先判断N是否为非冲突集合簇中集合的子集.若是，按照剪枝规则2跳转到下一个节点；否则，对N调用SAT求解器.

标示规则[12]. 当N是冲突集时，将N加入到冲突集合簇中，将其标示“0”，并将冲突集合簇中N的超集标示“1”.

2.2 CSRDSE算法

CSRDSE算法的主要思想就是基于剪枝规则和标识规则在反向遍历集合枚举树时对树进行剪枝.该算法伪代码如下：

算法1. CSRDSE.

①Node=SE-Tree的最左节点；

② While (Node≠∅)

③notCS=isunsolve(Node)；

④ If (notCS=0)

⑤judge←ISCS()；

⑥ If (judge=0)

⑦addtosolve(Node)；

⑧ 按照剪枝规则2给Node赋值；

⑨ Else

⑩addtosolve(Node)；

3 CSRDSE剪枝规则的改进

设节点Leaf是SE-Tree中的一个叶节点，下面介绍2个定义.

定义6. 同层兄弟节点.设节点F是SE-Tree的一个节点，若节点F与叶节点Leaf在集合枚举树中处于同层，且节点F是叶节点Leaf同层中相邻的下个节点，则称F为Leaf的同层兄弟节点.

如图1中{c1,c2,c5}的同层兄弟节点是{c1,c3,c4}.

Fig. 1 SE-Tree of {c1,c2,c3,c4,c5}图1 {c1,c2,c3,c4,c5}对应的集合枚举树

定义7. 子叶节点.设节点F是叶节点Leaf的同层兄弟节点，若Leaf与F之间存在叶节点，称这些叶节点是Leaf的子叶节点.

如图1中{c1,c2,c4,c5}的子叶节点是{c1,c2,c5}.

下面介绍算法CSRDSE中剪枝规则1的改进.

第2节我们提到，在算法CSRDSE剪枝规则2中，当叶节点不是冲突集时，跳转至下一个叶节点进行判断.例如图1所示的SE-Tree中，当{c1,c3,c4,c5}不是冲突集时，需要跳转至其子叶节点{c1,c3,c5}，{c1,c4,c5}，{c1,c5}进行判断.但通过观察可发现{c1,c3,c5}，{c1,c4,c5}，{c1,c5}都是{c1,c3,c4,c5}的子集，因此当{c1,c3,c4,c5}不是冲突集时，根据推论2可知，它的子叶节点也不是冲突集，因此可省去对{c1,c3,c4,c5}子叶节点的判断，直接跳转至{c2,c3,c4,c5}进行判断.

设叶节点Leaf的所有子叶节点组成的集合为SUB_LEAVES.通过进一步观察可知，在集合枚举树中，SUB_LEAVES中的所有元素都是叶节点Leaf的真子集.因此，当节点F不是冲突集时，SUB_LEAVES中的任一元素都不是冲突集，因此可省去对SUB_LEAVES中所有元素的判断，直接跳转至以叶节点Leaf的同层兄弟节点为根节点的最左节点进行判断.

通过分析，剪枝规则1可改为：若N没有下一个兄弟节点，则跳转到以其同层兄弟节点为根节点的子树的最左节点.

为方便阐述，本文将改进剪枝规则后的CSRDSE算法称为CSRDSE 2.

在算法CSRDSE剪枝规则3中规定，在对某节点调用SAT求解器前，首先判断其是否为非冲突集的子集.通过改进的剪枝规则2可知，当叶节点不是冲突集时，不必再判断其子叶节点是否为非冲突集的子集，因此，可减少遍节点的次数，同时也减少了对非冲突集合簇的检测次数.

对本节提出的改进策略的最坏情况和最好情况进行分析，结论如下：

1) 最坏情况.当SE-Tree的所有叶节点都是冲突集时，使用算法CSRDSE 2遍历集合枚举树时并不能跳过叶节点的子叶节点，此时，算法CSRDSE 2与算法CSRDSE访问节点次数相同，因此改进策略失效.

2) 最好情况.当SE-Tree的所有叶节点都不是冲突集时，使用算法CSRDSE 2在访问完最左节点后算法结束，因此算法CSRDSE 2访问节点的次数为1.而算法CSRDSE仍需遍历全部叶节点，因此当系统元件总数为n时，算法CSRDSE访问节点的次数是2n-1，为整棵枚举树节点总数的一半.此时，算法CSRDSE 2与算法CSRDSE相比，减少了对SE-Tree中一半节点的访问，同时，还避免了2n-1-1次与非冲突集合簇的检测.

4 结合故障输出结构特征的极小冲突求解算法

CSRDSE 2算法优化了求解空间，但是进一步分析可知，与异常输出端无关的电路元件间的任意组合都不是冲突集.因此，本节在CSRDSE 2算法基础上，提出在SE-Tree中对这些与异常输出无关的电路元件间的所有组合进行剪枝，进一步缩小了SAT求解问题的规模.下面给出结合故障输出结构特征的极小冲突求解算法的相关概念和算法思想.

4.1 相关概念

定义8. 故障输出元件.对于三元组{SD,COMPS,OBS}，若存在元件c∈COMPS，c的输出是诊断系统的输出，且该输出是系统的故障输出，即该输出的观测值与预期不符，则称元件c是该系统的故障输出元件.

定义9. 故障输出相关元件集.对于故障输出元件c，称从电路输入到c的路径上经过的元件(包含c)是故障输出相关元件.系统中所有故障输出相关元件组成的集合是系统的故障输出相关元件集.

定义10. 故障输出无关元件集.设集合S是系统的故障输出相关元件集，称集合COMPSS为系统的故障输出无关元件集.

为了更好地理解相关定义，下面用C17电路来举例说明.如图2所示：

Fig. 2 C17 circuit图2 C17电路

在C17电路中，假设输出端12输出异常、输出端13输出正常，则c4是故障输出元件.故障输出相关元件集为{c1，c2，c3，c4}，故障输出无关元件集是{c5，c6}.

4.2 求解故障输出无关元件集算法

算法2.GetCompS(SD.cnf，OBS.cnf).

① 初始化：outABCompS=∅；

EXP_OUT=∅；

onABCompS=∅；

unOnABCompS=∅；

COMPS，从SD.cnf的第1行中获取；

OBS_IN，从OBS.cnf中获取；

OBS_OUT，从OBS.cnf中获取；

②EXP_OUT←getExp(SD.cnf，OBS_IN，COMPS)；

③ While (OBS_OUT中仍有未与EXP_OUT对比的元素)

④ If (OBS_OUT[i]≠EXP_OUT[i])

⑤outABCompS.add(输出是

OBS_OUT[i]的故障输出元件)；

⑥ EndIf

⑦ EndWhile

⑧ While(outABCompS中有未判断的元素outComp)

⑨onABCompS.add(与outComp连接的元件)；

⑩ EndWhile

在算法2中，将系统描述、输入观测和系统所有元件正常表示的CNF形式输入SAT求解器中，求出预期输出EXP_OUT(行②)；将预期输出与实际输出对比，求出故障输出元件集outABCompS(行③～⑦)；通过系统描述，求出故障输出相关元件集onABCompS(行⑧～⑩)；最后求出故障输出无关元件集unOnABCompS并返回(行～).

4.3 结合故障输出结构特征的极小冲突求解算法

定理1. 非冲突集定理：系统的故障输出无关元件集的子集不是冲突集.

证明. 反证法.设UNABCS是系统故障输出无关元件集的任一子集.若UNABCS是冲突集，则根据定义3，当UNABCS中所有元件正常时系统的输出与系统实际输出不一致，即与UNABCS相关的所有输出中至少有一个是系统的故障输出.而根据定义10可知，与UNABCS相关的所有输出是系统的正常输出，故二者矛盾.因此，UNABCS不是冲突集.

证毕.

根据定理1我们可以进一步优化CSRDSE 2算法.在构造集合S的SE-Tree时，将故障输出相关元件放在S的前半部分，故障输出无关元件放在S的后半部分.例如，系统元件集为{c1,c2,c3,c4,c5},其中故障输出相关元件集为{c2,c4}，故障输出无关元件集为{c1,c3,c5}，其集合枚举树如图3所示.

而通过观察可知，树中以{c1}，{c3}，{c5}为根节点的分支子树中的所有节点恰好是故障输出无关元件集{c1,c3,c5}的所有非空子集.因此，根据非冲突集定理，可将以{c1}，{c3}，{c5}为根节点的分支子树剪枝，得到新的枚举树如图4所示.

Fig. 3 SE-Tree图3 集合枚举树

Fig. 4 SE-Tree after pruning图4 剪枝后的集合枚举树

通过上述分析可知，在用CSRDSE 2算法遍历SE-Tree的过程中，当遍历到的节点是故障输出无关元件集的子集时，便可终止遍历这棵树，因为剩余的所有节点都是故障输出无关元件集的子集，不是冲突集.下面给出结合故障输出结构特征的极小冲突求解算法MCS-SFFO.

算法3. MCS-SFFO算法.

输入：系统描述的CNF文件SD.cnf、系统观测的CNF文件OBS.cnf、故障输出相关元件集onABCompS、故障输出无关元件集unOnABCompS；

输出：极小冲突集合簇MCSRes.

①CSRes=∅，unCSRes=∅，Node=∅；

② 生成集合{onABCompS[0],onABCompS[1],…,onABCompS[NUM1-1],unOnAB-CompS[0],unOnABCompS[1],…,unOnABCompS[NUM2-1]}的集合枚举树CSTree.其中，NUM1是onABCompS[]的元素个数，NUM2是unOnABCompS的元素个数；

③Node赋值为CSTree的最左节点；

④ While (Node≠∅)

⑤ If (Node⊆unOnABCompS)

⑥ Break；

⑦ Else

⑧ If (Node是unCSRes元素的子集)

⑨ 按照剪枝规则1给Node赋值；

⑩ Else

算法3按照故障输出相关元件在前、故障输出无关元件在后的顺序生成集合枚举树CSTree(行②)，并将CSTree的最左节点赋值给Node(行③).每次迭代节点Node时先判断Node是否为故障输出无关元件集的子集(行⑤)，若是则跳出循环(行⑥)；否则，继续使用算法CSRDSE 2遍历CSTree(行⑧～).当遍历完CSTree后，将冲突集合簇中标识为“0”的冲突集加入到极小冲突集合簇MCSRes中(行～)，最后返回MCSRes.

根据算法3的描述可知，算法3是完备算法，因为集合枚举树将组件的所有组合都枚举出来，所有的极小冲突集会在遍历完这棵枚举树之后全部产生，不会发生丢解.

其次，MCS-SFFO算法将故障输出相关元件放在待枚举的集合的前部，故障输出无关元件集放在后部，对故障输出无关元件间所有组合进行剪枝，因此与CSRDSE 2算法相比，调用SAT求解器次数将会大量减少，求解效率也将会明显提高.

算法3的复杂性分析：设系统元件总数为n，系统故障输出无关元件个数为k，则使用MCS-SFFO算法剪枝的故障输出无关元件集子集的节点个数为2k.因此当k越大时剪枝的节点数越多.下面对算法的最好情况和最坏情况进行分析：

1) 最坏情况.当k=0，即故障输出无关元件个数为0，此时故障输出无关元件集子集个数为0，因此与算法CSRDSE 2相比，使用算法MCS-SFFO剪枝的节点个数没有增多，算法MCS-SFFO退化为算法CSRDSE 2.

2) 最好情况.当k=n-1，即故障输出无关元件个数约等于元件总数时，此时故障输出无关元件集子集个数为2k.算法MCS-SFFO剪枝步骤可分为2个，首先直接剪枝2k个故障输出无关元件集的子集节点，此时剩余子树的节点数也为2k；然后使用算法CSRDSE继续对剩余子树进行剪枝.而算法CSRDSE仍需遍历节点数为2k+1的整棵集合枚举树，与算法MCS-SFFO相比，多遍历了集合枚举树的一半节点.

5 实验结果

本节实现了CSRDSE 2和MCS-SFFO算法，将这2种算法与刘伯文等人[12]提出的CSRDSE算法进行了比较并给出了实验结果.实验运行平台如下：Dell Dimension C521，Ubuntu 12.04 LTS，GCC编译器，AMD Athlon(tm) 64 X2 Dual Core Processor 3600+，1.90 GHz，3 GB RAM.算法调用的SAT求解器为Picosat.

为与CSRDSE算法对比，本文测试用例仍选用文献[12]中的电路，包括电路C17，Fulladder_1，Fulladder_2，Fulladder_3，Fulladder_4，Fulladder_5，Polybox_5，Polybox_9.在实验中，对每个电路给出大量观测，然后分别用CSRDSE，CSRDSE 2，MCS-SFFO算法进行求解.用算法MCS-SFFO求解冲突集时，首先根据系统描述和系统观测求出电路的故障输出相关元件集和故障输出无关元件集，并将其保存至相应文件内；然后将该文件作为MCS-SFFO算法的输入参数来求解极小冲突集.

表1是分别用CSRDSE和CSRDSE 2算法求解极小冲突集时平均访问节点的次数.其中，d表示算法CSRDSE与算法CSRDSE 2平均访问节点数之差，p表示算法CSRDSE与算法CSRDSE 2平均访问节点数之比.从表1可以看出，与CSRDSE算法相比，CSRDSE 2算法平均访问节点次数明显减少，并随着电路规模的扩大，CSRDSE 2算法效率提高越明显.CSRDSE 2算法减少了对某些节点的子叶节点查找非冲突集合簇的次数，同时避免了与非冲突集合簇进行子集检测的问题，但调用SAT求解器次数与算法CSRDSE相等.

Table 1 Average Number of Access Nodes表1 平均访问节点数

表2是分别用CSRDSE和MCS-SFFO算法求解极小冲突集时调用SAT求解器次数.其中，d表示算法CSRDSE与算法MCS-SFFO平均调用SAT求解器次数之差，p表示算法CSRDSE与算法MCS-SFFO平均调用SAT求解器次数之比.从表2中可以看出与CSRDSE算法相比，MCS-SFFO算法调用SAT求解器次数明显减少.对于不同电路，MCS-SFFO算法优化程度不同.Fulladder_1电路平均提高0.06倍，而Fulladder_3电路平均提高3.48倍.这些都源于Fulladder_1与Fulladder_3电路特征的差异.Fulladder_1电路的故障输出无关元件数占元件总数比例较小，因此使用MCS-SFFO算法剪枝的节点较少，效率提高不明显;而Fulladder_3电路的故障输出无关元件数占元件总数比例较大，使用MCS-SFFO算法剪枝的节点也相对较多，求解效率提高较大.

表3是MCS-SFFO，CSRDSE 2，CSRDSE算法求解极小冲突集的时间对比结果，其中最后一列表示CSRDSE与MCS-SFFO求解时间的加速比(其中因除数为0而无法运算加速比用空白表示).从表3中可以看出，CSRDSE 2算法与CSRDSE算法相比，求解时间减少，但效率提高并不明显；而MCS-SFFO算法与CSRDSE 2算法相比，大部分电路的求解时间明显减少.这源于MCS-SFFO与CSRDSE 2算法遍历节点数相对CSRDSE算法虽然都有减少，但CSRDSE 2算法并没有减少调用SAT求解器的次数，只减少了扫描非冲突集合簇的次数，而MCS-SFFO大量减少了调用SAT求解器的次数.而调用SAT求解器耗时较长，因此MCS-SFFO算法效率提高更加显著.

Table 2 Average Number of SAT Call表2 平均调用SAT求解器次数

Table 3 Running Time表3 求解时间

6 结束语

基于模型诊断一直是人工智能领域内重要的研究方向.随着SAT问题的求解算法不断优化，使用SAT求解器求解冲突集已得到众多学者的关注.本文在对CSRDSE算法研究的基础上，提出了结合故障输出结构特征的极小冲突求解算法MCS-SFFO.该算法首先对CSRDSE算法的剪枝规则做出改进，避免了对非冲突集的叶节点对应子叶节点的访问；其次给出求解故障输出无关元件集的算法GetCompS，根据系统描述和系统观测，利用SAT求解器计算出故障输出无关元件集；最后，提出非冲突集定理——系统故障输出无关元件集的子集不是冲突集，根据此定理可对SE-Tree中的故障输出无关元件集的子集节点进行剪枝，在生成SE-Tree时将故障输出无关元件置于待枚举集合末端，当遍历到的节点是故障输出无关元件集的子集时，停止遍历SE-Tree.实验结果表明，对CSRDSE算法的剪枝规则改进后，访问节点数大幅度减少，求解时间相对较短.MCS-SFFO算法相对于CSRDSE算法剪枝节点数更多，调用SAT求解器次数明显减少.并且，随着电路规模的扩大，故障输出无关元件数目也越多，因此，剪枝的节点个数也增多，MCS-SFFO算法效率提升更加显著.