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

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

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

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

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

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

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

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

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

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

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

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

1 預備知識

在本節，我們首先介紹基于模型的診斷中的相關概念，而后介紹SAT問題，最后介紹將基于模型的診斷轉換成SAT問題.

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

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

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

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

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

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

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

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

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

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

1.2 SAT問題

首先，我們將要用到的符號定義如下：

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

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

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

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

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

-3 4 0

-4 0

1 0

經過上面的轉化，判定命題公式集合R是否為真時，只需要將公式R轉換成CNF文件描述，接下來調用SAT求解器對轉換后的CNF文件進行求解就可以得到結果.如果CNF文件是可滿足的，那么命題公式R為真，否則公式R為假.

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

1.3 基于模型的診斷轉換成SAT問題

在本節，將介紹如何將診斷系統的模型以及系統的觀測轉換成CNF形式的文件.

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

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

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

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

Fig. 2 C17.cnf圖2 C17.cnf

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

7 0

-8 0

-9 0

10 0

11 0

12 0

-13 0

通過上面這樣的轉換方式，我們就可以將一個診斷系統轉換成相應的CNF文件描述，也就是轉換成SAT問題，然后針對該CNF文件進行相應地處理，調用SAT求解器對其進行求解，最后得到診斷系統的診斷解，具體的算法我們在第2節進行介紹.

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

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

2.1 ISDAG算法

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

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

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

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

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

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

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

輸入：將要判斷系統的一個組件子集Sub;

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

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

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

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

Step4. 調用SAT求解器對系統文件DigSysDis.cnf進行可滿足性判斷，如果得到的結果是可滿足的，那么表明組件集合Sub是診斷解，返回1.如果得到的結果是不可滿足的，那么表明組件集合Sub不是診斷解，返回0.

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

1 0

2 0

3 0

-4 0

-5 0

-6 0

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

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

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

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

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

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

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

近些年以來，大部分求解系統的基于一致性診斷都是根據上面的枚舉樹，按照廣度優先遍歷或者深度優先遍歷，采用一定的剪枝規則，減少遍歷的結點，從而得到最后的診斷解.

趙相福等人[11-12]提出了CSSE-tree方法，CSSE-tree也是基于這樣的一棵枚舉樹，對整個枚舉樹中的結點進行遍歷，然后進行相應的操作得到最后的極小診斷解.CSSE-tree的提出使得求解基于一致性診斷的求解時間得到了提升,它的優點有2點：

1) 根據系統的組件個數，系統地枚舉出跟該組件集合相關冪集的所有元素，然后從根結點開始進行廣度優先遍歷，這樣保證產生的解集是極小診斷解，并且保證了CSSE-tree的完備性，不會丟掉任何一個解.

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

然而CSSE-tree也存在2個缺點：

1) 如果系統的組件個數太多，枚舉出跟組件集合相關冪集合的所有元素將會使得CSSE-tree變得相當得龐大，使得空間復雜度相當得大.而且，如果在解很少的情況下，修剪規則的剪枝空間較少，效率提升較小.

2) 根據對實際例子的分析，我們知道枚舉樹中不是解的結點占據了枚舉樹中大量的結點.CSSE-tree中的修剪規則只是對是解的那些結點起作用，對于不是解的那些結點，只能進行逐個判斷求解.

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

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

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

3.1 有解剪枝和無解剪枝

首先給出在這部分要用到的相關的定義：

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

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

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

定義9. 反向搜索.針對一棵枚舉樹，當枚舉樹的層數已經給定時，稱從枚舉樹的最后一層向枚舉樹的根結點搜索的過程為樹的反向搜索.

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

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

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

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

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

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

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

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

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

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

算法2. LLBRS-tree算法.

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

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

局部變量:診斷解集合DigRes[]、診斷系統組件的個數ComNum、枚舉樹的總層數DigTreeLevel、待判斷的第1層的某個結點及其子樹Sub-tree.

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

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

Step3. 將DigSE-tree的第1層最左邊的結點及其子樹賦值給Sub-tree.

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

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

對該子樹最底層的最左邊的結點調用ISDAG算法判斷;

if (該結點可滿足)

① 將該結點加入到診斷解結合DigRes中，并且將在DigRes中所有該結點的真超集刪除;

② 有解剪枝，將該結點的沒有訪問過的子孫結點剪掉;

③ 對該結點的父結點進行判斷;

else

① 無解剪枝，將該結點的父結點剪掉；

② 對該結點的右邊的結點進行判斷；

end if

Step4.2. 將第1層的下一個結點及其子樹賦值給Sub-tree，接著對Sub-tree進行判斷.

Step5. 返回集合DigRes.

1) 該算法是完備的，會得到所有的極小診斷解，不會出現丟掉一部分解的情況.因為我們用一棵枚舉樹的形式將所有可能出現的情況都一一列舉出來，所以不會出現丟解，所有的極小診斷解在遍歷完這棵樹以后全部產生.

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

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

4 實驗結果

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

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

Table 1 Solution Time

×：Timeout.

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

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

Table 2 Numbers of Cut Node

×: Timeout.

Table 3 Time of Multi-Diagnosis

M.O: Out of memory.

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

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

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

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

5 結束語

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

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

在后續的工作中，我們考慮利用增量SAT求解器來求解基于模型的診斷，只需要一次調用SAT求解器，就可以得到多個解，這樣求解效率會得到進一步提升.

[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)(姜云飛, 林笠. 用布爾代數方法計算最小碰集[J].計算機學報, 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) (張立明, 歐陽丹彤, 曾海林. 基于動態極大度的極小碰集求解方法[J]. 計算機研究與發展, 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]. 計算機研究與發展, 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]. 軟件學報, 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) (劉娟, 歐陽丹彤, 王藝源, 等. 結合特征學習的粒子群求解極小碰集方法[J]. 電子學報, 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 的運算電路查錯方法[J]. 計算機學報, 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) (張學農, 姜云飛, 陳藹祥，等. 基于模型診斷的分步求解[J]. 軟件學報, 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求解器產生所有極小沖突部件集[J]. 電子學報, 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)(陳榮, 高健, 張維石. 基于邏輯相容性的數字電路故障診斷方法及系統[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) (歐陽丹彤, 張立明, 趙劍. 利用標志傳播求解基于模型的故障診斷[J]. 儀器儀表學報, 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)(欒尚敏, 戴國忠. 利用結構信息的故障診斷方法[J]. 計算機學報, 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

國家自然科學基金項目(61672261,61502199,61402196,61272208);浙江省自然科學基金項目(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