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

歐陽(yáng)丹彤 周建華 劉伯文 張立明

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

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

歐陽(yáng)丹彤1,2,3周建華1,3劉伯文2,3張立明1,2,3

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

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

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

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

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

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

針對(duì)CSSE-tree中只對(duì)是解的結(jié)點(diǎn)進(jìn)行剪枝這樣的缺點(diǎn)，我們?cè)诒疚闹刑岢隽嘶诜聪蛩阉鞯挠薪鉄o(wú)解剪枝方法LLBRS-tree.在該方法中我們不僅剪掉是解的結(jié)點(diǎn)，而且第1次提出了無(wú)解剪枝的思想，對(duì)不是解的那些結(jié)點(diǎn)也進(jìn)行剪枝.并且在利用SAT求解器來(lái)判斷一個(gè)組件集合是否是診斷解時(shí)，我們首先對(duì)長(zhǎng)度比較長(zhǎng)的組件集合進(jìn)行處理，使得生成的CNF形式的文件中要判斷的子句的數(shù)量較少，因此調(diào)用SAT求解器來(lái)判斷時(shí)所耗費(fèi)的時(shí)間也將更少.

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

在本節(jié)，我們首先介紹基于模型的診斷中的相關(guān)概念，而后介紹SAT問(wèn)題，最后介紹將基于模型的診斷轉(zhuǎn)換成SAT問(wèn)題.

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”，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è)基于一致性診斷.

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

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

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

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

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

1.2 SAT問(wèn)題

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

變量xi(i=1,2,…,m)表示布爾變量;X={x1,x2,…,xm}表示變量的集合；在子句中我們用符號(hào)xi表示與變量xi相對(duì)應(yīng)的正文字，符號(hào)xi表示與變量xi相對(duì)應(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問(wèn)題又叫做命題可滿足問(wèn)題，即判斷給定的一個(gè)命題公式是不是可滿足的,其形式化的定義如下：

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

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

迄今為止，許多學(xué)者都投入到SAT問(wèn)題的研究中來(lái)，每年舉行一次的SAT競(jìng)賽也使得很多成熟高效的SAT求解器產(chǎn)生.對(duì)于常規(guī)的SAT求解器，都是以CNF形式的文件作為SAT求解器的輸入.針對(duì)給定的命題公式或者命題公式集合，都可以將其轉(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)過(guò)上面的轉(zhuǎn)化，判定命題公式集合R是否為真時(shí)，只需要將公式R轉(zhuǎn)換成CNF文件描述，接下來(lái)調(diào)用SAT求解器對(duì)轉(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)的觀測(cè)描述一起構(gòu)建成一個(gè)CNF形式的文件，接下來(lái)調(diào)用SAT求解器進(jìn)行可滿足性判定即可.如果SAT求解器返回真值，那么S是系統(tǒng)的一個(gè)基于一致性診斷解.否則，S不是.

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

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

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

以圖1所表示的ISCAS-85_c17為例，介紹我們是如何對(duì)診斷系統(tǒng)進(jìn)行建模，得到相對(duì)應(yīng)的CNF文件描述.根據(jù)ISCAS-85_c17的Verilog電路描述，我們得到圖1所示的邏輯電路.在該邏輯電路中有6個(gè)組件，都是與非門，分別用N1，N2，N3，N4，N5，N6來(lái)標(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)地，我們還需要對(duì)系統(tǒng)的觀測(cè)給出CNF形式的描述.例如，當(dāng)邏輯電路ISCAS-85_c17當(dāng)前得到的觀測(cè)值為：輸入觀測(cè)點(diǎn)“7”，“8”，“9”，“10”，“11”的觀測(cè)分別為高電平，低電平，低電平，高電平，高電平；輸出觀測(cè)點(diǎn)“12”，“13”的觀測(cè)值為高電平，低電平.則我們得到系統(tǒng)觀測(cè)的CNF子句描述如下：

7 0

-8 0

-9 0

10 0

11 0

12 0

-13 0

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

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

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

2.1 ISDAG算法

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

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

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

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

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

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

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

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

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

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

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

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

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

針對(duì)ISDAG算法中的Step2，Step3我們舉例說(shuō)明，假設(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)的觀測(cè)都追加到系統(tǒng)描述文件中，然后在考慮組件集合Sub中的每一個(gè)組件都反常的情況下(相當(dāng)于指定Sub組件集合中的組件為診斷解，即加入單元子句，將其置為正文字)，也就相當(dāng)于將組件集合Sub中的每一個(gè)組件所對(duì)應(yīng)的子句置為恒真子句，接著看剩余的組件集合(COMPS-Sub)都正常的情況下，是否能正常解釋系統(tǒng)在當(dāng)前觀測(cè)下面的行為(相應(yīng)的這3步對(duì)應(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è)解，如果想要得到所有的診斷解，那么需要枚舉出所有的組件集合，然后對(duì)這些集合進(jìn)行判斷，進(jìn)一步得到所有解.

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

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

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

根據(jù)圖3的樹模型，在求解系統(tǒng)的所有診斷的過(guò)程中，我們用這棵樹對(duì)求解過(guò)程進(jìn)行模擬.利用集合枚舉樹模型我們要求解所有的診斷解，只需要遍歷這棵樹上的所有結(jié)點(diǎn)，對(duì)每個(gè)結(jié)點(diǎn)進(jìn)行相應(yīng)地判斷就可以得到最后的解.例如，針對(duì)集合{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

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

趙相福等人[11-12]提出了CSSE-tree方法，CSSE-tree也是基于這樣的一棵枚舉樹，對(duì)整個(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ò)修剪規(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ù)對(duì)實(shí)際例子的分析，我們知道枚舉樹中不是解的結(jié)點(diǎn)占據(jù)了枚舉樹中大量的結(jié)點(diǎn).CSSE-tree中的修剪規(guī)則只是對(duì)是解的那些結(jié)點(diǎn)起作用，對(duì)于不是解的那些結(jié)點(diǎn)，只能進(jìn)行逐個(gè)判斷求解.

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

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

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

3.1 有解剪枝和無(wú)解剪枝

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

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

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

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

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

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

為了解釋上面的定義，我們舉例說(shuō)明，如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).對(duì)這棵樹進(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).

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

針對(duì)上面的這棵枚舉樹，樹中一共有第1層的{N1}，{N2}，{N3}，{N4}這4個(gè)結(jié)點(diǎn)以及它們的子樹構(gòu)成了這棵樹.對(duì)這4個(gè)結(jié)點(diǎn)處理的方式是一樣的，只對(duì)結(jié)點(diǎn){N1}進(jìn)行舉例說(shuō)明.針對(duì)結(jié)點(diǎn){N1}及其子孫結(jié)點(diǎn)，我們首先判斷最后一層結(jié)點(diǎn){N1,N2,N3}的可滿足性，如果該結(jié)點(diǎn)是可滿足的，那么向上回溯，判斷{N1,N2}結(jié)點(diǎn).否則，根據(jù)無(wú)解剪枝的定義，可以剪掉結(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ǔ)極小解的過(guò)程中，我們將可滿足的解存起來(lái)，但是如果新來(lái)一個(gè)解，我們會(huì)判斷是否是已經(jīng)存在解的子集，如果是，那么將會(huì)更新原來(lái)的解，否則將新解加入到解集中.

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

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

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

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

算法2. LLBRS-tree算法.

輸入:系統(tǒng)描述的CNF文件DigSysDis.cnf、系統(tǒng)觀測(cè)的CNF文件DigSysObs.cnf、極小診斷的最大診斷長(zhǎng)度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ù)輸入的最小診斷長(zhǎng)度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)及其子樹還沒(méi)判斷).

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

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

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

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

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

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

else

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

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

end if

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

Step5. 返回集合DigRes.

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

2) 通過(guò)對(duì)第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求解器對(duì)該文件進(jìn)行可滿足性判斷的時(shí)間也將會(huì)相應(yīng)地縮短.在LLBRS-tree算法中，我們先對(duì)長(zhǎng)度長(zhǎng)的結(jié)點(diǎn)進(jìn)行判斷，這些結(jié)點(diǎn)的長(zhǎng)度與極小診斷解的最大長(zhǎng)度相等，那么相應(yīng)地在調(diào)用ISDAG算法時(shí)，使得在調(diào)用SAT求解器對(duì)DigSysDis.cnf文件處理的時(shí)間縮短.同時(shí)，先對(duì)長(zhǎng)度最長(zhǎng)的結(jié)點(diǎn)進(jìn)行處理，那么我們可以進(jìn)行無(wú)解剪枝的過(guò)程，這樣在反向搜索向上判斷時(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ì)被有解剪枝和無(wú)解剪枝剪掉，從而調(diào)用SAT的次數(shù)也是大大地減少.當(dāng)我們?cè)谔幚斫M件個(gè)數(shù)不是很多，且求解的是單雙診斷時(shí)，效率可能不是很明顯.但是當(dāng)組件個(gè)數(shù)很多時(shí)，無(wú)解剪枝將會(huì)剪掉大量的結(jié)點(diǎn)，求解的時(shí)間將會(huì)得到大大地縮短.

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

本節(jié)我們對(duì)趙相福等人提出的CSSE-trees算法和本文提出的LLBRS-tree算法進(jìn)行了實(shí)現(xiàn)，同時(shí)將2個(gè)算法進(jìn)行多方面地比較.測(cè)試環(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ò)的成績(jī)，而且該求解器的接口寫得很詳細(xì)，在使用接口時(shí)很方便，所以我們選擇了該求解器.

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

Table 1 Solution Time

×：Timeout.

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

由于單診斷并沒(méi)有涉及到有解剪枝和無(wú)解剪枝的情況，所以我們?cè)诒?中只給出了2診斷和3診斷的結(jié)點(diǎn)剪枝情況，“×”表示在1 h內(nèi)求解失敗.而且針對(duì)c1908，c2670，c3540這3個(gè)電路，我們?cè)O(shè)置的求解時(shí)間限制是10 000 s，但是由于這3個(gè)電路的組件個(gè)數(shù)過(guò)多，所以2個(gè)算法都超出了時(shí)間的限制.根據(jù)表2中的雙診斷剪枝結(jié)點(diǎn)的信息，由Δ這一列的差值信息Δ=(LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)-CSSE-tree剪掉的結(jié)點(diǎn)數(shù))可以看出，由于存在無(wú)解剪枝的情況，而且伴隨著有解剪枝，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)出來(lái).從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)椋S著枚舉樹的層數(shù)增加，樹中不可滿足的結(jié)點(diǎn)數(shù)目也大大地增加了，那么算法LLBRS-tree的無(wú)解剪枝策略將會(huì)發(fā)揮關(guān)鍵的作用，所以剪掉的結(jié)點(diǎn)數(shù)目遠(yuǎn)遠(yuǎn)大于算法CSSE-tree.基于這樣的原因，算法LLBRS-tree在求解的過(guò)程中所消耗的時(shí)間才會(huì)小于CSSE-tree算法.而且，隨著枚舉樹的層數(shù)增加，也就是當(dāng)極小診斷解的最大長(zhǎng)度增加時(shí)，樹中不是解的結(jié)點(diǎn)數(shù)目還會(huì)不斷地增加，遠(yuǎn)遠(yuǎn)大于是解的結(jié)點(diǎn)數(shù)目，那么算法LLBRS-tree的無(wú)解剪枝剪掉的結(jié)點(diǎn)也將會(huì)大幅度地增加，該算法的效率也會(huì)彰顯出來(lái)，而CSSE-tree算法的效率將會(huì)變得越來(lái)越慢，更有可能內(nèi)存溢出的情況.我們分別用2種算法針對(duì)組件個(gè)數(shù)適中的幾個(gè)測(cè)試用例求解多診斷得到的結(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.測(cè)試用例為c432并且診斷長(zhǎng)度為4時(shí)，算法CSSE-tree求解時(shí)間是算法LLBRS-tree的2.6倍；但是當(dāng)求解5診斷時(shí)，卻是3.3倍；并且當(dāng)診斷長(zhǎng)度為6時(shí)，CSSE-tree算法出現(xiàn)了內(nèi)存溢出的情況，而算法LLBRS-tree仍然能求解.當(dāng)測(cè)試用例為c499和c880時(shí)，伴隨著組件個(gè)數(shù)和診斷長(zhǎng)度的增加，算法CSSE-tree更早的出現(xiàn)了內(nèi)存溢出的情況，而算法LLBRS依舊能正常的工作.這是因?yàn)樗惴↙LBRS-tree針對(duì)無(wú)解剪枝空間進(jìn)行大量剪枝，加上有解空間的剪枝，使得需要判斷的結(jié)點(diǎn)很少.而算法LLBRS生成大量的結(jié)點(diǎn)進(jìn)行判斷，導(dǎo)致了內(nèi)存溢出.重要的是，根據(jù)LLBRS-tree算法的求解時(shí)間我們可以發(fā)現(xiàn)，即使診斷長(zhǎng)度增加，該算法的求解時(shí)間也是平緩的增加，不會(huì)出現(xiàn)劇烈的抖動(dòng).這是由于有解無(wú)解剪枝策略在求解過(guò)程中起到重要的作用.為了更加清晰地說(shuō)明這種情況，我們對(duì)測(cè)試用例c432求多診斷得到結(jié)果如圖5所示：

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

圖5是算法LLBRS-tree和算法CSSE-tree針對(duì)電路c432(160個(gè)組件)求解診斷1～10的時(shí)間對(duì)比圖.從圖5我們可以看出，在求解3診斷以前，2個(gè)算法的時(shí)間相差幾乎沒(méi)有太大的差距.但是在求解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)行無(wú)解剪枝，剪掉大量不是解的結(jié)點(diǎn)，所以針對(duì)多診斷，依舊能正常地運(yùn)行.

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

5 結(jié)束語(yǔ)

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

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

在后續(xù)的工作中，我們考慮利用增量SAT求解器來(lái)求解基于模型的診斷，只需要一次調(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) (張立明, 歐陽(yáng)丹彤, 曾海林. 基于動(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) (王藝源, 歐陽(yáng)丹彤, 張立明，等. 利用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) (劉娟, 歐陽(yáng)丹彤, 王藝源, 等. 結(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) (趙相福, 歐陽(yáng)丹彤. 使用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]. 中國(guó): 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) (歐陽(yáng)丹彤, 張立明, 趙劍. 利用標(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)(欒尚敏, 戴國(guó)忠. 利用結(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

國(guó)家自然科學(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