歐陽丹彤 周建華 劉伯文 張立明

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

基于模型診斷中結(jié)合問題特征的新方法

歐陽丹彤1,2,3周建華1,3劉伯文2,3張立明1,2,3

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

基于模型診斷一直是人工智能領(lǐng)域中熱門的研究問題.近些年來，隨著SAT求解器效率的逐漸提高，基于模型的診斷也被轉(zhuǎn)換成SAT問題進(jìn)行求解.在對基于模型診斷求解方法CSSE-tree深入研究基礎(chǔ)上,結(jié)合診斷問題和SAT求解過程的特征，給出先對包含組件個(gè)數(shù)較多的候選診斷進(jìn)行求解的方法，進(jìn)而減小SAT求解問題的規(guī)模；在對極小診斷解和非極小診斷解剪枝方法的基礎(chǔ)上，首次提出非診斷解定理及非診斷解空間的剪枝方法，有效地實(shí)現(xiàn)了對診斷的無解空間進(jìn)行剪枝.根據(jù)組件個(gè)數(shù)較多的候選診斷先求解及有解無解剪枝方法特征，構(gòu)建基于反向搜索的LLBRS-tree方法.實(shí)驗(yàn)結(jié)果表明:與CSSE-tree算法相比，LLBRS-tree算法減少了SAT求解次數(shù)、減小了求解問題規(guī)模，效率較好，尤其是求解多診斷時(shí)效率提高更為顯著.

基于模型的診斷；無解空間剪枝；合取范式；SAT求解器；枚舉樹

自1980年至今，基于模型診斷(model-based diagnosis, MBD)在人工智能領(lǐng)域一直是一個(gè)熱門的研究問題，對人工智能領(lǐng)域的推進(jìn)起到了十分重要的作用.最早的模型診斷方法由Reiter[1]于1987年提出，求解最終診斷結(jié)果的過程分為2個(gè)步驟:1)產(chǎn)生所有極小沖突集的沖突識(shí)別;2)產(chǎn)生所有極小碰集的候選產(chǎn)生.這2個(gè)步驟在得到最后的診斷結(jié)果中起著重要作用.國內(nèi)外學(xué)者對碰集求解方法做了許多研究和改進(jìn).碰集的求解方法主要分為基于枚舉的完備性算法[2-5]和基于局部搜索的非完備性算法[6-7].完備性算法雖然可以準(zhǔn)確給出碰集問題的所有解，但隨著碰集問題規(guī)模的增大，求解時(shí)間也會(huì)隨之以指數(shù)級增加.基于局部搜索的非完備性算法雖然不確定能給出特定的解，但對于大規(guī)模問題有較好效率.

國內(nèi)學(xué)者在模型診斷方法研究上也做了大量相關(guān)的工作.張健等人[8-9]給出了將診斷問題轉(zhuǎn)換為布爾公式和數(shù)學(xué)公式的混合形式描述，然后用帶有標(biāo)志子句技術(shù)的求解器進(jìn)行診斷；姜云飛等人[10]在候選診斷的分解與組合問題上給出了基于分步求解的診斷分解的方法；趙相福等人[11-13]提出利用SAT求解器來判斷一個(gè)組件集合是否是系統(tǒng)的診斷解，然后結(jié)合CSSE-tree求出所有的極小診斷求解方法；陳榮等人[14]先利用SAT求解器得到診斷系統(tǒng)對應(yīng)的沖突部件集，然后對沖突部件集調(diào)用碰集算法得到系統(tǒng)的候選診斷；歐陽丹彤等人[15]提出通過在診斷系統(tǒng)中傳播元件的輸出標(biāo)識(shí),來判斷當(dāng)前候選元件集合是否為系統(tǒng)的候選診斷的方法；欒尚敏等人[16]提出結(jié)合系統(tǒng)結(jié)構(gòu)信息來求解極小沖突集和直接求解候選診斷的方法.以上給出的診斷方法或是提高了診斷求解效率，或是減小了求解時(shí)的內(nèi)存空間消耗.

命題可滿足問題(propositional satisfiability problem，SAT)是人工智能領(lǐng)域中很活躍的一個(gè)分支，它是NP完全問題[17-19].人工智能中很多NP完全問題都可以轉(zhuǎn)換為SAT問題，然后進(jìn)行求解，而且隨著SAT求解器效率的提高，越來越多的NP問題都先轉(zhuǎn)化為SAT問題，然后進(jìn)行求解[20-22].如智能規(guī)劃問題以及模型檢測問題都可以轉(zhuǎn)化為SAT問題進(jìn)行求解[23].相應(yīng)地，MBD問題也可以轉(zhuǎn)換成SAT問題來求解.基于SAT求解器的發(fā)展，以及根據(jù)將基于模型的診斷轉(zhuǎn)換成SAT問題求解的思想，國內(nèi)學(xué)者趙相福等人給出的利用SAT求解器結(jié)合CSSE-tree求出所有的極小診斷解.在判斷一個(gè)組件集合是否是系統(tǒng)的診斷時(shí)，該文將要判斷的組件集合的補(bǔ)集中所有組件的正常行為謂詞描述、系統(tǒng)描述和觀測描述3部分文件構(gòu)造成一個(gè)CNF文件，然后調(diào)用SAT求解器去判斷可滿足性，如果可滿足，則是診斷解.基于這樣的基礎(chǔ)，該文結(jié)合CSSE-tree樹模型，根據(jù)組件集合的個(gè)數(shù)，枚舉出組件集合的所有冪集合，然后進(jìn)行一一的判斷.而且為了更加高效地求解，本文提出了2個(gè)優(yōu)化策略：1)從根結(jié)點(diǎn)開始，利用廣度優(yōu)先遍歷，對長度小的集合先判斷，直接先得到最終的極小診斷解;2)根據(jù)CSSE-tree的生成方式，利用極小診斷解的真超集一定不是極小診斷解的剪枝規(guī)則，將極小診斷解的子結(jié)點(diǎn)全部剪掉.但是，給合實(shí)際的診斷實(shí)例特征，我們可以知道在CSSE-tree中只有較少的結(jié)點(diǎn)是極小診斷解，該方法中的修剪規(guī)則只針對有解的那些結(jié)點(diǎn)，所以剪掉的結(jié)點(diǎn)數(shù)量較少.

針對CSSE-tree中只對是解的結(jié)點(diǎn)進(jìn)行剪枝這樣的缺點(diǎn)，我們在本文中提出了基于反向搜索的有解無解剪枝方法LLBRS-tree.在該方法中我們不僅剪掉是解的結(jié)點(diǎn)，而且第1次提出了無解剪枝的思想，對不是解的那些結(jié)點(diǎn)也進(jìn)行剪枝.并且在利用SAT求解器來判斷一個(gè)組件集合是否是診斷解時(shí)，我們首先對長度比較長的組件集合進(jìn)行處理，使得生成的CNF形式的文件中要判斷的子句的數(shù)量較少，因此調(diào)用SAT求解器來判斷時(shí)所耗費(fèi)的時(shí)間也將更少.

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

在本節(jié)，我們首先介紹基于模型的診斷中的相關(guān)概念，而后介紹SAT問題，最后介紹將基于模型的診斷轉(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為觀測集合，是一階謂詞公式的有限集合.

在下面我們使用一元謂詞AB(·)表示“abnormal”，AB(c)為真當(dāng)且僅當(dāng)c反常，其中c∈COMPS.

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

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

通過上面的定義可以知道，我們要判斷一個(gè)組件集合是否是系統(tǒng)的一個(gè)基于一致性的診斷集，只需要判定這個(gè)組件集合中的所有組件為反常的情況下，剩余組件的正常行為描述與診斷系統(tǒng)相關(guān)的系統(tǒng)描述以及系統(tǒng)觀測描述的邏輯是否是一致的.

而且，根據(jù)基于一致性診斷的極小診斷集的定義可以得到下面的結(jié)論：如果組件集合A是系統(tǒng)的一個(gè)基于一致性診斷的極小診斷集，且組件集合B?COMPS，組件集合C?COMPS，則有2種情況:

1) 如果組件集合A?B，那么組件集合B不是基于一致性診斷的極小診斷集；

2) 如果組件集合C?B且B不是診斷解，那么組件集合C一定不是診斷解.

上面的情況表明一個(gè)極小診斷集的真超集一定不是極小診斷集；并且進(jìn)一步說明如果一個(gè)組件集合不是診斷解，那么它的真子集一定不是診斷解.這2種情況是我們判斷診斷解以及極小診斷集的基礎(chǔ).

1.2 SAT問題

首先，我們將要用到的符號(hào)定義如下：

變量xi(i=1,2,…,m)表示布爾變量;X={x1,x2,…,xm}表示變量的集合；在子句中我們用符號(hào)xi表示與變量xi相對應(yīng)的正文字，符號(hào)xi表示與變量xi相對應(yīng)的負(fù)文字；符號(hào)Ci(i=1,2,…,n)表示子句，子句由文字的析取構(gòu)成，我們可以將子句看作是文字的集合.符號(hào)Φ，Φi(i=1,2,3,…)代表CNF公式，CNF公式是由子句的合取構(gòu)成，可以將它看成是子句的集合.在本文中，命題公式指的就是CNF公式.

SAT問題又叫做命題可滿足問題，即判斷給定的一個(gè)命題公式是不是可滿足的,其形式化的定義如下：

定義4. 命題可滿足問題[19].針對給定的一個(gè)命題公式Φ，X={x1,x2,…,xm}是該公式的變量集合，SAT問題是指是否存在一組X的賦值使得Φ的取值為真.如果存在這樣的一組賦值，那么我們則稱命題公式Φ是可滿足的，否則Φ是不可滿足的.

根據(jù)SAT問題的定義，我們只需要找到一組賦值使得給定的命題公式的取值為真，就可以判定該命題公式是可滿足的.

迄今為止，許多學(xué)者都投入到SAT問題的研究中來，每年舉行一次的SAT競賽也使得很多成熟高效的SAT求解器產(chǎn)生.對于常規(guī)的SAT求解器，都是以CNF形式的文件作為SAT求解器的輸入.針對給定的命題公式或者命題公式集合，都可以將其轉(zhuǎn)化成一個(gè)CNF形式的文件描述.例如：給定的一個(gè)命題公式集合R：{x1→x2,x2→x3,x3→x4,x4,x1}，我們可以將其表示為下面的一個(gè)CNF文件.使用數(shù)字1，2，3，4分別表示公式R中的變量x1，x2，x3，x4：

-3 4 0

-4 0

1 0

經(jīng)過上面的轉(zhuǎn)化，判定命題公式集合R是否為真時(shí)，只需要將公式R轉(zhuǎn)換成CNF文件描述，接下來調(diào)用SAT求解器對轉(zhuǎn)換后的CNF文件進(jìn)行求解就可以得到結(jié)果.如果CNF文件是可滿足的，那么命題公式R為真，否則公式R為假.

根據(jù)上面的這種思想，我們要判斷一個(gè)組件集合S是否是一個(gè)系統(tǒng)的一個(gè)基于一致性的診斷，只需要假設(shè)要判斷的組件集合S為診斷解，將COMPS-S集合中每一個(gè)組件相關(guān)的正常子句描述，系統(tǒng)描述以及系統(tǒng)的觀測描述一起構(gòu)建成一個(gè)CNF形式的文件，接下來調(diào)用SAT求解器進(jìn)行可滿足性判定即可.如果SAT求解器返回真值，那么S是系統(tǒng)的一個(gè)基于一致性診斷解.否則，S不是.

1.3 基于模型的診斷轉(zhuǎn)換成SAT問題

在本節(jié)，將介紹如何將診斷系統(tǒng)的模型以及系統(tǒng)的觀測轉(zhuǎn)換成CNF形式的文件.

給定一個(gè)診斷系統(tǒng)，本文中對其進(jìn)行建模的方式與Reiter[1]建模的方法不同，我們將使用命題邏輯對該系統(tǒng)相關(guān)的行為進(jìn)行建模.我們將使用變量來表示系統(tǒng)中的相關(guān)組件的輸入以及輸出，并且我們將對每個(gè)組件進(jìn)行編號(hào).跟診斷系統(tǒng)的定義一樣，我們也使用AB(c)和AB(c)來表示組件屬于反常模式或者正常模式.

以圖1所表示的ISCAS-85_c17為例，介紹我們是如何對診斷系統(tǒng)進(jìn)行建模，得到相對應(yīng)的CNF文件描述.根據(jù)ISCAS-85_c17的Verilog電路描述，我們得到圖1所示的邏輯電路.在該邏輯電路中有6個(gè)組件，都是與非門，分別用N1，N2，N3，N4，N5，N6來標(biāo)識(shí)出6個(gè)邏輯與非門.而“7”，“8”，“9”，“10”，“11”分別表示系統(tǒng)相應(yīng)的輸入變量，“12”，“13”分別表示系統(tǒng)的輸出變量，“14”，“15”，“16”，“17”分別表示組件內(nèi)部的連接結(jié)點(diǎn).例如變量“14”既表示組件N2的輸出，又是組件N3的輸入.

Fig. 1 Logic circuit of ISCAS-85_c17圖1 ISCAS-85_c17邏輯電路

為了將系統(tǒng)最后轉(zhuǎn)換成CNF文件的形式進(jìn)行描述，我們需將該邏輯電路ISCAS-85_c17采用CNF文件的編碼，并進(jìn)行相應(yīng)地轉(zhuǎn)換.最后，我們得到邏輯電路ISCAS-85_c17的部分CNF文件描述為C17.cnf，如圖2所示.

Fig. 2 C17.cnf圖2 C17.cnf

圖2所給的僅僅是部分系統(tǒng)描述，相應(yīng)地，我們還需要對系統(tǒng)的觀測給出CNF形式的描述.例如，當(dāng)邏輯電路ISCAS-85_c17當(dāng)前得到的觀測值為：輸入觀測點(diǎn)“7”，“8”，“9”，“10”，“11”的觀測分別為高電平，低電平，低電平，高電平，高電平；輸出觀測點(diǎn)“12”，“13”的觀測值為高電平，低電平.則我們得到系統(tǒng)觀測的CNF子句描述如下：

7 0

-8 0

-9 0

10 0

11 0

12 0

-13 0

通過上面這樣的轉(zhuǎn)換方式，我們就可以將一個(gè)診斷系統(tǒng)轉(zhuǎn)換成相應(yīng)的CNF文件描述，也就是轉(zhuǎn)換成SAT問題，然后針對該CNF文件進(jìn)行相應(yīng)地處理，調(diào)用SAT求解器對其進(jìn)行求解，最后得到診斷系統(tǒng)的診斷解，具體的算法我們在第2節(jié)進(jìn)行介紹.

2 用ISDAG算法結(jié)合枚舉樹求解所有診斷

在第1節(jié)我們將一個(gè)診斷系統(tǒng)轉(zhuǎn)換成SAT問題，本節(jié)將首先介紹判斷一個(gè)組件集合是否是診斷解的算法ISDAG，然后講解利用ISDAG算法，結(jié)合枚舉樹來求解一個(gè)給定診斷系統(tǒng)的所有基于一致性診斷的極小診斷解.

2.1 ISDAG算法

我們給出如下的一些定義，方便對算法進(jìn)行描述.

定義5. 反常單元子句表示.對于給定的一個(gè)組件，該組件的反常單元子句表示是指用正文字單元子句描述該組件.

定義6. 正常單元子句表示.對于給定的一個(gè)組件，該組件的正常單元子句表示是指用負(fù)文字單元子句描述該組件.

例如:組件N1，我們用數(shù)字“1”代表這個(gè)組件，那么組件N1的反常單元子句表示如下：

組件N1的正常單元子句表示如下：

當(dāng)給定一個(gè)診斷系統(tǒng)后，假設(shè)系統(tǒng)所對應(yīng)的描述以及觀測都已經(jīng)通過離線方式創(chuàng)建完成，正如在1.3節(jié)所述.假設(shè)系統(tǒng)描述的文件為DigSysDis.cnf以及DigSysObs.cnf，下面的ISDAG算法將介紹如何使用SAT求解器來判斷一個(gè)組件集合是否是給定診斷系統(tǒng)的基于一致性診斷的診斷解.

算法1. ISDAG(Sub[])算法.

輸入：將要判斷系統(tǒng)的一個(gè)組件子集Sub;

輸出：bool類型值，如果組件子集Sub是系統(tǒng)的基于一致性診斷，則返回1，否則返回0.

Step1. 將系統(tǒng)的觀測文件DigSysObs.cnf中的子句追加到系統(tǒng)描述文件DigSysDis.cnf中.

Step2. 對于在組件集合Sub中的每一個(gè)組件，將其對應(yīng)的反常單元子句表示(相當(dāng)于一個(gè)選擇器，表明假設(shè)該組件集合都發(fā)生故障的情況)追加到系統(tǒng)描述文件DigSysDis.cnf中.

Step3. 對于在組件集合(COMPS-Sub)中的每一個(gè)組件，將其對應(yīng)的正常單元子句表示(表明這些組件都正常工作，沒有發(fā)生故障)追加到系統(tǒng)描述文件DigSysDis.cnf中.

Step4. 調(diào)用SAT求解器對系統(tǒng)文件DigSysDis.cnf進(jìn)行可滿足性判斷，如果得到的結(jié)果是可滿足的，那么表明組件集合Sub是診斷解，返回1.如果得到的結(jié)果是不可滿足的，那么表明組件集合Sub不是診斷解，返回0.

針對ISDAG算法中的Step2，Step3我們舉例說明，假設(shè)COMPS={N1，N2，N3，N4，N5，N6}，而Sub={N1，N2，N3}時(shí)，那么在執(zhí)行Step2以及Step3后，我們加入到DigSysDis.cnf文件中的子句如下:

1 0

2 0

3 0

-4 0

-5 0

-6 0

我們要判斷一個(gè)組件子集Sub是否是系統(tǒng)的診斷，首先需要將系統(tǒng)的觀測都追加到系統(tǒng)描述文件中，然后在考慮組件集合Sub中的每一個(gè)組件都反常的情況下(相當(dāng)于指定Sub組件集合中的組件為診斷解，即加入單元子句，將其置為正文字)，也就相當(dāng)于將組件集合Sub中的每一個(gè)組件所對應(yīng)的子句置為恒真子句，接著看剩余的組件集合(COMPS-Sub)都正常的情況下，是否能正常解釋系統(tǒng)在當(dāng)前觀測下面的行為(相應(yīng)的這3步對應(yīng)算法1的Step1，Step2，Step3).最后在Step4中調(diào)用SAT求解器，看看是否能解釋系統(tǒng)在當(dāng)前狀態(tài)下的行為，如果是可滿足的，返回1，表明能解釋，那么我們假設(shè)組件集合Sub為診斷解成立，Sub是系統(tǒng)的基于一致性診斷的解.如果是不可滿足的，返回0，那么表明在假設(shè)組件集合Sub為故障的情況下，不能解釋系統(tǒng)現(xiàn)在的行為，則Sub不是系統(tǒng)的基于一致性診斷的診斷解.

ISDAG算法僅僅只能判斷一個(gè)組件集合是否是系統(tǒng)的診斷解，即只能得到系統(tǒng)的一個(gè)解，如果想要得到所有的診斷解，那么需要枚舉出所有的組件集合，然后對這些集合進(jìn)行判斷，進(jìn)一步得到所有解.

2.2 利用枚舉樹求解所有診斷解

為了求解給定診斷系統(tǒng)的所有基于一致性診斷的極小診斷解，我們只需要考慮所有可能出現(xiàn)故障的集合，假設(shè)該組件集合是故障組件集合，則調(diào)用算法ISDAG判斷該組件集合是不是診斷解.這個(gè)過程其實(shí)就是一個(gè)枚舉所有組件集合的過程，可以用枚舉樹來進(jìn)行枚舉，下面我們簡單介紹一下枚舉樹.

集合枚舉樹(set-enumeration-tree，SE-tree)是由國外學(xué)者Rymon[24]提出，這種樹模型在很大程度上可以枚舉出給定的集合中元素的所有可能的組合.例如當(dāng)前集合SS= {N1，N2，N3，N4}，則集合SS的完全集合枚舉樹如圖3所示.

根據(jù)圖3的樹模型，在求解系統(tǒng)的所有診斷的過程中，我們用這棵樹對求解過程進(jìn)行模擬.利用集合枚舉樹模型我們要求解所有的診斷解，只需要遍歷這棵樹上的所有結(jié)點(diǎn)，對每個(gè)結(jié)點(diǎn)進(jìn)行相應(yīng)地判斷就可以得到最后的解.例如，針對集合{N2,N3}，我們表示的是當(dāng)組件集合{N2,N3}都出現(xiàn)故障時(shí)，組件N1，N4正常的情況下，是否能解釋系統(tǒng)當(dāng)前的行為.那么就需要調(diào)用ISDAG算法，將組件集合{N2,N3}作為輸入?yún)?shù)，進(jìn)行判斷.如果調(diào)用ISDAG算法的返回值是1，那么表明組件集合{N2,N3}是系統(tǒng)的診斷解，如果是0，那么它就不是診斷解.當(dāng)然，為了求解所有的極小診斷解，我們只需要保留樹中其真子集不是診斷解的所有結(jié)點(diǎn)，這些結(jié)點(diǎn)就是最后的基于一致性診斷的極小診斷解.

Fig. 3 SE-tree of set SS圖3 集合SS的SE-tree

近些年以來，大部分求解系統(tǒng)的基于一致性診斷都是根據(jù)上面的枚舉樹，按照廣度優(yōu)先遍歷或者深度優(yōu)先遍歷，采用一定的剪枝規(guī)則，減少遍歷的結(jié)點(diǎn)，從而得到最后的診斷解.

趙相福等人[11-12]提出了CSSE-tree方法，CSSE-tree也是基于這樣的一棵枚舉樹，對整個(gè)枚舉樹中的結(jié)點(diǎn)進(jìn)行遍歷，然后進(jìn)行相應(yīng)的操作得到最后的極小診斷解.CSSE-tree的提出使得求解基于一致性診斷的求解時(shí)間得到了提升,它的優(yōu)點(diǎn)有2點(diǎn)：

1) 根據(jù)系統(tǒng)的組件個(gè)數(shù)，系統(tǒng)地枚舉出跟該組件集合相關(guān)冪集的所有元素，然后從根結(jié)點(diǎn)開始進(jìn)行廣度優(yōu)先遍歷，這樣保證產(chǎn)生的解集是極小診斷解，并且保證了CSSE-tree的完備性，不會(huì)丟掉任何一個(gè)解.

2) 根據(jù)極小診斷解的定義可以知道，一個(gè)極小診斷解的真超集一定不是極小診斷解.CSSE-tree利用該特征作為修剪規(guī)則，避免了所有極小診斷解真超集的判斷，而且由極小診斷解得定義保證了修剪規(guī)則的正確性.通過修剪規(guī)則可以減少一些不是極小診斷解的結(jié)點(diǎn)產(chǎn)生，使樹中的結(jié)點(diǎn)數(shù)目減少，從而使得求解的效率得到相應(yīng)的提高.

然而CSSE-tree也存在2個(gè)缺點(diǎn)：

1) 如果系統(tǒng)的組件個(gè)數(shù)太多，枚舉出跟組件集合相關(guān)冪集合的所有元素將會(huì)使得CSSE-tree變得相當(dāng)?shù)谬嫶?，使得空間復(fù)雜度相當(dāng)?shù)么?而且，如果在解很少的情況下，修剪規(guī)則的剪枝空間較少，效率提升較小.

2) 根據(jù)對實(shí)際例子的分析，我們知道枚舉樹中不是解的結(jié)點(diǎn)占據(jù)了枚舉樹中大量的結(jié)點(diǎn).CSSE-tree中的修剪規(guī)則只是對是解的那些結(jié)點(diǎn)起作用，對于不是解的那些結(jié)點(diǎn)，只能進(jìn)行逐個(gè)判斷求解.

根據(jù)上面對CSSE-tree方法的分析，我們可以知道，在求極小診斷解時(shí)，是解的結(jié)點(diǎn)只是小部分，在我們判斷的過程中，不是診斷解的結(jié)點(diǎn)占據(jù)了樹中大量的結(jié)點(diǎn).不能對非解的結(jié)點(diǎn)進(jìn)行相應(yīng)地處理是CSSE-tree方法最致命的缺點(diǎn)，如果能給出相應(yīng)的策略剪掉一些不是解的結(jié)點(diǎn)，那么求解的效率將會(huì)得到進(jìn)一步的提高.基于剪掉不是解的結(jié)點(diǎn)這樣的思想，我們提出了基于反向搜索的有解無解剪枝方法，不僅剪掉是診斷解但非極小診斷解的一些結(jié)點(diǎn)，而且剪掉樹中大部分不是解的結(jié)點(diǎn).

3 基于反向搜索的有解無解空間剪枝方法

2.2節(jié)描述了基于枚舉樹，結(jié)合ISDAG算法求診斷系統(tǒng)的所有基于一致性診斷的診斷解.然而我們發(fā)現(xiàn)枚舉樹中大量的結(jié)點(diǎn)都不是解，據(jù)此我們提出了基于反向搜索的有解無解剪枝方法.該方法不但可以剪掉是解但非極小診斷解的一些結(jié)點(diǎn)，而且也剪掉了不是解的結(jié)點(diǎn)，使得我們遍歷整棵枚舉樹的過程中，不用遍歷到所有的結(jié)點(diǎn)，只需要遍歷少量的結(jié)點(diǎn)，這樣可以加快求解所有解的過程.本節(jié)首先給出相關(guān)的一些定義，然后描述基于反向搜索的有解無解剪枝方法.

3.1 有解剪枝和無解剪枝

首先給出在這部分要用到的相關(guān)的定義：

定義7. 有解剪枝.給定一棵枚舉樹，在遍歷這棵枚舉樹時(shí)，對于樹中的某一個(gè)結(jié)點(diǎn)，如果先判斷其父結(jié)點(diǎn)或者祖先結(jié)點(diǎn)，得到的結(jié)果是可滿足的，那么該結(jié)點(diǎn)一定不是極小診斷解，可以不用對其進(jìn)行判斷.稱跳過枚舉樹中這樣結(jié)點(diǎn)的過程叫做有解剪枝.

定義8. 無解剪枝.給定一棵枚舉樹，在遍歷這棵枚舉樹時(shí)，對于樹中的某一個(gè)結(jié)點(diǎn)，如果先判斷其子結(jié)點(diǎn)或者子孫結(jié)點(diǎn)，得到的結(jié)果是不可滿足，那么可以跳過該結(jié)點(diǎn)，不用對這個(gè)結(jié)點(diǎn)進(jìn)行判斷.我們稱跳過判斷枚舉樹中這樣結(jié)點(diǎn)的過程叫做無解剪枝.

定義7和定義8是基于原理基于極小診斷的定義，即如果一個(gè)組件集合是極小診斷解，那么其真超集一定不是極小診斷解；如果一個(gè)組件集合不是診斷解，那么其真子集一定不是診斷解.

定義9. 反向搜索.針對一棵枚舉樹，當(dāng)枚舉樹的層數(shù)已經(jīng)給定時(shí)，稱從枚舉樹的最后一層向枚舉樹的根結(jié)點(diǎn)搜索的過程為樹的反向搜索.

根據(jù)反向搜索的定義，只需要從樹的最后一層向根結(jié)點(diǎn)進(jìn)行向上搜索即可，在中間這些層之間，可以是自上向下，也可以是自下而上.并且，在訪問中間層這些結(jié)點(diǎn)時(shí)并沒有固定的順序，只需要遍歷整棵樹的所有結(jié)點(diǎn)就可以.

為了解釋上面的定義，我們舉例說明，如S={N1，N2，N3，N4}的部分枚舉樹如圖4所示：

Fig. 4 Part SE-tree of set S圖4 集合S的部分枚舉樹

在這棵枚舉樹中，除了根結(jié)點(diǎn)以外，一共有14個(gè)結(jié)點(diǎn)，為了得到所有的解，我們要遍歷樹上的所有結(jié)點(diǎn).對這棵樹進(jìn)行反向搜索時(shí)，我們先遍歷最后一層的一些結(jié)點(diǎn)，如{N1,N2,N3}，{N1,N2,N4}，然后遍歷第2層的結(jié)點(diǎn){N1,N2}；接著再去遍歷第3層的結(jié)點(diǎn){N1,N3,N4}、第2層的結(jié)點(diǎn){N1,N3}，{N1,N4}、第1層的結(jié)點(diǎn){N1}.根據(jù)這樣的遍歷方式，我們可以遍歷結(jié)點(diǎn){N2}，{N3}，{N4}這些結(jié)點(diǎn)以及這些結(jié)點(diǎn)的子孫結(jié)點(diǎn).

在求診斷解的過程中，在進(jìn)行反向搜索時(shí)，我們需要一邊遍歷結(jié)點(diǎn)、一邊對結(jié)點(diǎn)調(diào)用SAT求解器進(jìn)行判斷.在這個(gè)過程中，根據(jù)結(jié)點(diǎn)的判斷結(jié)果，可以知道樹中的某些結(jié)點(diǎn)可以不用遍歷，那么可以跳過樹中一些結(jié)點(diǎn)的判斷過程，減少調(diào)用SAT求解器的次數(shù)，這就是剪枝過程.剪枝的過程可能是針對是解的那些結(jié)點(diǎn)，也有可能是針對不是解的那些結(jié)點(diǎn)，也就是有解剪枝和無解剪枝過程.例如，對于上面的這棵枚舉樹，我們基于反向搜索以及有解剪枝和無解剪枝的思想，求解極小診斷解的過程如下：

針對上面的這棵枚舉樹，樹中一共有第1層的{N1}，{N2}，{N3}，{N4}這4個(gè)結(jié)點(diǎn)以及它們的子樹構(gòu)成了這棵樹.對這4個(gè)結(jié)點(diǎn)處理的方式是一樣的，只對結(jié)點(diǎn){N1}進(jìn)行舉例說明.針對結(jié)點(diǎn){N1}及其子孫結(jié)點(diǎn)，我們首先判斷最后一層結(jié)點(diǎn){N1,N2,N3}的可滿足性，如果該結(jié)點(diǎn)是可滿足的，那么向上回溯，判斷{N1,N2}結(jié)點(diǎn).否則，根據(jù)無解剪枝的定義，可以剪掉結(jié)點(diǎn){N1,N2}，接著繼續(xù)判斷結(jié)點(diǎn){N1,N2,N4}.如果{N1,N2,N3}可滿足，{N1,N2}也可滿足，那么根據(jù)有解剪枝的定義，可以剪掉結(jié)點(diǎn){N1,N2,N4}，然后向上回溯判斷結(jié)點(diǎn){N1}.否則如果{N1,N2}不可滿足，那么結(jié)點(diǎn){N1}被剪掉，接著判斷{N1,N2,N4}，然后是{N1,N3,N4}.如果結(jié)點(diǎn){N1,N2,N3}，{N1,N2}，{N1}都可滿足，那么根據(jù)有解剪枝的定義，結(jié)點(diǎn){N1}下面的所有其他結(jié)點(diǎn)都被剪掉，接著判斷以{N2}為根的子樹，判斷{N2,N3,N4}.否則如果{N1}不可滿足，那么我們接著判斷{N1,N3,N4}.到了判斷{N1,N3,N4}時(shí)，我們按照判斷{N1,N2,N3}的模式繼續(xù)判斷即可.在存儲(chǔ)極小解的過程中，我們將可滿足的解存起來，但是如果新來一個(gè)解，我們會(huì)判斷是否是已經(jīng)存在解的子集，如果是，那么將會(huì)更新原來的解，否則將新解加入到解集中.

根據(jù)上面的求解思路，我們在3.2節(jié)給出基于反向搜索的有解無解空間剪枝算法.

3.2 基于反向搜索的有解無解空間剪枝算法

基于有解剪枝和無解剪枝這樣的思想，我們可以從枚舉樹的第1層最左邊的第1棵子樹開始，對第1層的每個(gè)結(jié)點(diǎn)以及子樹按相同方式處理即可.針對每一棵子樹，我們先判斷其最左邊的結(jié)點(diǎn)，如果是可滿足的，我們反向搜索，判斷其父結(jié)點(diǎn)，并且將其根據(jù)有解剪枝的定義，將該結(jié)點(diǎn)還沒有訪問的子孫結(jié)點(diǎn)都剪掉.如果是不可滿足，那么可以根據(jù)無解剪枝的定義，跳過對該節(jié)點(diǎn)父節(jié)點(diǎn)的遍歷，然后接著判斷該結(jié)點(diǎn)右邊的結(jié)點(diǎn).

那么下面我們給出該算法的偽代碼：

算法2. LLBRS-tree算法.

輸入:系統(tǒng)描述的CNF文件DigSysDis.cnf、系統(tǒng)觀測的CNF文件DigSysObs.cnf、極小診斷的最大診斷長度MiniDigLen;

輸出:極小診斷解的集合.

局部變量:診斷解集合DigRes[]、診斷系統(tǒng)組件的個(gè)數(shù)ComNum、枚舉樹的總層數(shù)DigTreeLevel、待判斷的第1層的某個(gè)結(jié)點(diǎn)及其子樹Sub-tree.

Step1. 初始化:DigRes=?，ComNum=0,DigTreeLevel=0.

Step2. 從文件DigSysDis.cnf中的第1行中讀取出診斷系統(tǒng)中組件的個(gè)數(shù)，賦值給變量ComNum，然后根據(jù)輸入的最小診斷長度MiniDigLen，賦值給變量DigTreeLevel.然后根據(jù)局部變量ComNum，DigTreeLevel的值，生成集合{1,2,3,…,ComNum}的局部集合枚舉樹DigSE-tree，DigTreeLevel是DigSE-tree的最大層數(shù)(根結(jié)點(diǎn)默認(rèn)為第0層).

Step3. 將DigSE-tree的第1層最左邊的結(jié)點(diǎn)及其子樹賦值給Sub-tree.

Step4. while(DigSE-tree中存在第1層結(jié)點(diǎn)及其子樹還沒判斷).

Step4.1. while(Sub-tree判斷未完成)

對該子樹最底層的最左邊的結(jié)點(diǎn)調(diào)用ISDAG算法判斷;

if (該結(jié)點(diǎn)可滿足)

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

② 有解剪枝，將該結(jié)點(diǎn)的沒有訪問過的子孫結(jié)點(diǎn)剪掉;

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

else

① 無解剪枝，將該結(jié)點(diǎn)的父結(jié)點(diǎn)剪掉；

② 對該結(jié)點(diǎn)的右邊的結(jié)點(diǎn)進(jìn)行判斷；

end if

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

Step5. 返回集合DigRes.

1) 該算法是完備的，會(huì)得到所有的極小診斷解，不會(huì)出現(xiàn)丟掉一部分解的情況.因?yàn)槲覀冇靡豢妹杜e樹的形式將所有可能出現(xiàn)的情況都一一列舉出來，所以不會(huì)出現(xiàn)丟解，所有的極小診斷解在遍歷完這棵樹以后全部產(chǎn)生.

2) 通過對第2節(jié)的ISDAG算法分析可以發(fā)現(xiàn)，在ISDAG算法中的Step2這一步，當(dāng)我們向系統(tǒng)描述文件DigSysDis.cnf中添加的反常單元子句的數(shù)目越多時(shí)，那么意味著單元傳播的次數(shù)將會(huì)很多，文件DigSysDis.cnf中可滿足的子句數(shù)目也會(huì)大大地增加，繼而調(diào)用SAT求解器對該文件進(jìn)行可滿足性判斷的時(shí)間也將會(huì)相應(yīng)地縮短.在LLBRS-tree算法中，我們先對長度長的結(jié)點(diǎn)進(jìn)行判斷，這些結(jié)點(diǎn)的長度與極小診斷解的最大長度相等，那么相應(yīng)地在調(diào)用ISDAG算法時(shí)，使得在調(diào)用SAT求解器對DigSysDis.cnf文件處理的時(shí)間縮短.同時(shí)，先對長度最長的結(jié)點(diǎn)進(jìn)行處理，那么我們可以進(jìn)行無解剪枝的過程，這樣在反向搜索向上判斷時(shí)可以剪掉大量不是診斷解的結(jié)點(diǎn).所以，利用LLBRS-tree算法去求解給定系統(tǒng)的基于一致性診斷的極小診斷時(shí)，時(shí)間效率將會(huì)得到大大地提高.

3) 算法LLBRS-tree的時(shí)間復(fù)雜度以及空間復(fù)雜度主要取決于樹中遍歷的結(jié)點(diǎn)數(shù)目.在生成該樹時(shí)，我們可以用自動(dòng)機(jī)去模擬樹中結(jié)點(diǎn)的生成，并且隨著結(jié)點(diǎn)的生成與判斷，樹中的大量結(jié)點(diǎn)都會(huì)被有解剪枝和無解剪枝剪掉，從而調(diào)用SAT的次數(shù)也是大大地減少.當(dāng)我們在處理組件個(gè)數(shù)不是很多，且求解的是單雙診斷時(shí)，效率可能不是很明顯.但是當(dāng)組件個(gè)數(shù)很多時(shí)，無解剪枝將會(huì)剪掉大量的結(jié)點(diǎn)，求解的時(shí)間將會(huì)得到大大地縮短.

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

本節(jié)我們對趙相福等人提出的CSSE-trees算法和本文提出的LLBRS-tree算法進(jìn)行了實(shí)現(xiàn)，同時(shí)將2個(gè)算法進(jìn)行多方面地比較.測試環(huán)境為：Dell Dimension C521，Ubuntu 12.04 LTS，GCC編譯器，AMD AthlonTM64 X2 Dual Core Processor 3600+，1.90 GHz，3 GB RAM.其中在算法ISDAG中，我們調(diào)用的SAT求解器是Picosat[25]，該求解器在SAT比賽中也取得了不錯(cuò)的成績，而且該求解器的接口寫得很詳細(xì)，在使用接口時(shí)很方便，所以我們選擇了該求解器.

我們使用的測試用例均來自于基準(zhǔn)電路ISCAS-85[26]中7個(gè)電路，它們分別是c17，c432，c499，c880，c1355，c2670，c3540.我們首先通過這些電路的電路描述得到各個(gè)電路的系統(tǒng)描述文件DigSysDis.cnf，然后根據(jù)給出的觀測值得到系統(tǒng)的觀測文件DigSysObs.cnf，這些CNF形式的文件都是離線構(gòu)造.然后我們分別使用CSSE-tree算法和LLBRS-tree算法對ISCAS-85的這幾個(gè)電路進(jìn)行多次測試，記錄了相關(guān)的求解時(shí)間.我們分別用2種算法對這些電路求解長度為1，2，3的極小診斷，得到的結(jié)果如表1所示:

Table 1 Solution Time

×：Timeout.

從表1中可以看出，在極小診斷解得最大長度為1時(shí)，算法LLBRS-tree跟算法CSSE-tree的求解時(shí)間基本持平，“×”表示在1 h內(nèi)求解失敗.這是因?yàn)楫?dāng)極小診斷解的最大長度為1時(shí)，2個(gè)算法都需要遍歷枚舉樹中的所有結(jié)點(diǎn)，沒有剪枝的情況，所以2個(gè)算法的時(shí)間基本一樣.但是當(dāng)極小診斷解的最大長度為2和3時(shí)，算法LLBRS-tree的求解時(shí)間比算法CSSE-tree的時(shí)間少了很多.算法LLBRS-tree的時(shí)間在平均情況下提高了5%左右，而且在極小診斷解的最大長度為3時(shí)，有些例子可以達(dá)到8%.這是因?yàn)殡S著極小診斷解的最大長度的增加，枚舉樹的層數(shù)相應(yīng)地增加，樹中結(jié)點(diǎn)的數(shù)目也增加，那么樹中不是解的結(jié)點(diǎn)個(gè)數(shù)多于是解的結(jié)點(diǎn)個(gè)數(shù).在這樣的情況下，LLBRS-tree算法將會(huì)對枚舉樹進(jìn)行無解剪枝和有解剪枝，遍歷求解的結(jié)點(diǎn)數(shù)也將少于CSSE-tree算法，所以效率得到了提高.為了說明LLBRS-tree算法遍歷的結(jié)點(diǎn)數(shù)目小于CSSE-tree算法遍歷的結(jié)點(diǎn)數(shù)目，我們給出2個(gè)算法剪掉的結(jié)點(diǎn)個(gè)數(shù)，如表2所示.

由于單診斷并沒有涉及到有解剪枝和無解剪枝的情況，所以我們在表2中只給出了2診斷和3診斷的結(jié)點(diǎn)剪枝情況，“×”表示在1 h內(nèi)求解失敗.而且針對c1908，c2670，c3540這3個(gè)電路，我們設(shè)置的求解時(shí)間限制是10 000 s，但是由于這3個(gè)電路的組件個(gè)數(shù)過多，所以2個(gè)算法都超出了時(shí)間的限制.根據(jù)表2中的雙診斷剪枝結(jié)點(diǎn)的信息，由Δ這一列的差值信息Δ=(LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)-CSSE-tree剪掉的結(jié)點(diǎn)數(shù))可以看出，由于存在無解剪枝的情況，而且伴隨著有解剪枝，LLBRS-tree算法剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)多于CSSE-tree算法剪掉的結(jié)點(diǎn)數(shù)目.而且當(dāng)我們求解3診斷時(shí)，枚舉樹中的結(jié)點(diǎn)數(shù)目急劇增加，算法LLBRS-tree的作用更加地顯現(xiàn)出來.從3診斷的Δ那一列數(shù)據(jù)，我們看出：算法LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)遠(yuǎn)遠(yuǎn)大于算法CSSE-tree剪掉的結(jié)點(diǎn)數(shù)目，有的例子剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)高出CSSE-tree算法的十幾倍.這是因?yàn)?，隨著枚舉樹的層數(shù)增加，樹中不可滿足的結(jié)點(diǎn)數(shù)目也大大地增加了，那么算法LLBRS-tree的無解剪枝策略將會(huì)發(fā)揮關(guān)鍵的作用，所以剪掉的結(jié)點(diǎn)數(shù)目遠(yuǎn)遠(yuǎn)大于算法CSSE-tree.基于這樣的原因，算法LLBRS-tree在求解的過程中所消耗的時(shí)間才會(huì)小于CSSE-tree算法.而且，隨著枚舉樹的層數(shù)增加，也就是當(dāng)極小診斷解的最大長度增加時(shí)，樹中不是解的結(jié)點(diǎn)數(shù)目還會(huì)不斷地增加，遠(yuǎn)遠(yuǎn)大于是解的結(jié)點(diǎn)數(shù)目，那么算法LLBRS-tree的無解剪枝剪掉的結(jié)點(diǎn)也將會(huì)大幅度地增加，該算法的效率也會(huì)彰顯出來，而CSSE-tree算法的效率將會(huì)變得越來越慢，更有可能內(nèi)存溢出的情況.我們分別用2種算法針對組件個(gè)數(shù)適中的幾個(gè)測試用例求解多診斷得到的結(jié)果如表3所示.

Table 2 Numbers of Cut Node

×: Timeout.

Table 3 Time of Multi-Diagnosis

M.O: Out of memory.

從表3中可以看出，在求解多診斷時(shí)，算法LLBRS-tree的求解時(shí)間遠(yuǎn)遠(yuǎn)小于算法CSSE-tree.測試用例為c432并且診斷長度為4時(shí)，算法CSSE-tree求解時(shí)間是算法LLBRS-tree的2.6倍；但是當(dāng)求解5診斷時(shí)，卻是3.3倍；并且當(dāng)診斷長度為6時(shí)，CSSE-tree算法出現(xiàn)了內(nèi)存溢出的情況，而算法LLBRS-tree仍然能求解.當(dāng)測試用例為c499和c880時(shí)，伴隨著組件個(gè)數(shù)和診斷長度的增加，算法CSSE-tree更早的出現(xiàn)了內(nèi)存溢出的情況，而算法LLBRS依舊能正常的工作.這是因?yàn)樗惴↙LBRS-tree針對無解剪枝空間進(jìn)行大量剪枝，加上有解空間的剪枝，使得需要判斷的結(jié)點(diǎn)很少.而算法LLBRS生成大量的結(jié)點(diǎn)進(jìn)行判斷，導(dǎo)致了內(nèi)存溢出.重要的是，根據(jù)LLBRS-tree算法的求解時(shí)間我們可以發(fā)現(xiàn)，即使診斷長度增加，該算法的求解時(shí)間也是平緩的增加，不會(huì)出現(xiàn)劇烈的抖動(dòng).這是由于有解無解剪枝策略在求解過程中起到重要的作用.為了更加清晰地說明這種情況，我們對測試用例c432求多診斷得到結(jié)果如圖5所示：

Fig. 5 Comparison chart of multi-diagnosis (ISCAS-85_c432)圖5 多診斷時(shí)間對比圖(ISCAS-85_c432)

圖5是算法LLBRS-tree和算法CSSE-tree針對電路c432(160個(gè)組件)求解診斷1～10的時(shí)間對比圖.從圖5我們可以看出，在求解3診斷以前，2個(gè)算法的時(shí)間相差幾乎沒有太大的差距.但是在求解4～5診斷時(shí)，從2條線的斜率可以看出，算法LLBRS-tree的時(shí)間增加很平緩，而CSSE-tree算法求解的時(shí)間急劇增加.而且更重要的是，算法LLBRS-tree在求解6～10診斷時(shí)，時(shí)間依舊很平緩地增加，不會(huì)出現(xiàn)急劇增加的情況，但是算法CSSE-tree卻只能求到5診斷，6～10診斷出現(xiàn)了內(nèi)存溢出的情況，不能求出結(jié)果.這是因?yàn)闃渲薪Y(jié)點(diǎn)的數(shù)目急劇地增加，算法CSSE-tree剪掉的結(jié)點(diǎn)很少，隨著結(jié)點(diǎn)的膨脹，所以算法出現(xiàn)了內(nèi)存溢出的情況.而算法LLBRS-tree進(jìn)行無解剪枝，剪掉大量不是解的結(jié)點(diǎn)，所以針對多診斷，依舊能正常地運(yùn)行.

由上面的實(shí)驗(yàn)結(jié)果可以知道，對于沒有應(yīng)用無解空間剪枝策略的求解算法，當(dāng)組件集合增加，極小診斷長度加大，并且診斷解分布在集合枚舉樹的右側(cè)時(shí)，算法的時(shí)間復(fù)雜性是指數(shù)級.但是應(yīng)用本文提出的有解和無解剪枝策略后，樹中不是診斷解的結(jié)點(diǎn)將會(huì)被減掉大部分，算法的時(shí)間復(fù)雜度將小于指數(shù)級.由于受到具體診斷實(shí)例的輸入和輸出觀測影響，基于模型診斷算法的時(shí)間復(fù)雜度將會(huì)變得十分復(fù)雜，這也將成為我們以后研究工作的一部分.

5 結(jié)束語

基于模型診斷在人工智能領(lǐng)域一直以來都備受關(guān)注，從問題的提出到現(xiàn)在，越來越多的人投入到該問題的研究中.基于極小診斷解的真超集一定不是極小診斷解的原理，CSSE-tree對枚舉樹進(jìn)行了修剪，提高了診斷求解效率.但是CSSE-tree只是針對是解的結(jié)點(diǎn)進(jìn)行剪枝，并沒有考慮不是解的結(jié)點(diǎn).本文首次提出對無解進(jìn)行剪枝的思想，并結(jié)合有解剪枝給出LLBRS-tree診斷求解方法.

在LLBRS-tree算法中，根據(jù)包含組件個(gè)數(shù)較多的候選診斷解對應(yīng)的SAT問題規(guī)模較小的特點(diǎn)，先對包含組件個(gè)數(shù)較多的結(jié)點(diǎn)進(jìn)行判斷，進(jìn)而從減少求解問題規(guī)模的角度提高診斷求解效率.算法LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)目遠(yuǎn)大于算法CSSE-tree，所以求解所用的時(shí)間更短，效率高于算法CSSE-tree.尤其在求解多診斷時(shí)，所要枚舉結(jié)點(diǎn)的數(shù)目急劇增加，算法CSSE-tree只對有解進(jìn)行剪枝，剪掉的結(jié)點(diǎn)較少.而算法LLBRS-tree進(jìn)行無解和有解剪枝，在剪掉有解空間基礎(chǔ)上還剪掉大量不是解的結(jié)點(diǎn).所以，在求解多診斷時(shí)，算法LLBRS-tree剪掉的結(jié)點(diǎn)更多，與算法CSSE-tree相比，效率有更大提高.

在后續(xù)的工作中，我們考慮利用增量SAT求解器來求解基于模型的診斷，只需要一次調(diào)用SAT求解器，就可以得到多個(gè)解，這樣求解效率會(huì)得到進(jìn)一步提升.

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

[2]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal hitting sets based on join relation[J].IEEE Trans on Systems Man Cybernetics-Systems, 2015, 45(7): 1063-1076

[3]Jiang Yunfei, Lin Li. The computation of hitting sets with boolean formulas[J]. Chinese Journal of Computers, 2003, 26(8): 919-924 (in Chinese)(姜云飛, 林笠. 用布爾代數(shù)方法計(jì)算最小碰集[J].計(jì)算機(jī)學(xué)報(bào), 2003, 26(8): 919-924)

[4]Zhang Liming, Ouyang Dantong, Zeng Hailin. Computing the minimal hitting set based on dynamic maximum degree[J]. Journal of Computer Research and Development, 2011, 48(2): 209-215 (in Chinese) (張立明, 歐陽丹彤, 曾海林. 基于動(dòng)態(tài)極大度的極小碰集求解方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2011, 48(2): 209-215)

[5]Wang Yiyuan, Ouyang Dantong, Zhang Liming, et al. A method of computing minimal hitting sets using CSP[J]. Journal of Computer Research and Development, 2015, 52(3): 588-595 (in Chinese) (王藝源, 歐陽丹彤, 張立明，等. 利用CSP求解極小碰集的方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2015, 52(3): 588-595)

[6]Huang Jie, Chen Lin, Zou Peng. Computing minimal diagnosis by compounded genetic and simulated annealing algorithm[J]. Journal of Software, 2004, 15(9): 1345-1350 (in Chinese)(黃杰, 陳琳, 鄒鵬. 一種求解極小碰集的遺傳模擬退火算法[J]. 軟件學(xué)報(bào), 2004, 15(9): 1345-1350)

[7]Liu Juan, Ouyang Dantong, Wang Yiyuan, et all. Computing minimal hitting sets with particle swarm optimization combined characteristics learning[J]. Acta Electronica Sinica, 2015, 43(5): 841-845 (in Chinese) (劉娟, 歐陽丹彤, 王藝源, 等. 結(jié)合特征學(xué)習(xí)的粒子群求解極小碰集方法[J]. 電子學(xué)報(bào), 2015, 43(5): 841-845)

[8]Chen Yunji, Zhang Jian, Shen Haihua. A SAT-Based arithmetic circuit bug-hunting method[J]. Chinese Journal of Computers, 2007, 30(12): 2082-2089 (in Chinese) (陳云霽, 張健, 沈海華. 一種基于 SAT 的運(yùn)算電路查錯(cuò)方法[J]. 計(jì)算機(jī)學(xué)報(bào), 2007, 30(12): 2082-2089)

[9]Zhang Jian, Ma Feifei, Zhang Zhiqiang. Faulty interaction identification via constraint solving and optimization[G]Theory and Applications of Satisfiability Testing-SAT. Berlin: Springer, 2012: 186-199

[10]Zhang Xuenong, Jiang Yunfei, Chen Aixiang, et al. A gradual approach for model-based diagnosis[J]. Journal of Software, 2008, 19(3): 584-593 (in Chinese) (張學(xué)農(nóng), 姜云飛, 陳藹祥，等. 基于模型診斷的分步求解[J]. 軟件學(xué)報(bào), 2008, 19(3): 584-593)

[11]Zhao Xiangfu, Zhang Liming, Ouyang Dantong, et al. Deriving all minimal consistency-based diagnosis sets using SAT solvers[J]. Progress in Natural Science, 2009, 19(4): 489-494

[12]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)

[13]Zhang Liming, Zeng Hailin, Yang Fang, et al. Dynamic theorem proving algorithm for consistency-based diagnosis[J]. Expert Systems With Applications, 2011, 38(6): 7511-7516

[14]Chen Rong, Gao Jian, Zhang Weishi. Digital circuit fault diagnosis method and system based on logic compatibility [P]. Chinese: CN102156772A, 2011-08-17 (in Chinese)(陳榮, 高健, 張維石. 基于邏輯相容性的數(shù)字電路故障診斷方法及系統(tǒng)[P]. 中國: CN102156772A, 2011-08-17)

[15]Ouyang Dantong, Zhang Liming, Zhao Jian. 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)

[16]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)(欒尚敏, 戴國忠. 利用結(jié)構(gòu)信息的故障診斷方法[J]. 計(jì)算機(jī)學(xué)報(bào), 2005, 28(5): 801-808)

[17]Xu Ke, Boussemart F, Hemery F, et al. Random constraint satisfaction: Easy generation of hard (satisfiable) instances[J]. Artificial Intelligence, 2007, 171(8): 514-534

[18]Xu Ke, Li Wei. Exact phase transitions in random constraint satisfaction problems[J]. Journal of Artificial Intelligence Research, 2000, 12(1): 93-103

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

[20] 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: AAAI, 2014: 2703-2709

[21]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 Int. Menlo Park: AAAI, 2013: 489-495

[22]Cai Shaowei, Su Kaile. Local search for Boolean Satisfiability with configuration checking and subscore[J]. Artificial Intelligence, 2013, 204(9): 75-98

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

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

[25]Biere A. PicoSAT essentials[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4(20): 75-97

[26]Metodi A, Stern R, Kalech M, et al. A novel SAT-based approach to model based diagnosis[J]. Journal of Artificial Intelligence Research, 2014, 51(1): 377-411

Ouyang Dantong, 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).

Zhou Jianhua, born in 1991. Master candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning.

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

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

A New Algorithm Combining with the Characteristic of the Problem for Model-Based Diagnosis

Ouyang Dantong1,2,3, Zhou Jianhua1,3, Liu Bowen2,3, and Zhang Liming1,2,3

1(CollegeofSoftware,JilinUniversity,Changchun130012)2(CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012)3(KeyLaboratoryofSymbolicComputationandKnowledgeEngineering(JilinUniversity),MinistryofEducation,Changchun130012)

Model-based diagnosis has been popular in the field of artificial intelligence. In recent years, with a gradual increase of the efficiency of SAT solvers, model-based diagnosis is converted into SAT problem. After deeply studying CSSE-tree algorithm—a method for solving model-based diagnosis, combining with the characteristics of diagnose problem and SAT solving process, we solve the problem by diagnosing the candidate solutions which contain more elements first, thereby reducing the scale of SAT problem. Based on the minimal diagnostic solutions and non-minimal pruning methods on diagnostic solutions, we firstly propose a non-diagnostic solution theorem and a non-solution space pruning algorithm, which implements the non-solution space pruning effectively. We first solve the candidate solutions which contain more elements. According to the features of solution and non-solution method, we construct LLBRS-tree method based on reverse search. Experimental results show that compared with the algorithm of CSSE-tree, the algorithm of LLBRS-tree has less number of SAT solving, has smaller scale of the problem, better efficiency, especially when solving multiple diagnose problems its efficiency is more significant.

model-based diagnosis; non-solution space pruning; conjunctive normal form; SAT solver; set-enumeration-tree

2015-11-03；

2016-04-13

國家自然科學(xué)基金項(xiàng)目(61672261,61502199,61402196,61272208);浙江省自然科學(xué)基金項(xiàng)目(LY16F020004) This work was supported by the National Natural Science Foundation of China (61672261, 61502199, 61402196, 61272208) and the Natural Science Foundation of Zhejiang Province of China (LY16F020004).

張立明(limingzhang@jlu.edu.cn)

TP18