歐陽丹彤 智華云 劉伯文 張立明 張永剛

(吉林大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 長(zhǎng)春 130012) (符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué)) 長(zhǎng)春 130012) (ouyangdantong@163.com)

基于模型診斷(model-based diagnosis， MBD)問題對(duì)人工智能領(lǐng)域的發(fā)展具有十分重要的推動(dòng)作用[1].其主要思想是根據(jù)設(shè)備的內(nèi)部結(jié)構(gòu)和行為來診斷該設(shè)備，從模型和觀測(cè)出發(fā)推理出設(shè)備的故障組件，解釋預(yù)期行為和觀測(cè)行為之間的差異.基于模型診斷過程主要分為3個(gè)步驟:1)診斷產(chǎn)生.已知一個(gè)差異，決定可能失靈的組件導(dǎo)致該差異.2)診斷測(cè)試.測(cè)試診斷過程中產(chǎn)生的所有診斷解，找出能夠解釋設(shè)備所有觀測(cè)的組件集合.3)診斷辨別.若有多個(gè)診斷通過測(cè)試，搜集額外信息以得到最后的診斷解.

著名MBD專家Reiter[2]提出了根據(jù)極小沖突集求解極小碰集(即系統(tǒng)的極小診斷解)的方法HS-Tree，但該方法要遍歷整棵枚舉樹，導(dǎo)致診斷空間很大且會(huì)因剪枝丟失診斷解.針對(duì)這些缺點(diǎn)，Greiner等人[3]提出了改進(jìn)方法HS-DAG，解決了HS-Tree的丟解問題.隨著對(duì)MBD問題深入的探索和研究，許多新的方法被提出.Stein等人[4]提出的診斷方法允許待診斷系統(tǒng)的組件及其行為有缺省信息，并用合理的假設(shè)表示系統(tǒng)的異常行為，有效地提升了該方法對(duì)特定問題的求解效率.趙相福等人[5]提出了CSISE-Tree方法，在對(duì)集合枚舉樹進(jìn)行剪枝優(yōu)化的基礎(chǔ)上求出診斷系統(tǒng)所有的診斷解.歐陽丹彤等人[6]提出了利用標(biāo)志傳播求解系統(tǒng)所有候選解的方法，通過傳播系統(tǒng)的輸出標(biāo)志來判斷組件集合是否是診斷解.Schmitz等人[7]利用部分診斷解優(yōu)化沖突集，并提出了根據(jù)極小沖突集求診斷解的時(shí)序診斷方法.

近年來，命題可滿足問題(propositional satis-fiability problem， SAT)受到國(guó)內(nèi)外學(xué)者的廣泛關(guān)注[8].Cook[9]于1971年首次證明SAT問題是NP完全問題，人工智能領(lǐng)域的很多NP問題都可以轉(zhuǎn)化成SAT問題求解[10]且研究表明，與直接求解NP問題相比，將其轉(zhuǎn)化成SAT問題后求解更加高效.一些優(yōu)秀的求解引擎已被廣泛應(yīng)用于布局布線、自動(dòng)測(cè)試矢量、電路等價(jià)性驗(yàn)證、智能規(guī)劃等[11]領(lǐng)域.隨著對(duì)MBD問題研究的深入，發(fā)現(xiàn)該問題也可以轉(zhuǎn)換成SAT問題求解且已取得顯著成果.

基于SAT求解器的發(fā)展，國(guó)內(nèi)外許多學(xué)者開始投入到結(jié)合SAT求解診斷的研究領(lǐng)域中.Feldman等人[12]提出利用帶權(quán)重的MaxSat求解MBD，該方法將子句分為hard子句和soft子句，并對(duì)子句賦予權(quán)重，最終要求滿足子句權(quán)重乘積之和最大，進(jìn)而得到所有診斷解.Metodi等人[13]提出了一種新的編碼方式，將MBD編碼成布爾可滿足問題來求解，并對(duì)診斷系統(tǒng)進(jìn)行了復(fù)雜的預(yù)處理.Marques-Silva等人[14]提出將MBD轉(zhuǎn)成MaxSat問題求解的方法，根據(jù)阻塞結(jié)點(diǎn)和邊、過濾結(jié)點(diǎn)和邊縮減診斷系統(tǒng)規(guī)模，減小診斷系統(tǒng)求解空間.國(guó)內(nèi)學(xué)者周建華等人[15]利用SAT求解器結(jié)合LLBRS-Tree算法求出診斷系統(tǒng)所有的極小診斷解，此方法是目前基于枚舉樹結(jié)構(gòu)利用SAT求解診斷效率較高的方法.

LLBRS-Tree方法從葉結(jié)點(diǎn)開始向上遍歷枚舉樹直到根結(jié)點(diǎn)為止，同時(shí)基于非診斷解的祖先結(jié)點(diǎn)一定不是診斷解進(jìn)行無解剪枝[15]以及診斷解的子孫結(jié)點(diǎn)一定不是極小診斷解進(jìn)行有解剪枝[15]，通過有解剪枝和無解剪枝剪掉大量結(jié)點(diǎn).本文在LLBRS-Tree方法的基礎(chǔ)上進(jìn)行了改進(jìn)，提出了根據(jù)組件的靜態(tài)偽故障度和動(dòng)態(tài)偽故障度生成枚舉樹，動(dòng)態(tài)更新枚舉樹遍歷順序進(jìn)行剪枝的方法DYN-Tree.該方法計(jì)算每個(gè)組件發(fā)生故障的概率(記為靜態(tài)偽故障度)，根據(jù)組件的靜態(tài)偽故障度生成枚舉樹，當(dāng)調(diào)用SAT求解器求得一個(gè)組件集合是極小診斷解時(shí)，更新該集合中組件的動(dòng)態(tài)偽故障度，重新動(dòng)態(tài)生成新的枚舉樹遍歷順序，對(duì)新生成的枚舉樹進(jìn)行有解剪枝和無解剪枝，直到求得診斷系統(tǒng)的所有極小診斷解為止.該方法能夠較早地發(fā)現(xiàn)極小診斷解，裁剪掉大量冗余的診斷解.

1 預(yù)備知識(shí)

本節(jié)首先介紹一些基于模型診斷的相關(guān)概念，然后介紹如何將基于模型診斷問題轉(zhuǎn)化成SAT問題求解.

1.1 基于模型診斷的相關(guān)概念

定義1. 診斷系統(tǒng)[1]. 一個(gè)系統(tǒng)定義為一個(gè)三元組(SD，COMPS，OBS)，其中：SD是系統(tǒng)描述，是謂詞公式的集合；COMPS是系統(tǒng)的組成部件集合，是一個(gè)有限常量集合；而OBS是觀測(cè)集合，是謂詞公式的有限集合.

AB意味著“abnormal”(反常)，當(dāng)部件c∈COMPS反常時(shí)，AB(c)為真，否則，AB(c)為真.

定義2. 基于一致性診斷[1]. 設(shè)組件集合Δ?COMPS，稱Δ為關(guān)于(SD，COMPS，OBS)的一個(gè)基于一致性診斷，若SD∪OBS∪{AB(c)|c∈COMPS-Δ}是可滿足的.

定義3. 極小診斷解[1]. 稱關(guān)于(SD，COMPS，OBS)的一個(gè)基于一致性診斷Δ是極小的診斷，當(dāng)且僅當(dāng)不存在Δ的任何真子集也是關(guān)于(SD，COMPS，OBS)的一個(gè)基于一致性診斷.

在弱故障模型診斷中，根據(jù)極小診斷解的定義可知：若集合A是(SD，COMPS，OBS)的一個(gè)極小診斷解，其中有B?COMPS，C?COMPS，則：

1) 若A?C，則C一定是該系統(tǒng)的一個(gè)基于一致性診斷，但C不是極小診斷解；

2) 若B不是診斷解且C?B，則C一定不是該系統(tǒng)的基于一致性診斷.

根據(jù)1)和2)可知，如果某組件集合不是基于一致性診斷，那它的真子集肯定不是基于一致性診斷；基于一致性診斷解的真超集依然是該系統(tǒng)的診斷解，但不是極小診斷解.本文利用上述性質(zhì)對(duì)集合枚舉樹進(jìn)行剪枝，提高診斷解求解效率.

1.2 將基于模型診斷轉(zhuǎn)化成命題可滿足問題

本節(jié)介紹SAT問題的基本定義，并介紹如何將基于模型診斷問題轉(zhuǎn)化為SAT問題求解的方法.

SAT問題是指對(duì)于給定的一個(gè)CNF合取范式Q=C1∧C2∧…∧Cn，X={x1,x2,…,xm}是該公式的變量集合，Ci(i=1,2,…,n)是變量x1,x2,…,xm或變量否定的析取式，如果變量x1,x2,…,xm找到一組賦值能夠使得公式Q最后取值為真，則稱Q是可滿足的，否則是不可滿足的.

SAT求解器的輸入是CNF形式的文件，故需要將電路系統(tǒng)的內(nèi)部結(jié)構(gòu)信息、觀測(cè)信息和組件信息3部分用CNF子句表示，并構(gòu)成一個(gè)CNF文件.SAT求解器處理該CNF文件，如果最后返回結(jié)果為真，那么該CNF文件是可滿足的，否則不是.

首先，我們先將診斷系統(tǒng)轉(zhuǎn)換成CNF描述形式，圖1是診斷系統(tǒng)中常用的組件.

Fig. 1 The components of system圖1 系統(tǒng)組件

在電路系統(tǒng)中，輸入有高電平、低電平之分，本文中，輸入為正數(shù)代表高電平，負(fù)數(shù)代表低電平.比如圖1(a)中或門，輸入端口“5”表示的是高電平，而不是電平值.假設(shè)圖1組件均正常，根據(jù)離散數(shù)學(xué)和數(shù)字邏輯知識(shí)，再結(jié)合這些組件的輸入，可以推出組件對(duì)應(yīng)的輸出，則圖1中各組件的CNF子句形式表示如下：

假設(shè)上述組件均正常，根據(jù)離散數(shù)學(xué)和數(shù)字邏輯知識(shí)，再結(jié)合這些組件的輸入，可以推出組件對(duì)應(yīng)的輸出，并以CNF子句的形式表示如下.

1) OR(或門)

(5∨6∨-13∨N1)∧(-5∨13∨N1)∧(-6∨13∨N1)；

2) AND(與門)

(-7∨-8∨14∨N2)∧(7∨-14∨N2)∧(8∨-14∨N2)；

3) XOR(異或門)

(9∨10∨-15∨N3)∧(-9∨-10∨-15∨N3)∧(-9∨10∨15∨N3)∧(9∨-10∨15∨N3);

4) NOR(或非門)

(11∨12∨16∨N4)∧(-11∨-16∨N4)∧(-12∨-16∨N4).

本節(jié)描述了怎樣將系統(tǒng)組件轉(zhuǎn)換成CNF表達(dá)式，下面將給出圖1(a)中或門的CNF子句在文件中的組織形式：

pcnf331-51310∕*p,cnf是文件語法,第1行第1個(gè)3表示變量個(gè)數(shù),第2個(gè)3表示子句個(gè)數(shù),1是組件個(gè)數(shù)*∕56-130∕*5,6代表文字,-13是變量的否定,每行都是一個(gè)子句,子句都以0結(jié)束*∕-61310∕*最后1個(gè)子句可表示為(-6∨13∨1)*∕

通過上面的轉(zhuǎn)換，可以將系統(tǒng)的內(nèi)部功能信息、系統(tǒng)觀測(cè)以及組件信息表示成CNF命題形式，然后調(diào)用SAT求解器處理，根據(jù)SAT求解器返回值求解該系統(tǒng)的基于一致性診斷解.第2節(jié)將介紹求解系統(tǒng)對(duì)應(yīng)的所有診斷解的具體算法.

2 SE-Tree及LLBRS-Tree診斷求解方法

第1節(jié)介紹了如何將基于模型診斷問題轉(zhuǎn)化成SAT問題求解，本節(jié)將要介紹求解診斷基于樹結(jié)構(gòu)的2種方法：基于集合枚舉樹(set-enumeration tree， SE-Tree)的遍歷方法和反向遍歷的LLBRS-Tree方法.

2.1 根據(jù)集合枚舉樹求解所有診斷

集合枚舉樹(SE-Tree)由國(guó)外學(xué)者Rymon[16]提出：它可以枚舉出一個(gè)集合所有的子集.集合SS有M個(gè)元素，SE-Tree可以按照某種順序枚舉出SS的2M個(gè)子集；設(shè)SS={N1，N2，N3，N4}，默認(rèn)枚舉樹從第0層開始，如果枚舉樹第1層從左到右組件出現(xiàn)的順序分別是{N4}，{N3}，{N2}，{N1}，則集合SS的完全枚舉樹如圖2所示：

Fig. 2 SE-Tree of the set {N1,N2,N3,N4}圖2 集合{N1,N2,N3,N4}的完全枚舉樹

SE-Tree在求系統(tǒng)的診斷解時(shí)是完備的算法，它遍歷集合枚舉樹中所有結(jié)點(diǎn)，每當(dāng)求解得到新的診斷解時(shí)，就會(huì)更新原來的診斷解，以保證最后剩余的都是極小診斷解.雖然SE-Tree是完備的，但沒有任何剪枝優(yōu)化策略，效率并不高.趙相福等學(xué)者在SE-Tree的基礎(chǔ)上提出了CSISE-Tree方法.該算法通過廣度優(yōu)先策略遍歷翻轉(zhuǎn)的集合枚舉樹，對(duì)非診斷解及其所有的真子集進(jìn)行剪枝.

2.2 LLBRS-Tree算法求診斷解

周建華等人[15]在CSISE-Tree的基礎(chǔ)上提出了改進(jìn)算法LLBRS-Tree，下面介紹該算法的相關(guān)定義及實(shí)現(xiàn).

定義4. 反向搜索[15].對(duì)于一個(gè)集合枚舉樹，稱從樹的葉結(jié)點(diǎn)向根結(jié)點(diǎn)遍歷的過程為反向搜索.

定義5. 有解剪枝[15].對(duì)于一個(gè)集合枚舉樹，如果在遍歷它時(shí)發(fā)現(xiàn)某個(gè)結(jié)點(diǎn)是診斷解，那么該結(jié)點(diǎn)的所有子孫結(jié)點(diǎn)一定不是極小診斷解，因此，可以直接跳過這些子孫結(jié)點(diǎn)，不再判斷.稱跳過該結(jié)點(diǎn)的子孫結(jié)點(diǎn)的過程為有解剪枝.

定義6. 無解剪枝[15].在遍歷一個(gè)枚舉樹時(shí)，發(fā)現(xiàn)某個(gè)結(jié)點(diǎn)不是系統(tǒng)的診斷解，那么該結(jié)點(diǎn)的父結(jié)點(diǎn)及其祖先結(jié)點(diǎn)也不是診斷解，因此，可以直接跳過這個(gè)結(jié)點(diǎn)的父結(jié)點(diǎn)和其祖先結(jié)點(diǎn)，不再判斷.稱跳過該結(jié)點(diǎn)的父結(jié)點(diǎn)及其祖先結(jié)點(diǎn)的過程為無解剪枝.

算法LLBRS-Tree對(duì)集合枚舉樹反向搜索，在從葉結(jié)點(diǎn)向根結(jié)點(diǎn)遍歷搜索過程中，同時(shí)進(jìn)行有解剪枝和無解剪枝，減掉枚舉樹中的部分結(jié)點(diǎn).LLBRS-Tree算法的偽代碼如下：

算法1. LLBRS-Tree算法.

輸入： 系統(tǒng)描述CNF的文件SysDis.CNF、系統(tǒng)觀測(cè)的CNF文件SysObs.CNF、極小診斷解的最大診斷長(zhǎng)度MinDigLen；

輸出： 極小診斷解的集合DigRes[].

局部變量： 待判斷的第1層某個(gè)結(jié)點(diǎn)及其子樹sub-tree.

① 初始化DigRes=?；

② 從SysDis.CNF文件中的第1行中讀取出診斷系統(tǒng)變量個(gè)數(shù)、CNF子句個(gè)數(shù)及組件個(gè)數(shù)；

③ 將集合枚舉樹的第1層最左邊的結(jié)點(diǎn)及其子樹賦值給sub-tree，子樹的高度是MinDigLen(默認(rèn)集合枚舉樹從第0層開始)；

④ while(集合枚舉樹中存在第1層結(jié)點(diǎn)及其子樹還沒判斷)

while(sub-tree判斷未完成)

先判斷sub-tree最后1層最左邊的結(jié)點(diǎn)是否是診斷解；

if (該結(jié)點(diǎn)是診斷解)

將結(jié)點(diǎn)加入到集合DigRes中，并且刪除在DigRes集合中該結(jié)點(diǎn)的所有真超集；

刪除枚舉樹中該結(jié)點(diǎn)的所有子孫結(jié)點(diǎn)；

對(duì)該結(jié)點(diǎn)的父結(jié)點(diǎn)進(jìn)行判斷；

else

刪除該結(jié)點(diǎn)的父結(jié)點(diǎn)及其祖先結(jié)點(diǎn)；

訪問下一個(gè)沒有被訪問及其刪除的葉結(jié)點(diǎn)；

endif

將第1層的下一個(gè)結(jié)點(diǎn)及其子樹賦值給sub-tree，接著對(duì)sub-tree進(jìn)行判斷；

endwhile

endwhile

⑤ 返回集合DigRes.

在弱故障模型診斷中，LLBRS-Tree的提出對(duì)于系統(tǒng)的極小診斷解的求解效率有了一定的提升，主要優(yōu)點(diǎn)有2項(xiàng)：

1) 根據(jù)診斷解的定義，非診斷解的所有真子集均不是診斷系統(tǒng)的診斷解.LLBRS-Tree利用該特征進(jìn)行剪枝，避免了一些非診斷解的判斷.

2) 根據(jù)極小診斷解的定義，極小診斷解的所有真超集均不是極小診斷解.因此，在遍歷枚舉樹時(shí)我們可以不去判斷極小診斷解的真超集.

與CSISE-Tree相比，LLBRS-Tree在求解極小診斷解的效率時(shí)有很大的提升，但是在求解過程中，該算法遍歷了大量極小診斷解的真超集，而這些真超集不是最終解，最后都會(huì)被刪除.針對(duì)這種情況對(duì)該算法進(jìn)行了改進(jìn)，能減少很多冗余解(極小診斷解的真超集)的產(chǎn)生，剪掉大量極小診斷解的真超集，提高問題求解效率.

3 基于偽故障度動(dòng)態(tài)生成枚舉樹的診斷方法

通過分析可知，在一個(gè)電路系統(tǒng)中，極小診斷解的數(shù)量并不多，剩下的大多數(shù)結(jié)點(diǎn)是非診斷解和冗余解.基于此，提出針對(duì)冗余解的剪枝策略.該算法是完備算法，不需要訪問枚舉樹中所有結(jié)點(diǎn)，只遍歷部分結(jié)點(diǎn)可以得到系統(tǒng)所有的極小診斷解.

定義7. 故障輸出.對(duì)于一個(gè)電路系統(tǒng)，如果該終端組件的實(shí)際輸出和觀測(cè)輸出不一樣，稱該終端組件的輸出為故障輸出.

通過分析電路內(nèi)部結(jié)構(gòu)關(guān)系、系統(tǒng)觀測(cè)行為和預(yù)期行為，得知每個(gè)組件出現(xiàn)故障的概率并不相同，與故障輸出相關(guān)的組件比一般的組件出現(xiàn)故障的概率要大.

定義8. 部分診斷解.設(shè)在診斷系統(tǒng)中與某組件comp輸入相連組件個(gè)數(shù)是N，如果其中M(1≤M≤N)個(gè)組件同時(shí)故障與組件comp故障時(shí)的故障輸出相同，即M個(gè)組件同時(shí)故障能解釋組件comp故障時(shí)的故障輸出，則此M個(gè)組件集合稱為部分診斷解.

定義9. 靜態(tài)偽故障度.稱系統(tǒng)中某組件comp發(fā)生故障的概率為該組件的靜態(tài)偽故障度(記為SD)，并且故障輸出對(duì)應(yīng)組件的SD=1，正常組件的SD=0；設(shè)組件comp的SD=Dc(Dc>0)，與組件comp對(duì)應(yīng)的部分診斷解中有M個(gè)組件，這M個(gè)組件的SD分別為DcM；若某組件的SD有多個(gè)取值Di(i=1,2,…,m)，則該組件的SD=max{Di|i=1,2,…,m}.

由定義9計(jì)算出每個(gè)組件的SD，再根據(jù)組件的SD大小對(duì)組件進(jìn)行排序.在生成枚舉樹時(shí)，SD值大的組件排在前面，遍歷時(shí)首先訪問這些組件組成的集合.比如在圖2中，我們認(rèn)為組件4的靜態(tài)偽故障度最大(組件i的偽故障度記為SDi)，組件1的靜態(tài)偽故障度最小，即SD4>SD3>SD2>SD1.并且集合枚舉樹隨著極小診斷解的產(chǎn)生而動(dòng)態(tài)改變.

定義10. 動(dòng)態(tài)偽故障度.診斷系統(tǒng)中，記某組件comp在枚舉樹第1層中位置是否變化的標(biāo)志為該組件的動(dòng)態(tài)偽故障度(簡(jiǎn)稱DD).若組件comp靜態(tài)偽故障度大于0，設(shè)該組件的動(dòng)態(tài)偽故障度等于1，其在枚舉樹第1層結(jié)點(diǎn)中的位置不再改變.對(duì)于靜態(tài)偽故障度等于0的組件，其DD初始化為0，并且根據(jù)以下2個(gè)規(guī)則更新這些組件的DD：

1) 枚舉樹第1層中某個(gè)集合K，以K為根結(jié)點(diǎn)的子樹中已經(jīng)有結(jié)點(diǎn)被訪問過，更新集合K中組件的DD=1；

2) 在遍歷枚舉樹時(shí)，搜索到一個(gè)結(jié)點(diǎn)為極小診斷解，且該結(jié)點(diǎn)中有組件的DD值為0，則這些組件的DD重新賦值為1.

在定義10中，以方式1)改變集合K中組件的DD后，K在枚舉樹第1層結(jié)點(diǎn)中的位置不再改變；而以方式2)改變某些組件的DD值后，還要改變這些組件在枚舉樹第1層結(jié)點(diǎn)中的順序.設(shè)枚舉樹第1層結(jié)點(diǎn)從左到右對(duì)應(yīng)的組件分別是：comp1,comp2,…,compj,compj+1,…,compk,compk+1,…,compn(j

定義11. 最左結(jié)點(diǎn)[17].以某結(jié)點(diǎn)為根結(jié)點(diǎn)形成的子樹中，我們稱最底層最左邊的結(jié)點(diǎn)為最左結(jié)點(diǎn).

如圖2中的{N4,N3,N2,N1}是最左結(jié)點(diǎn).

定義12. 兄弟結(jié)點(diǎn)[17].如果若干個(gè)結(jié)點(diǎn)有共同的父結(jié)點(diǎn)，則稱這些結(jié)點(diǎn)是兄弟結(jié)點(diǎn).

如圖2中的{N4,N3}，{N4,N2}，{N4,N1}是兄弟結(jié)點(diǎn).

下面我們給出該算法的偽代碼.

算法2. DYN-Tree算法.

輸入: 系統(tǒng)描述的CNF文件SysDis.CNF、系統(tǒng)觀測(cè)的CNF文件SysObs.CNF；

輸出： 診斷系統(tǒng)的極小診斷解集合Res.

①initialize()；

②calweight(SysDis.CNF,SysObs.CNF)；

③ while(S≠?)

④flag=issolve(S);

⑤ if (flag==1)

⑥addsol(S,Res)；

⑦updatetree(true,S)；

⑧ if (S是以S的父結(jié)點(diǎn)為根結(jié)點(diǎn)的子樹中最左邊分支上的結(jié)點(diǎn))

⑨S←S的父結(jié)點(diǎn)；

⑩ else if (S是從最底層向上回溯后的結(jié)點(diǎn))

S←下一個(gè)葉結(jié)點(diǎn)；

在算法2中，步驟②calweight算法計(jì)算系統(tǒng)的故障輸出，找到能夠解釋故障輸出的組件集合，進(jìn)而計(jì)算出每個(gè)組件的SD，生成新的集合枚舉樹，下面就是遍歷集合枚舉樹的步驟.步驟③～，當(dāng)枚舉樹沒有被遍歷完時(shí)進(jìn)入循環(huán)體，繼續(xù)尋找可能的診斷解.步驟④，issolve(S)判斷集合S是否是診斷解.步驟⑤⑥，當(dāng)S是診斷解時(shí)，addsol(S,Res)更新診斷解的集合Res，如果Res中有S的真超集，那么用S替換S的真超集；步驟⑦，若S是極小診斷解，算法updatetree更新S中動(dòng)態(tài)偽故障度等于0的組件，隨后對(duì)組件重新排序，動(dòng)態(tài)生成新的枚舉樹；步驟⑧～表示S是診斷解時(shí)，確定下一個(gè)要遍歷的結(jié)點(diǎn)；步驟，以枚舉樹第1層的結(jié)點(diǎn)為根結(jié)點(diǎn)的子樹中有結(jié)點(diǎn)被遍歷過，算法updatetree更新該根結(jié)點(diǎn)組件的動(dòng)態(tài)偽故障度；步驟，結(jié)點(diǎn)S不是診斷解時(shí)確定下一個(gè)要訪問的結(jié)點(diǎn)；最后返回極小診斷解的集合.

計(jì)算系統(tǒng)組件靜態(tài)偽故障度的算法calweight如下.

算法3.calweight()算法.

輸入：系統(tǒng)描述的CNF文件 SysDis.CNF、系統(tǒng)觀測(cè)的CNF文件SysObs.CNF；

輸出： 系統(tǒng)的部分診斷解PartSol.

局部變量： 故障輸出的組件和可能故障的組件ErrorOut，可能故障組件的輸入In_Out，與故障輸出組件和可能故障的組件相關(guān)的組件CComp.

①ErrorOut←由SysDis.CNF和SysObs.CNF找到系統(tǒng)故障輸出組件；

② for(i=0；i

③In_Out←ErrorOut[i]的輸入；

④ for(j=0；j

⑤CComp←找到以In_Out[j]作為輸出的組件；

⑥ if(對(duì)CComp中某些組件的輸出取反后能解釋故障輸出)

⑦PartSol←輸出值被取反的組件組成的集合；

⑧ErrorOut←輸出值被取反的組件；

⑨ endif

⑩ endfor

算法3的步驟①找到系統(tǒng)故障輸出的組件；步驟②～⑤求解哪些組件的輸出是故障輸出組件及可能故障組件的輸入；步驟⑥～⑧，CComp中的若干個(gè)組件均故障能夠解釋故障輸出，那么這些組件組成的集合是部分診斷解，并且該部分診斷解中組件故障的概率較大.最后返回部分診斷解的集合.

計(jì)算組件動(dòng)態(tài)偽故障度的算法updatetree如下.

算法4.updatetree()算法.

輸入：判斷結(jié)點(diǎn)S是否極小診斷解的boolean變量，枚舉樹中一個(gè)結(jié)點(diǎn)S.

① if(boolean==true)

② for(i=0；i

③S[i].DD=1；

endfor

④ else

⑤S[0].DD=1；

⑥ endif

算法4的步驟②③，boolean=true時(shí)，說明結(jié)點(diǎn)S是極小診斷解，S中組件故障的概率比較大，故S中如果有組件DD=0，更新這些組件的DD=1；步驟⑤，以枚舉樹第1層結(jié)點(diǎn)K為根結(jié)點(diǎn)的子樹中有結(jié)點(diǎn)被遍歷過，那么結(jié)點(diǎn)K在枚舉樹中的位置不再改變，賦值結(jié)點(diǎn)K中組件的DD=1.

Fig. 3 The circuit diagram of component set {N1,N2,N3,N4,N5,N6,N7}圖3 組件{N1,N2,N3,N4,N5,N6,N7}的電路圖

4 實(shí)驗(yàn)結(jié)果分析

實(shí)現(xiàn)了周建華等人[15]提出的LLBRS-Tree方法和本文提出的DYN-Tree方法，并對(duì)2個(gè)方法的效率進(jìn)行了對(duì)比.實(shí)驗(yàn)平臺(tái)如下：Dell GX620，Ubuntu 12.04，GCC編譯器，CPU AMD AthlonTM64 X2 Dual Core Processor 3600+1.9 GHz，3.00 GB RAM.LLBRS-Tree方法和DYN-Tree方法調(diào)用的SAT求解器均是Picosat[18].

本次使用的測(cè)試?yán)又饕獊碜訧SCAS-85的基準(zhǔn)電路，包括c17，c432，c499，c880，c1355，c1908，c2670.對(duì)于一個(gè)故障電路，系統(tǒng)觀測(cè)不同，最后的極小診斷解一般不同，我們改變某些電路的系統(tǒng)觀測(cè)以得到更多的測(cè)試?yán)?，使得DYN-Tree算法更具有說服力.如果一個(gè)電路有多個(gè)不同觀測(cè)，我們分別命名為：電路名-o1，電路名-o2，…，電路名-on，比如，c432有2個(gè)不同的觀測(cè)，我們可以分別命名成c432-o1，c432-o2.

本文分別對(duì)LLBRS-Tree方法和DYN-Tree方法在上述電路測(cè)試用例上進(jìn)行測(cè)試，極小診斷長(zhǎng)度是1時(shí)，所有組件都需要判斷，理論上2個(gè)算法效率一樣.因此，表1只需列出極小診斷長(zhǎng)度為2，3時(shí)2個(gè)算法的時(shí)間.理論上，極小診斷解長(zhǎng)度越長(zhǎng)，DYN-Tree算法剪掉的結(jié)點(diǎn)越多，效率提高的越多，這是由于在LLBRS-Tree算法的枚舉樹中，遍歷位置靠后的大量冗余解在DYN-Tree算法生成的動(dòng)態(tài)枚舉樹中都被優(yōu)先提前生成，且不需要被遍歷就可以剪掉.實(shí)驗(yàn)結(jié)果也表明極小診斷解長(zhǎng)度是2時(shí)，DYN-Tree算法效率平均提高了8%，極小診斷是3時(shí)，DYN-Tree算法效率平均提高了15%.在表1和表2中，空白表示在10 000 s內(nèi)算法求不出診斷解，極小診斷長(zhǎng)度是3時(shí)，對(duì)于電路c1908和c2670，LLBRS-Tree均求不出診斷解，DYN-Tree可以成功地求出診斷解.

單診斷所有結(jié)點(diǎn)都需要判斷，不存在剪枝情況.因此，表2中只列出了極小診斷長(zhǎng)度為2，3的情況，2個(gè)算法剪掉的結(jié)點(diǎn)數(shù)的差值是Δ為DYN-Tree算法剪掉的結(jié)點(diǎn)數(shù)目減去LLBRS-Tree算法剪掉的結(jié)點(diǎn)數(shù)目.Picosat求解器在判斷結(jié)點(diǎn)是否是診斷解時(shí)用了規(guī)則單元傳播和分裂規(guī)則，在求解時(shí)只要有一個(gè)終端組件的實(shí)際輸出和觀測(cè)輸出不一樣就可以斷定該結(jié)點(diǎn)是非診斷解，而確定一個(gè)結(jié)點(diǎn)是診斷解需要計(jì)算出所有終端組件的實(shí)際輸出和觀測(cè)輸出都一樣才行.因此，判斷一個(gè)結(jié)點(diǎn)是診斷解比判斷一個(gè)結(jié)點(diǎn)是非診斷解花費(fèi)時(shí)間更長(zhǎng)，而本文提出的改進(jìn)算法DYN-Tree剪掉了大量的冗余解，對(duì)問題求解效率提升明顯.

Table 1 Solution Time表1 求解時(shí)間 s

Table 2 Number of Cut Nodes表2 剪掉結(jié)點(diǎn)的個(gè)數(shù)

5 結(jié)束語

一直以來，基于模型診斷問題都是人工智能領(lǐng)域最重要的問題之一，本文將基于模型診斷問題轉(zhuǎn)換成SAT問題并利用SAT求解器求解，簡(jiǎn)化了問題求解難度.LLBRS-Tree是目前利用SAT求解診斷效率較高的方法，此方法雖然使用了有解剪枝和無解剪枝，但是仍然有許多冗余解存在，并且通過分析得知Picosat求解器求解冗余解時(shí)耗時(shí)更長(zhǎng).本文提出的DYN-Tree方法根據(jù)組件的靜態(tài)偽故障度生成枚舉樹，每當(dāng)遍歷到新的極小診斷解時(shí)，更新該診斷解中組件的動(dòng)態(tài)偽故障度，并根據(jù)組件的動(dòng)態(tài)偽故障度生成新的枚舉樹.該算法能夠及早地發(fā)現(xiàn)系統(tǒng)的極小診斷解，剪掉大量冗余解，減少SAT求解器調(diào)用次數(shù).實(shí)驗(yàn)結(jié)果表明DYN-Tree方法對(duì)于求解極小診斷解效率較LLBRS-Tree方法而言有較大提高.

[1]Console L, Dressler O. Model-based diagnosis in the real world: Learned and challenges remaining[C]Proc of the 16th Int Joint Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 1999: 1393-1400

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

[3]Greiner R, Smith B A, Wilkerson R W. A correction to the algorithm in Reiter’s theory of diagnosis[J]. Artificial Intelligence, 1989, 41(1): 79-88

[4]Stein B, Niggemann O, Lettmann T. Speeding up model-based diagnosis by a heuristic approach to solving SAT[C]Proc of the 24th Int Association of Science and Technology for Development on Artificial Intelligence and Applications. Anaheim, CA: ACTA, 2006: 273-278

[5]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal conflict sets using satisfiability algorithms[J]. Acta Electronica Sinica, 2009, 37(4): 804-810 (in Chinese)(趙相福, 歐陽丹彤. 使用SAT求解器產(chǎn)生所有極小沖突部件集[J]. 電子學(xué)報(bào), 2009, 37(4): 804-810)

[6]Ouyang Dantong, Zhang Liming, Zhao Jian, et al. Solving model-based fault diagnosis with flag propagation[J]. Chinese Journal of Scientific Instrument, 2011, 32(12): 2857-2862 (in Chinese)(歐陽丹彤, 張立明, 趙劍, 等. 利用標(biāo)志傳播求解基于模型的故障診斷[J]. 儀器儀表學(xué)報(bào), 2011, 32(12): 2857-2862)

[7]Shchekotykhin K, Schmitz T, Jannach D. Efficient sequential model-based fault-localization with partial diagnoses[C]Proc of the 25th Int Joint Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2016: 1164-1170

[8]Luo Chuan, Cai Shaowei, Wu Wei, et al. Double configuration checking in stochastic local search for satisfiability[C]Proc of the 28th AAAI Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2014: 2703-2709

[9]Cook S A. The complexity of theorem-proving procedures[C]Proc of the 3rd Annual ACM Symp on Theory of Computing. New York: ACM, 1971: 151-158

[10]Cai Shaowei, Su Kaile. Comprehensive score: Towards efficient local search for SAT with long clauses[C]Proc of the 23rd Int Joint Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2013: 489-495

[11]Cai Dunbo, Yin Minghao. On the utility of landmarks in SAT based planning[J]. Knowledge-Based Systems, 2012, 36(6): 146-154

[12]Feldman A, Provan G, de Kleer J, et al. Solving model-based diagnosis problems with Max-Sat Solvers and vice versa[C]Proc of the 21st Int Workshop on Principles of Diagnosis. New York: IJPHM, 2010: 185-192

[13]Metodi A, Stern R, Kalech M, et al. Compiling model-based diagnosis to Boolean satisfaction[C]Proc of the 26th AAAI Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2012: 793-799

[14]Marques-Silva J, Janota M, Ignatiev A, et al. Efficient model based diagnosis with maximum satisfiability[C]Proc of the 24th Int Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2015: 1966-1972

[15]Zhou Jianhua, Ouyang Dantong, Liu Bowen, et al. A new algorithm combining with the characteristic of the problem for model-based diagnosis[J]. Journal of Computer Rearch and Development, 2017, 54(3): 502-513 (in Chinese)(周建華, 歐陽丹彤, 劉伯文, 等. 基于模型診斷中結(jié)合問題特征的新方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2017, 54(3): 502-513)

[16]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

[17]Ouyang Dantong, Liu Bowen, Zhou Jianhua, et al. A method of computing minimal conflict sets combining the structure property with the anti-depth SE-TREE[J]. Acta Electronica Sinica, 2016, 45(5): 1175-1181 (in Chinese)

(歐陽丹彤, 劉伯文, 周建華, 等. 結(jié)合問題特征利用 SE-Tree 反向深度求解沖突集方法[J]. 電子學(xué)報(bào), 2016, 45(5): 1175-1181)

[18]Le Berre D, Parrain A. The SAT4j library, release 2.2[J]. Journal on Satisfiability Boolean Modeling and Computation, 2010, 7(11): 59-64

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.

ZhiHuayun, born in 1992. Master candidate at Jilin University. Her main research interests include model-based diagnosis, SAT problem and automated reasoning (13756941032@163.com).

LiuBowen, born in 1993. Master candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning (1591365445@qq.com).

ZhangLiming, born in 1980. PhD, post-doctor in Jilin University. His main research interests include model-based diagnosis, model checking and Boolean satisfiability.

ZhangYonggang, born in 1975. PhD. Associate professor in Jilin University. His main research interests include constraint satisfaction problem and automated reasoning.