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

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

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

基于模型诊断(model-based diagnosis)是人工智能领域中的重要研究方向,而基于极小冲突求诊断是求解诊断问题的经典方法,因此求解极小冲突是诊断中的一个重要步骤.通过对电路模型特征的研究,结合CSRDSE极小冲突集求解算法,提出结合故障输出结构特征的极小冲突求解算法MCS-SFFO:首先对CSRDSE算法的剪枝规则进行了改进,避免对集合枚举树SE-Tree中非冲突集叶节点对应子叶节点的访问;其次,提出故障输出无关元件集与故障输出相关元件集等相关概念,并根据系统描述和观测给出求解故障输出无关元件集的方法;最后,提出非冲突集定理,即故障输出无关元件集的子集不是冲突集,并根据非冲突集定理,给出极小冲突集求解算法MCS-SFFO.MCS-SFFO算法在基于CSRDSE算法求冲突集方法的基础上对无解空间进一步剪枝,减少了调用SAT求解器的次数.实验结果表明:与CSRDSE算法相比,MCS-SFFO算法求解效率明显提升.

关键词基于模型诊断;极小冲突集;集合枚举树;SAT求解器;故障输出无关元件

基于模型诊断(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].诊断系统是可用三元组(SDCOMPSOBS)表示,分别是系统描述、元件集、观测集.

定义2. 基于一致性诊断[3].设ΔCOMPS,称Δ为关于(SDCOMPSOBS)的基于一致性诊断,如果SDOBS∪{AB(c)|cΔ}∪{AB(c)|cCOMPS\Δ}是一致的.

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

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

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

1.2SAT问题

我们用xi(i=1,2,…,n)表示布尔变量.xixi称作文字,其中,xi称作变量xi的正文字,xi称作变量xi的负文字.X={x1,x2,…,xn}表示变量的集合.Qi(i=1,2,…,m)表示子句,每一个子句是一组文字的析取式.符号Φ代表CNF公式,CNF公式是由子句的合取构成,即合取范式CNF:Φ=Q1Q2∧…∧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.2CSRDSE算法

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

算法1. CSRDSE.

Node=SE-Tree的最左节点;

② While (Node≠∅)

notCS=isunsolve(Node);

④ If (notCS=0)

judgeISCS();

⑥ If (judge=0)

addtosolve(Node);

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

⑨ Else

addtosolve(Node);

按照剪枝规则1给Node赋值;

EndIf

Else

按剪枝规则2给Node赋值;

EndIf

EndWhile

3CSRDSE剪枝规则的改进

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

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

如图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的同层兄弟节点,若LeafF之间存在叶节点,称这些叶节点是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},若存在元件cCOMPSc的输出是诊断系统的输出,且该输出是系统的故障输出,即该输出的观测值与预期不符,则称元件c是该系统的故障输出元件.

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

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

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

Fig. 2 C17 circuit
图2 C17电路

在C17电路中,假设输出端12输出异常、输出端13输出正常,则c4是故障输出元件.故障输出相关元件集为{c1c2c3c4},故障输出无关元件集是{c5c6}.

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

算法2.GetCompS(SD.cnfOBS.cnf).

① 初始化:outABCompS=∅;

EXP_OUT=∅;

onABCompS=∅;

unOnABCompS=∅;

COMPS,从SD.cnf的第1行中获取;

OBS_IN,从OBS.cnf中获取;

OBS_OUT,从OBS.cnf中获取;

EXP_OUTgetExp(SD.cnfOBS_INCOMPS);

③ 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

While (COMPS中有未判断的元素oneComp)

If (oneComponABCompS)

unOnABCompS.add(oneComp);

EndIf

EndWhile

ReturnunOnABCompS.

在算法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 (NodeunOnABCompS)

⑥ Break;

⑦ Else

⑧ If (NodeunCSRes元素的子集)

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

⑩ Else

If (Node是冲突集)

Node加入到CSRes中,并按照标示规则将其超集标示为“1”;

按照剪枝规则1给Node赋值;

Else

Node加入到unCSRes中;

按照剪枝规则2给Node赋值;

EndIf

EndIf

EndIf

EndWhile

While (CSRes中还有标示为“0”的节点MCS_Node未加入到MCSRes中)

MCSRes.add(MCS_Node);

EndWhile

ReturnMCSRes.

算法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相等.

Table1AverageNumberofAccessNodes
表1平均访问节点数

InstanceAverage Number of Access NodesCSRDSE2CSRDSEdpC1723.8638.3814.521.61Fulladder_114.0619.945.881.42Fulladder_2113.34480.75367.414.24Polybox_518.5621.933.371.18Polybox_9232.09329.0596.961.42Fulladder_3361.061915.531554.475.30Fulladder_410850.7433348.4222497.683.07Fulladder_593339.89995783.44902443.5510.67

表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算法效率提高更加显著.

Table2AverageNumberofSATCall
表2平均调用SAT求解器次数

InstanceAverage Number of SAT CallMCS-SFFOCSRDSEdpC1713.1114.661.551.12Fulladder_18.819.310.501.06Fulladder_259.1775.8116.641.28Polybox_59.5312.502.971.31Polybox_940.48126.5786.093.13Fulladder_369.34310.66241.324.48Fulladder_41151.014421.013270.003.84Fulladder_57160.8010018.002857.201.40

Table3RunningTime
表3求解时间

InstanceNumber of TestsRunning Time∕sMCS-SFFOCSRDSE2CSRDSESpeedup RatioC1732000.005Fulladder_18000Fulladder_2320.00670.00330.02002.9851Polybox_564000.0050Polybox_92560.02000.04500.07503.7500Fulladder_3640.01670.11000.13678.1856Fulladder_45125.922532.375034.01005.7425Fulladder_55036.3375107.1775112.77753.1036

6结束语

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

参考文献

[1] Console L, Dressler O. Model-based diagnosis in the real world: Lessons learned and challenges remaining [C] //Proc of the 16th Int Joint Conf on Artificial Intelligence. San Francisco: Morgan Kaufmann, 1999: 1393-1400

[2]Liu Meng, Ouyang Dantong, Liu Bowen, et al. Grouped diagnosis approach using the feature of problem [J]. Acta Electronica Sinica, 2016, 46(3): 589-594 (in Chinese)

(刘梦, 欧阳丹彤, 刘伯文, 等. 结合问题特征的分组式诊断方法 [J]. 电子学报, 2016, 46(3): 589-594)

[3]Reiter R. A theory of diagnosis from first principles [J]. Artificial Intelligence, 1987, 32(1): 57-96

[4]Genesereth M R. The use of design descriptions in automated diagnosis [J]. Artificial Intelligence, 1984, 24(1): 411-436

[5]Haenni R. A query-driven anytime algorithm for argumentative and abductive reasoning[C] //Proc of the 1st Int Conf on Computing in an Imperfect World. Berlin: Springer, 2002: 114-127

[6]Luan Shangmin, Dai Guozhong. An approach to diagnosing a system with structure information [J]. Chinese Journal of Computers, 2005, 28(5): 801-808 (in Chinese)

(栾尚敏, 戴国忠. 利用结构信息的故障诊断方法 [J]. 计算机学报, 2005, 28(5): 801-808)

[7]Fang Min. A practical method to identify the minimal conflict [J]. Journal of Hefei University of Technology: Natural Science, 1999, 22(1): 39-43 (in Chinese)

(方敏. 一种识别最小冲突集的实用方法[J]. 合肥工业大学学报:自然科学版, 1999, 22(1): 39-43)

[8]Hou A. A theory of measurement in diagnosis from 1st principles [J]. Artificial Intelligence, 1994, 65(2): 281-328

[9]Han B, Lee S J. Deriving minimal conflict sets by CS-Trees with mark set in diagnosis from first principles [J]. IEEE Transactions on Systems, Man and Cybernetics, Part B(Cybernetic), 1999, 29(2): 281-286

[10]Zhao Xiangfu, Ouyang Dantong. A method of combining SE-Tree to compute all minimal hitting sets [J]. Progress in Natural Science, 2006, 16(2): 169-174

[11]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal conflict sets using satisfiability algorithms [J]. Acta Electronica Sinica, 2009, 37(4): 804-810 (in Chinese)

(赵相福, 欧阳丹彤. 使用SAT求解器产生所有极小冲突部件集[J]. 电子学报, 2009, 37(4): 804-810)

[12]Ouyang Dantong, Liu Bowen, Zhou Jianhua, et al. Using the method of SE-Tree depth of reverse search conflict sets combined with the feature of the problem [J]. Acta Electronica Sinica, 2017, 45(5): 1175-1181 (in Chinese)

(欧阳丹彤, 刘伯文, 周建华, 等. 结合问题特征利用SE-Tree反向深度求解冲突集方法 [J]. 电子学报, 2017, 45(5): 1175-1181)

[13]Zhou Junping, Yin Minghao, Zhou Chunguang. New worst-case upper bound for #2-SAT and #3-SAT with the number of clauses as the parameter [C] //Proc of the 24th AAAI Conf on Artificial Intelligence. Menlo Park: AAAI, 2010: 217-222

[14]Rymon R. Search through systematic set enumeration [C] //Proc of the 3rd Int Conf on Principles of Knowledge Representation and Reasoning. San Franasco, CA: Morgan Kaufmann, 1992: 539-550

AlgorithmofComputingMinimalConflictSetsBasedontheStructuralFeatureofFaultOutput

Xu Yini, Ouyang Dantong, Liu Meng, Zhang Liming, and Zhang Yonggang

(CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012) (KeyLaboratoryofSymbolicComputationandKnowledgeEngineering(JilinUniversity),MinistryofEducation,Changchun130012)

AbstractModel-based diagnosis is an important research in the field of artificial intelligence, and the diagnosis based on minimal conflict is a classical method to solve the problem of diagnosis. Therefore computing minimal conflict is an important step in model-based diagnosis. After studying the characteristics of the circuit model, this paper proposes an algorithm of computing minimal conflict sets based on the structural feature of fault output (MCS-SFFO) based on the CSRDSE algorithm. Firstly, the pruning rule of CSRDSE algorithm is improved, and it avoids the access to child leaf nodes of leaf nodes which are not conflict sets. Secondly, the concepts of component set independent of fault output and related to fault output are presented, and the method of computing component set independent of fault output is provided according to the system description and observation. Finally, a theorem about non-conflict set is proposed, that is, the component set independent of fault output and its subset are not conflict sets. MCS-SFFO algorithm that computes minimal conflict set is presented according to the non-conflict set theorem. Compared with CSRDSE algorithm, MCS-SFFO algorithm further prunes the non-solution space and reduces the number of calls to the SAT solver. Experimental evidence indicates that MCS-SFFO algorithm has better computational efficiency than CSRDSE algorithm.

Keywordsmodel-based diagnosis; minimal conflict set; SE-Tree; SAT solver; component independent of fault output

中图法分类号TP18

通信作者张永刚(zhangyg@jlu.edu.cn)

基金项目国家自然科学基金项目(61672261,61502199,61402196,61373052,61872159)This work was supported by the National Natural Science Foundation of China (61672261, 61502199, 61402196, 61373052, 61872159).

修回日期:2017-12-29

收稿日期2017-06-02;

XuYini, born in 1994. Master candidate at Jilin University. Her main research interests include model-based diagnosis, SAT problem.

OuyangDantong, born in 1968. Professor and PhD supervisor of Jilin University. Senior member of CCF. Her main research interests include model-based diagnosis, model checking and automated reasoning (ouyangdantong@163.com).

LiuMeng, born in 1993. PhD at Jilin University. Her main research interests include model-based diagnosis, SAT problem and automated reasoning (2238356051@qq.com).

ZhangLiming, born in 1980. PhD. Senior engineer of Jilin University. His main research interests include model-based diagnosis, model checking and Boolean satisfiability (limingzhang@jlu.edu.cn).

ZhangYonggang, born in 1975. Associate professor and PhD supervisor of Jilin University. His main research interests include model-based diagnosis and constraint satisfaction problem.