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

(吉林大學計算機科學與技術學院 長春 130012) (符號計算與知識工程教育部重點實驗室(吉林大學) 長春 130012) (ouyangdantong@163.com)

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

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

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

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

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

1 預備知識

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

1.1 基于模型診斷的相關概念

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

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

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

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

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

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

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

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

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

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

SAT問題是指對于給定的一個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é)構信息、觀測信息和組件信息3部分用CNF子句表示，并構成一個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ù)代表高電平，負數(shù)代表低電平.比如圖1(a)中或門，輸入端口“5”表示的是高電平，而不是電平值.假設圖1組件均正常，根據(jù)離散數(shù)學和數(shù)字邏輯知識，再結(jié)合這些組件的輸入，可以推出組件對應的輸出，則圖1中各組件的CNF子句形式表示如下：

假設上述組件均正常，根據(jù)離散數(shù)學和數(shù)字邏輯知識，再結(jié)合這些組件的輸入，可以推出組件對應的輸出，并以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表達式，下面將給出圖1(a)中或門的CNF子句在文件中的組織形式：

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

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

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

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

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

集合枚舉樹(SE-Tree)由國外學者Rymon[16]提出：它可以枚舉出一個集合所有的子集.集合SS有M個元素，SE-Tree可以按照某種順序枚舉出SS的2M個子集；設SS={N1，N2，N3，N4}，默認枚舉樹從第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)的診斷解時是完備的算法，它遍歷集合枚舉樹中所有結(jié)點，每當求解得到新的診斷解時，就會更新原來的診斷解，以保證最后剩余的都是極小診斷解.雖然SE-Tree是完備的，但沒有任何剪枝優(yōu)化策略，效率并不高.趙相福等學者在SE-Tree的基礎上提出了CSISE-Tree方法.該算法通過廣度優(yōu)先策略遍歷翻轉(zhuǎn)的集合枚舉樹，對非診斷解及其所有的真子集進行剪枝.

2.2 LLBRS-Tree算法求診斷解

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

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

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

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

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

算法1. LLBRS-Tree算法.

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

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

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

① 初始化DigRes=?；

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

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

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

while(sub-tree判斷未完成)

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

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

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

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

對該結(jié)點的父結(jié)點進行判斷；

else

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

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

endif

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

endwhile

endwhile

⑤ 返回集合DigRes.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

算法2. DYN-Tree算法.

輸入: 系統(tǒng)描述的CNF文件SysDis.CNF、系統(tǒng)觀測的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é)點為根結(jié)點的子樹中最左邊分支上的結(jié)點)

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

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

S←下一個葉結(jié)點；

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

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

算法3.calweight()算法.

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

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

局部變量： 故障輸出的組件和可能故障的組件ErrorOut，可能故障組件的輸入In_Out，與故障輸出組件和可能故障的組件相關的組件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(對CComp中某些組件的輸出取反后能解釋故障輸出)

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

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

⑨ endif

⑩ endfor

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

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

算法4.updatetree()算法.

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

① if(boolean==true)

② for(i=0；i

③S[i].DD=1；

endfor

④ else

⑤S[0].DD=1；

⑥ endif

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

實現(xiàn)了周建華等人[15]提出的LLBRS-Tree方法和本文提出的DYN-Tree方法，并對2個方法的效率進行了對比.實驗平臺如下：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].

本次使用的測試例子主要來自ISCAS-85的基準電路，包括c17，c432，c499，c880，c1355，c1908，c2670.對于一個故障電路，系統(tǒng)觀測不同，最后的極小診斷解一般不同，我們改變某些電路的系統(tǒng)觀測以得到更多的測試例子，使得DYN-Tree算法更具有說服力.如果一個電路有多個不同觀測，我們分別命名為：電路名-o1，電路名-o2，…，電路名-on，比如，c432有2個不同的觀測，我們可以分別命名成c432-o1，c432-o2.

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

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

Table 1 Solution Time表1 求解時間 s

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

5 結(jié)束語

一直以來，基于模型診斷問題都是人工智能領域最重要的問題之一，本文將基于模型診斷問題轉(zhuǎn)換成SAT問題并利用SAT求解器求解，簡化了問題求解難度.LLBRS-Tree是目前利用SAT求解診斷效率較高的方法，此方法雖然使用了有解剪枝和無解剪枝，但是仍然有許多冗余解存在，并且通過分析得知Picosat求解器求解冗余解時耗時更長.本文提出的DYN-Tree方法根據(jù)組件的靜態(tài)偽故障度生成枚舉樹，每當遍歷到新的極小診斷解時，更新該診斷解中組件的動態(tài)偽故障度，并根據(jù)組件的動態(tài)偽故障度生成新的枚舉樹.該算法能夠及早地發(fā)現(xiàn)系統(tǒng)的極小診斷解，剪掉大量冗余解，減少SAT求解器調(diào)用次數(shù).實驗結(jié)果表明DYN-Tree方法對于求解極小診斷解效率較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]. 電子學報, 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)(歐陽丹彤, 張立明, 趙劍, 等. 利用標志傳播求解基于模型的故障診斷[J]. 儀器儀表學報, 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]. 計算機研究與發(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]. 電子學報, 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.