結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法

徐旖旎 歐陽丹彤 劉 夢 張立明 張永剛

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

基于模型診斷(model-based diagnosis)一直是人工智能領(lǐng)域中的重要研究方向，對(duì)人工智能領(lǐng)域的發(fā)展起到了至關(guān)重要的作用[1].模型診斷方法包括基于沖突的求診斷方法和直接求診斷方法.基于沖突的求診斷方法主要分為2個(gè)步驟:1)求出極小沖突集;2)求解極小沖突集的極小碰集，即為診斷解.直接求診斷方法就是利用SAT(satisfiability)求解器直接求出診斷解，而不需要產(chǎn)生極小沖突集[2].

在基于模型診斷問題中，求解極小沖突集是求診斷解的重要步驟之一.Reiter[3]最早采用沖突部件集的概念來計(jì)算極小診斷.早期許多專家使用定理證明器的方法求解極小沖突.Genesereth[4]提出用DART(device-independent diagnostic program)方法進(jìn)行沖突識(shí)別.Haenni[5]在計(jì)算沖突集時(shí)使用歸結(jié)的方法.但傳統(tǒng)定理證明器效率較低，因此這些方法的實(shí)際應(yīng)用并不廣泛.

國內(nèi)學(xué)者也對(duì)沖突識(shí)別做出相關(guān)研究，如欒尚敏等人[6]提出利用系統(tǒng)結(jié)構(gòu)信息求解極小沖突集的方法，方敏[7]提出先離線求沖突然后在線求極小沖突的方法.然而，這些算法效率較低且通用性差，因此沒有得到廣泛應(yīng)用.20世紀(jì)90年代Hou[8]首次提出了利用枚舉樹求解極小沖突集的CS-Tree算法，但其算法由于剪枝策略會(huì)造成丟失解.2006年和2009年趙相福等人在CS-Tree，Inverse CS-Tree，CS-Tree with Mark Set[9]的基礎(chǔ)上分別提出2種改進(jìn)算法CSSE-Tree[10]和CSISE-Tree[11],并首次使用SAT求解器求解沖突集，使得算法效率大大提高.劉伯文等人[12]在CSISE-Tree算法上進(jìn)行改進(jìn)，提出利用集合枚舉樹SE-Tree反向深度求沖突集的算法CSRDSE.CSISE-Tree算法主要針對(duì)非沖突集進(jìn)行剪枝；而CSRDSE算法不僅對(duì)非沖突集進(jìn)行剪枝，且根據(jù)沖突集的真超集一定不是極小沖突集的思想對(duì)某些能夠確定的非極小沖突集進(jìn)行剪枝，減少了使用SAT求解器的次數(shù)，進(jìn)一步提高了求解極小沖突集的效率.

本文在對(duì)CSRDSE算法分析的基礎(chǔ)上，提出結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法MCS-SFFO(computing minimal conflict sets based on the structural feature of fault output).在MCS-SFFO算法中提出非沖突集定理——故障輸出無關(guān)元件集的子集不是沖突集，即與異常輸出不相關(guān)的元件任意組合都不是沖突集.因此，對(duì)故障輸出無關(guān)元件的任意組合都不需調(diào)用SAT求解器進(jìn)行判定.該算法在CSRDSE算法的基礎(chǔ)上進(jìn)一步對(duì)集合枚舉樹進(jìn)行無解空間的剪枝，從而減小SAT求解問題的規(guī)模.

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

本節(jié)首先介紹基于模型診斷的相關(guān)定義和概念，然后介紹SAT問題的基本概念.

1.1 基于模型診斷

定義1. 診斷系統(tǒng)[3].診斷系統(tǒng)是可用三元組(SD，COMPS，OBS)表示，分別是系統(tǒng)描述、元件集、觀測集.

定義2. 基于一致性診斷[3].設(shè)Δ?COMPS，稱Δ為關(guān)于(SD，COMPS，OBS)的基于一致性診斷，如果SD∪OBS∪{AB(c)|c∈Δ}∪{AB(c)|c∈COMPSΔ}是一致的.

稱Δ為極小診斷當(dāng)且僅當(dāng)對(duì)于Δ的任一真子集Δ′，Δ′都不是一個(gè)基于一致性的診斷.

定義3. 沖突集[3].系統(tǒng)(SD，COMPS，OBS)的沖突集CS是一個(gè)元件集合{c1，c2，…，ck}?COMPS，使得SD∪OBS∪{AB(c1)，AB(c2),…,AB(ck) }不一致.

稱某個(gè)沖突集為極小沖突集，當(dāng)且僅當(dāng)該沖突集的任意真子集都不是沖突集[8].

1.2 SAT問題

我們用xi(i=1,2,…,n)表示布爾變量.xi或xi稱作文字，其中，xi稱作變量xi的正文字，xi稱作變量xi的負(fù)文字.X={x1,x2,…,xn}表示變量的集合.Qi(i=1,2,…,m)表示子句，每一個(gè)子句是一組文字的析取式.符號(hào)Φ代表CNF公式，CNF公式是由子句的合取構(gòu)成，即合取范式CNF:Φ=Q1∧Q2∧…∧Qr，而SAT問題就是尋找是否存在一組X的賦值，使其滿足CNF公式.

定義4. SAT問題[13].SAT問題通常是指合取范式的可滿足問題.

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

第1節(jié)介紹了沖突集的概念，根據(jù)沖突集的定義可以得到2個(gè)結(jié)論：

推論1. 當(dāng)元件集C是沖突集時(shí)，C的任意嚴(yán)格超集都是非極小沖突集[12].

推論2. 當(dāng)元件集C不是沖突集時(shí)，C的任意真子集都不是沖突集[12].

通過推論可知，對(duì)沖突集的所有嚴(yán)格超集以及非沖突集的所有真子集可不必再進(jìn)行判斷.

本節(jié)介紹的SE-Tree反向深度求解沖突集算法就是運(yùn)用了上述2個(gè)推論思想對(duì)集合枚舉樹進(jìn)行剪枝，接下來介紹該算法的相關(guān)概念和算法思想.

2.1 相關(guān)概念

定義5. 集合枚舉樹[14].給定集合S，以樹結(jié)構(gòu)形式按一定順序枚舉出S中元素的所有組合，稱這樣的樹為集合枚舉樹.

設(shè)節(jié)點(diǎn)N為枚舉樹中要遍歷的節(jié)點(diǎn)，下面介紹3條剪枝規(guī)則和標(biāo)識(shí)規(guī)則.

剪枝規(guī)則1[12]. 當(dāng)N是沖突集時(shí)，將N加入到?jīng)_突集合簇中.

若N是以其父節(jié)點(diǎn)為根節(jié)點(diǎn)的子樹上最左側(cè)分支上的節(jié)點(diǎn)，則跳轉(zhuǎn)至其父節(jié)點(diǎn)；否則，跳轉(zhuǎn)至以N的下一個(gè)兄弟節(jié)點(diǎn)為根的子樹的最左節(jié)點(diǎn).

若N沒有下一個(gè)兄弟節(jié)點(diǎn)(此時(shí)N是葉節(jié)點(diǎn))，則跳轉(zhuǎn)到下一個(gè)葉節(jié)點(diǎn).

剪枝規(guī)則2[12]. 當(dāng)N不是沖突集時(shí)，將N加入到非沖突集合簇中.

若N是經(jīng)過下面節(jié)點(diǎn)回溯到的節(jié)點(diǎn)，則跳轉(zhuǎn)至N的最左側(cè)子節(jié)點(diǎn)的下一個(gè)兄弟節(jié)點(diǎn)為根節(jié)點(diǎn)的子樹的最左節(jié)點(diǎn)；否則，跳轉(zhuǎn)至其下一個(gè)兄弟節(jié)點(diǎn).

若N沒有下一個(gè)兄弟節(jié)點(diǎn)(此時(shí)N是葉節(jié)點(diǎn))，則跳轉(zhuǎn)到下一個(gè)葉節(jié)點(diǎn).

剪枝規(guī)則3[12]. 當(dāng)對(duì)N調(diào)用SAT求解器前，首先判斷N是否為非沖突集合簇中集合的子集.若是，按照剪枝規(guī)則2跳轉(zhuǎn)到下一個(gè)節(jié)點(diǎn)；否則，對(duì)N調(diào)用SAT求解器.

標(biāo)示規(guī)則[12]. 當(dāng)N是沖突集時(shí)，將N加入到?jīng)_突集合簇中，將其標(biāo)示“0”，并將沖突集合簇中N的超集標(biāo)示“1”.

2.2 CSRDSE算法

CSRDSE算法的主要思想就是基于剪枝規(guī)則和標(biāo)識(shí)規(guī)則在反向遍歷集合枚舉樹時(shí)對(duì)樹進(jìn)行剪枝.該算法偽代碼如下：

算法1. CSRDSE.

①Node=SE-Tree的最左節(jié)點(diǎn)；

② While (Node≠?)

③notCS=isunsolve(Node)；

④ If (notCS=0)

⑤judge←ISCS()；

⑥ If (judge=0)

⑦addtosolve(Node)；

⑧ 按照剪枝規(guī)則2給Node賦值；

⑨ Else

⑩addtosolve(Node)；

3 CSRDSE剪枝規(guī)則的改進(jìn)

設(shè)節(jié)點(diǎn)Leaf是SE-Tree中的一個(gè)葉節(jié)點(diǎn)，下面介紹2個(gè)定義.

定義6. 同層兄弟節(jié)點(diǎn).設(shè)節(jié)點(diǎn)F是SE-Tree的一個(gè)節(jié)點(diǎn)，若節(jié)點(diǎn)F與葉節(jié)點(diǎn)Leaf在集合枚舉樹中處于同層，且節(jié)點(diǎn)F是葉節(jié)點(diǎn)Leaf同層中相鄰的下個(gè)節(jié)點(diǎn)，則稱F為Leaf的同層兄弟節(jié)點(diǎn).

如圖1中{c1,c2,c5}的同層兄弟節(jié)點(diǎn)是{c1,c3,c4}.

Fig. 1 SE-Tree of {c1,c2,c3,c4,c5}圖1 {c1,c2,c3,c4,c5}對(duì)應(yīng)的集合枚舉樹

定義7. 子葉節(jié)點(diǎn).設(shè)節(jié)點(diǎn)F是葉節(jié)點(diǎn)Leaf的同層兄弟節(jié)點(diǎn)，若Leaf與F之間存在葉節(jié)點(diǎn)，稱這些葉節(jié)點(diǎn)是Leaf的子葉節(jié)點(diǎn).

如圖1中{c1,c2,c4,c5}的子葉節(jié)點(diǎn)是{c1,c2,c5}.

下面介紹算法CSRDSE中剪枝規(guī)則1的改進(jìn).

第2節(jié)我們提到，在算法CSRDSE剪枝規(guī)則2中，當(dāng)葉節(jié)點(diǎn)不是沖突集時(shí)，跳轉(zhuǎn)至下一個(gè)葉節(jié)點(diǎn)進(jìn)行判斷.例如圖1所示的SE-Tree中，當(dāng){c1,c3,c4,c5}不是沖突集時(shí)，需要跳轉(zhuǎn)至其子葉節(jié)點(diǎn){c1,c3,c5}，{c1,c4,c5}，{c1,c5}進(jìn)行判斷.但通過觀察可發(fā)現(xiàn){c1,c3,c5}，{c1,c4,c5}，{c1,c5}都是{c1,c3,c4,c5}的子集，因此當(dāng){c1,c3,c4,c5}不是沖突集時(shí)，根據(jù)推論2可知，它的子葉節(jié)點(diǎn)也不是沖突集，因此可省去對(duì){c1,c3,c4,c5}子葉節(jié)點(diǎn)的判斷，直接跳轉(zhuǎn)至{c2,c3,c4,c5}進(jìn)行判斷.

設(shè)葉節(jié)點(diǎn)Leaf的所有子葉節(jié)點(diǎn)組成的集合為SUB_LEAVES.通過進(jìn)一步觀察可知，在集合枚舉樹中，SUB_LEAVES中的所有元素都是葉節(jié)點(diǎn)Leaf的真子集.因此，當(dāng)節(jié)點(diǎn)F不是沖突集時(shí)，SUB_LEAVES中的任一元素都不是沖突集，因此可省去對(duì)SUB_LEAVES中所有元素的判斷，直接跳轉(zhuǎn)至以葉節(jié)點(diǎn)Leaf的同層兄弟節(jié)點(diǎn)為根節(jié)點(diǎn)的最左節(jié)點(diǎn)進(jìn)行判斷.

通過分析，剪枝規(guī)則1可改為：若N沒有下一個(gè)兄弟節(jié)點(diǎn)，則跳轉(zhuǎn)到以其同層兄弟節(jié)點(diǎn)為根節(jié)點(diǎn)的子樹的最左節(jié)點(diǎn).

為方便闡述，本文將改進(jìn)剪枝規(guī)則后的CSRDSE算法稱為CSRDSE 2.

在算法CSRDSE剪枝規(guī)則3中規(guī)定，在對(duì)某節(jié)點(diǎn)調(diào)用SAT求解器前，首先判斷其是否為非沖突集的子集.通過改進(jìn)的剪枝規(guī)則2可知，當(dāng)葉節(jié)點(diǎn)不是沖突集時(shí)，不必再判斷其子葉節(jié)點(diǎn)是否為非沖突集的子集，因此，可減少遍節(jié)點(diǎn)的次數(shù)，同時(shí)也減少了對(duì)非沖突集合簇的檢測次數(shù).

對(duì)本節(jié)提出的改進(jìn)策略的最壞情況和最好情況進(jìn)行分析，結(jié)論如下：

1) 最壞情況.當(dāng)SE-Tree的所有葉節(jié)點(diǎn)都是沖突集時(shí)，使用算法CSRDSE 2遍歷集合枚舉樹時(shí)并不能跳過葉節(jié)點(diǎn)的子葉節(jié)點(diǎn)，此時(shí)，算法CSRDSE 2與算法CSRDSE訪問節(jié)點(diǎn)次數(shù)相同，因此改進(jìn)策略失效.

2) 最好情況.當(dāng)SE-Tree的所有葉節(jié)點(diǎn)都不是沖突集時(shí)，使用算法CSRDSE 2在訪問完最左節(jié)點(diǎn)后算法結(jié)束，因此算法CSRDSE 2訪問節(jié)點(diǎn)的次數(shù)為1.而算法CSRDSE仍需遍歷全部葉節(jié)點(diǎn)，因此當(dāng)系統(tǒng)元件總數(shù)為n時(shí)，算法CSRDSE訪問節(jié)點(diǎn)的次數(shù)是2n-1，為整棵枚舉樹節(jié)點(diǎn)總數(shù)的一半.此時(shí)，算法CSRDSE 2與算法CSRDSE相比，減少了對(duì)SE-Tree中一半節(jié)點(diǎn)的訪問，同時(shí)，還避免了2n-1-1次與非沖突集合簇的檢測.

4 結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法

CSRDSE 2算法優(yōu)化了求解空間，但是進(jìn)一步分析可知，與異常輸出端無關(guān)的電路元件間的任意組合都不是沖突集.因此，本節(jié)在CSRDSE 2算法基礎(chǔ)上，提出在SE-Tree中對(duì)這些與異常輸出無關(guān)的電路元件間的所有組合進(jìn)行剪枝，進(jìn)一步縮小了SAT求解問題的規(guī)模.下面給出結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法的相關(guān)概念和算法思想.

4.1 相關(guān)概念

定義8. 故障輸出元件.對(duì)于三元組{SD,COMPS,OBS}，若存在元件c∈COMPS，c的輸出是診斷系統(tǒng)的輸出，且該輸出是系統(tǒng)的故障輸出，即該輸出的觀測值與預(yù)期不符，則稱元件c是該系統(tǒng)的故障輸出元件.

定義9. 故障輸出相關(guān)元件集.對(duì)于故障輸出元件c，稱從電路輸入到c的路徑上經(jīng)過的元件(包含c)是故障輸出相關(guān)元件.系統(tǒng)中所有故障輸出相關(guān)元件組成的集合是系統(tǒng)的故障輸出相關(guān)元件集.

定義10. 故障輸出無關(guān)元件集.設(shè)集合S是系統(tǒng)的故障輸出相關(guān)元件集，稱集合COMPSS為系統(tǒng)的故障輸出無關(guān)元件集.

為了更好地理解相關(guān)定義，下面用C17電路來舉例說明.如圖2所示：

Fig. 2 C17 circuit圖2 C17電路

在C17電路中，假設(shè)輸出端12輸出異常、輸出端13輸出正常，則c4是故障輸出元件.故障輸出相關(guān)元件集為{c1，c2，c3，c4}，故障輸出無關(guān)元件集是{c5，c6}.

4.2 求解故障輸出無關(guān)元件集算法

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

① 初始化：outABCompS=?；

EXP_OUT=?；

onABCompS=?；

unOnABCompS=?；

COMPS，從SD.cnf的第1行中獲?。?/p>

OBS_IN，從OBS.cnf中獲?。?/p>

OBS_OUT，從OBS.cnf中獲??；

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

③ While (OBS_OUT中仍有未與EXP_OUT對(duì)比的元素)

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

⑤outABCompS.add(輸出是

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

⑥ EndIf

⑦ EndWhile

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

⑨onABCompS.add(與outComp連接的元件)；

⑩ EndWhile

在算法2中，將系統(tǒng)描述、輸入觀測和系統(tǒng)所有元件正常表示的CNF形式輸入SAT求解器中，求出預(yù)期輸出EXP_OUT(行②)；將預(yù)期輸出與實(shí)際輸出對(duì)比，求出故障輸出元件集outABCompS(行③～⑦)；通過系統(tǒng)描述，求出故障輸出相關(guān)元件集onABCompS(行⑧～⑩)；最后求出故障輸出無關(guān)元件集unOnABCompS并返回(行～).

4.3 結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法

定理1. 非沖突集定理：系統(tǒng)的故障輸出無關(guān)元件集的子集不是沖突集.

證明. 反證法.設(shè)UNABCS是系統(tǒng)故障輸出無關(guān)元件集的任一子集.若UNABCS是沖突集，則根據(jù)定義3，當(dāng)UNABCS中所有元件正常時(shí)系統(tǒng)的輸出與系統(tǒng)實(shí)際輸出不一致，即與UNABCS相關(guān)的所有輸出中至少有一個(gè)是系統(tǒng)的故障輸出.而根據(jù)定義10可知，與UNABCS相關(guān)的所有輸出是系統(tǒng)的正常輸出，故二者矛盾.因此，UNABCS不是沖突集.

證畢.

根據(jù)定理1我們可以進(jìn)一步優(yōu)化CSRDSE 2算法.在構(gòu)造集合S的SE-Tree時(shí)，將故障輸出相關(guān)元件放在S的前半部分，故障輸出無關(guān)元件放在S的后半部分.例如，系統(tǒng)元件集為{c1,c2,c3,c4,c5},其中故障輸出相關(guān)元件集為{c2,c4}，故障輸出無關(guān)元件集為{c1,c3,c5}，其集合枚舉樹如圖3所示.

而通過觀察可知，樹中以{c1}，{c3}，{c5}為根節(jié)點(diǎn)的分支子樹中的所有節(jié)點(diǎn)恰好是故障輸出無關(guān)元件集{c1,c3,c5}的所有非空子集.因此，根據(jù)非沖突集定理，可將以{c1}，{c3}，{c5}為根節(jié)點(diǎn)的分支子樹剪枝，得到新的枚舉樹如圖4所示.

Fig. 3 SE-Tree圖3 集合枚舉樹

Fig. 4 SE-Tree after pruning圖4 剪枝后的集合枚舉樹

通過上述分析可知，在用CSRDSE 2算法遍歷SE-Tree的過程中，當(dāng)遍歷到的節(jié)點(diǎn)是故障輸出無關(guān)元件集的子集時(shí)，便可終止遍歷這棵樹，因?yàn)槭Ｓ嗟乃泄?jié)點(diǎn)都是故障輸出無關(guān)元件集的子集，不是沖突集.下面給出結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法MCS-SFFO.

算法3. MCS-SFFO算法.

輸入：系統(tǒng)描述的CNF文件SD.cnf、系統(tǒng)觀測的CNF文件OBS.cnf、故障輸出相關(guān)元件集onABCompS、故障輸出無關(guān)元件集unOnABCompS；

輸出：極小沖突集合簇MCSRes.

①CSRes=?，unCSRes=?，Node=?；

② 生成集合{onABCompS[0],onABCompS[1],…,onABCompS[NUM1-1],unOnAB-CompS[0],unOnABCompS[1],…,unOnABCompS[NUM2-1]}的集合枚舉樹CSTree.其中，NUM1是onABCompS[]的元素個(gè)數(shù)，NUM2是unOnABCompS的元素個(gè)數(shù)；

③Node賦值為CSTree的最左節(jié)點(diǎn)；

④ While (Node≠?)

⑤ If (Node?unOnABCompS)

⑥ Break；

⑦ Else

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

⑨ 按照剪枝規(guī)則1給Node賦值；

⑩ Else

算法3按照故障輸出相關(guān)元件在前、故障輸出無關(guān)元件在后的順序生成集合枚舉樹CSTree(行②)，并將CSTree的最左節(jié)點(diǎn)賦值給Node(行③).每次迭代節(jié)點(diǎn)Node時(shí)先判斷Node是否為故障輸出無關(guān)元件集的子集(行⑤)，若是則跳出循環(huán)(行⑥)；否則，繼續(xù)使用算法CSRDSE 2遍歷CSTree(行⑧～).當(dāng)遍歷完CSTree后，將沖突集合簇中標(biāo)識(shí)為“0”的沖突集加入到極小沖突集合簇MCSRes中(行～)，最后返回MCSRes.

根據(jù)算法3的描述可知，算法3是完備算法，因?yàn)榧厦杜e樹將組件的所有組合都枚舉出來，所有的極小沖突集會(huì)在遍歷完這棵枚舉樹之后全部產(chǎn)生，不會(huì)發(fā)生丟解.

其次，MCS-SFFO算法將故障輸出相關(guān)元件放在待枚舉的集合的前部，故障輸出無關(guān)元件集放在后部，對(duì)故障輸出無關(guān)元件間所有組合進(jìn)行剪枝，因此與CSRDSE 2算法相比，調(diào)用SAT求解器次數(shù)將會(huì)大量減少，求解效率也將會(huì)明顯提高.

算法3的復(fù)雜性分析：設(shè)系統(tǒng)元件總數(shù)為n，系統(tǒng)故障輸出無關(guān)元件個(gè)數(shù)為k，則使用MCS-SFFO算法剪枝的故障輸出無關(guān)元件集子集的節(jié)點(diǎn)個(gè)數(shù)為2k.因此當(dāng)k越大時(shí)剪枝的節(jié)點(diǎn)數(shù)越多.下面對(duì)算法的最好情況和最壞情況進(jìn)行分析：

1) 最壞情況.當(dāng)k=0，即故障輸出無關(guān)元件個(gè)數(shù)為0，此時(shí)故障輸出無關(guān)元件集子集個(gè)數(shù)為0，因此與算法CSRDSE 2相比，使用算法MCS-SFFO剪枝的節(jié)點(diǎn)個(gè)數(shù)沒有增多，算法MCS-SFFO退化為算法CSRDSE 2.

2) 最好情況.當(dāng)k=n-1，即故障輸出無關(guān)元件個(gè)數(shù)約等于元件總數(shù)時(shí)，此時(shí)故障輸出無關(guān)元件集子集個(gè)數(shù)為2k.算法MCS-SFFO剪枝步驟可分為2個(gè)，首先直接剪枝2k個(gè)故障輸出無關(guān)元件集的子集節(jié)點(diǎn)，此時(shí)剩余子樹的節(jié)點(diǎn)數(shù)也為2k；然后使用算法CSRDSE繼續(xù)對(duì)剩余子樹進(jìn)行剪枝.而算法CSRDSE仍需遍歷節(jié)點(diǎn)數(shù)為2k+1的整棵集合枚舉樹，與算法MCS-SFFO相比，多遍歷了集合枚舉樹的一半節(jié)點(diǎn).

5 實(shí)驗(yàn)結(jié)果

本節(jié)實(shí)現(xiàn)了CSRDSE 2和MCS-SFFO算法，將這2種算法與劉伯文等人[12]提出的CSRDSE算法進(jìn)行了比較并給出了實(shí)驗(yàn)結(jié)果.實(shí)驗(yàn)運(yùn)行平臺(tái)如下：Dell Dimension C521，Ubuntu 12.04 LTS，GCC編譯器，AMD Athlon(tm) 64 X2 Dual Core Processor 3600+，1.90 GHz，3 GB RAM.算法調(diào)用的SAT求解器為Picosat.

為與CSRDSE算法對(duì)比，本文測試用例仍選用文獻(xiàn)[12]中的電路，包括電路C17，F(xiàn)ulladder_1，F(xiàn)ulladder_2，F(xiàn)ulladder_3，F(xiàn)ulladder_4，F(xiàn)ulladder_5，Polybox_5，Polybox_9.在實(shí)驗(yàn)中，對(duì)每個(gè)電路給出大量觀測，然后分別用CSRDSE，CSRDSE 2，MCS-SFFO算法進(jìn)行求解.用算法MCS-SFFO求解沖突集時(shí)，首先根據(jù)系統(tǒng)描述和系統(tǒng)觀測求出電路的故障輸出相關(guān)元件集和故障輸出無關(guān)元件集，并將其保存至相應(yīng)文件內(nèi)；然后將該文件作為MCS-SFFO算法的輸入?yún)?shù)來求解極小沖突集.

表1是分別用CSRDSE和CSRDSE 2算法求解極小沖突集時(shí)平均訪問節(jié)點(diǎn)的次數(shù).其中，d表示算法CSRDSE與算法CSRDSE 2平均訪問節(jié)點(diǎn)數(shù)之差，p表示算法CSRDSE與算法CSRDSE 2平均訪問節(jié)點(diǎn)數(shù)之比.從表1可以看出，與CSRDSE算法相比，CSRDSE 2算法平均訪問節(jié)點(diǎn)次數(shù)明顯減少，并隨著電路規(guī)模的擴(kuò)大，CSRDSE 2算法效率提高越明顯.CSRDSE 2算法減少了對(duì)某些節(jié)點(diǎn)的子葉節(jié)點(diǎn)查找非沖突集合簇的次數(shù)，同時(shí)避免了與非沖突集合簇進(jìn)行子集檢測的問題，但調(diào)用SAT求解器次數(shù)與算法CSRDSE相等.

Table 1 Average Number of Access Nodes表1 平均訪問節(jié)點(diǎn)數(shù)

表2是分別用CSRDSE和MCS-SFFO算法求解極小沖突集時(shí)調(diào)用SAT求解器次數(shù).其中，d表示算法CSRDSE與算法MCS-SFFO平均調(diào)用SAT求解器次數(shù)之差，p表示算法CSRDSE與算法MCS-SFFO平均調(diào)用SAT求解器次數(shù)之比.從表2中可以看出與CSRDSE算法相比，MCS-SFFO算法調(diào)用SAT求解器次數(shù)明顯減少.對(duì)于不同電路，MCS-SFFO算法優(yōu)化程度不同.Fulladder_1電路平均提高0.06倍，而Fulladder_3電路平均提高3.48倍.這些都源于Fulladder_1與Fulladder_3電路特征的差異.Fulladder_1電路的故障輸出無關(guān)元件數(shù)占元件總數(shù)比例較小，因此使用MCS-SFFO算法剪枝的節(jié)點(diǎn)較少，效率提高不明顯;而Fulladder_3電路的故障輸出無關(guān)元件數(shù)占元件總數(shù)比例較大，使用MCS-SFFO算法剪枝的節(jié)點(diǎn)也相對(duì)較多，求解效率提高較大.

表3是MCS-SFFO，CSRDSE 2，CSRDSE算法求解極小沖突集的時(shí)間對(duì)比結(jié)果，其中最后一列表示CSRDSE與MCS-SFFO求解時(shí)間的加速比(其中因除數(shù)為0而無法運(yùn)算加速比用空白表示).從表3中可以看出，CSRDSE 2算法與CSRDSE算法相比，求解時(shí)間減少，但效率提高并不明顯；而MCS-SFFO算法與CSRDSE 2算法相比，大部分電路的求解時(shí)間明顯減少.這源于MCS-SFFO與CSRDSE 2算法遍歷節(jié)點(diǎn)數(shù)相對(duì)CSRDSE算法雖然都有減少，但CSRDSE 2算法并沒有減少調(diào)用SAT求解器的次數(shù)，只減少了掃描非沖突集合簇的次數(shù)，而MCS-SFFO大量減少了調(diào)用SAT求解器的次數(shù).而調(diào)用SAT求解器耗時(shí)較長，因此MCS-SFFO算法效率提高更加顯著.

Table 2 Average Number of SAT Call表2 平均調(diào)用SAT求解器次數(shù)

Table 3 Running Time表3 求解時(shí)間

6 結(jié)束語

基于模型診斷一直是人工智能領(lǐng)域內(nèi)重要的研究方向.隨著SAT問題的求解算法不斷優(yōu)化，使用SAT求解器求解沖突集已得到眾多學(xué)者的關(guān)注.本文在對(duì)CSRDSE算法研究的基礎(chǔ)上，提出了結(jié)合故障輸出結(jié)構(gòu)特征的極小沖突求解算法MCS-SFFO.該算法首先對(duì)CSRDSE算法的剪枝規(guī)則做出改進(jìn)，避免了對(duì)非沖突集的葉節(jié)點(diǎn)對(duì)應(yīng)子葉節(jié)點(diǎn)的訪問；其次給出求解故障輸出無關(guān)元件集的算法GetCompS，根據(jù)系統(tǒng)描述和系統(tǒng)觀測，利用SAT求解器計(jì)算出故障輸出無關(guān)元件集；最后，提出非沖突集定理——系統(tǒng)故障輸出無關(guān)元件集的子集不是沖突集，根據(jù)此定理可對(duì)SE-Tree中的故障輸出無關(guān)元件集的子集節(jié)點(diǎn)進(jìn)行剪枝，在生成SE-Tree時(shí)將故障輸出無關(guān)元件置于待枚舉集合末端，當(dāng)遍歷到的節(jié)點(diǎn)是故障輸出無關(guān)元件集的子集時(shí)，停止遍歷SE-Tree.實(shí)驗(yàn)結(jié)果表明，對(duì)CSRDSE算法的剪枝規(guī)則改進(jìn)后，訪問節(jié)點(diǎn)數(shù)大幅度減少，求解時(shí)間相對(duì)較短.MCS-SFFO算法相對(duì)于CSRDSE算法剪枝節(jié)點(diǎn)數(shù)更多，調(diào)用SAT求解器次數(shù)明顯減少.并且，隨著電路規(guī)模的擴(kuò)大，故障輸出無關(guān)元件數(shù)目也越多，因此，剪枝的節(jié)點(diǎn)個(gè)數(shù)也增多，MCS-SFFO算法效率提升更加顯著.