結合故障邏輯關系的極小沖突集求解方法

歐陽丹彤 高 菡 徐旖旎 張立明

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

極小沖突集問題是基于模型診斷(model-based diagnosis, MBD)[1]中的重要組成部分,基于模型診斷一直是人工智能領域中一個熱門的研究問題.Reiter[2]于1987年首次提出了模型診斷方法,首先生成所有極小沖突識別,然后生成候選極小碰集,最終得到所有診斷解;Genesereth[3]提出DART(device-independent diagnostic program)方法來進行沖突識別,并使用獨立于設備的語言來描述設備;2002年Haenni[4]提出使用歸結的方法生成沖突集,用于在基于邏輯的論證或誘導推理的背景下計算論證或解釋;欒尚敏等人[5]提出極小沖突集問題可以根據系統結構特征進行求解，進而由極小沖突求得診斷解;方敏[6]結合工業控制系統，提出先離線識別極小沖突候選，后根據測量和約束，在線確定極小沖突的方法;張立明等人[7]利用ATMS(assumption-based truth maintenance system)將所有極小沖突集導出,并將其分為2類極小沖突.經過對沖突集問題的深入研究,國內外學者發現通過集合枚舉樹(set enumeration tree, SE-Tree)求解極小沖突集是一種很高效的方法,將元件集合映射為樹節點，進而遍歷整棵枚舉樹進行沖突判別;Hou[8]在1994年提出的CS-Tree(conflict set tree)，是最早利用枚舉樹求解極小沖突集的方法，,但其剪枝策略不能保證算法的完備性.

隨著SAT(propositional satisfiability problem)求解器應用研究的擴展,部分學者發現可以把求解沖突集問題轉化為命題可滿足問題.沖突元件集從命題可滿足問題角度可以解釋為：在該集合內所有元件均假設為正常行為的模式下，不能找到一組賦值使得系統是一致可滿足的.于是可以調用SAT求解器判斷該集合中元件均正常的邏輯表示公式是否與系統是可滿足的.首次使用SAT求解器求解沖突集問題的是趙相福等人提出的HSSE-Tree(hitting set on set enumeration tree)[10],CSSE-Tree(conflict set on set enumeration tree)[10],CSISE-Tree(conflict set on inverse set enumeration tree)[11]方法;陳榮等人[12]在求解診斷問題時,先調用SAT求解器識別沖突后，由所有沖突集的極小碰集得到診斷解;劉伯文等人[13]提出反向深度遍歷SE-Tree,并用SAT求解器判別沖突集的方法CSRDSE;徐旖旎等人[14]在對比正常輸出與實際輸出情況后，結合故障輸出特征提出MCS -SFFO(minimal conflict set-structural feature of fault output)方法,將故障無關元件集及其子集剪枝,求解效率提高.

本文在對MCS -SFFO方法分析的基礎上,提出結合故障邏輯關系的有解剪枝以及無解剪枝方法MCS -FLR(fault logic relationship).提出單元件非沖突集定理以及非極小沖突定理：單元件集合都是非沖突的、故障輸出相關元件集的真超集都是沖突集,且都不是極小沖突集.因此,對故障輸出相關元件集的嚴格超集都不需要進行沖突判定,可以直接將其加入沖突集集合中.MCS -FLR方法在MCS -SFFO方法的基礎上進一步對SE-Tree進行單元件無解空間以及故障輸出相關元件真超集有解空間的剪枝,提高了沖突集求解效率、節省求解時間.

1 預備知識

本節首先介紹診斷的相關定義,然后介紹命題可滿足問題的基本概念,并將診斷相關問題轉化為命題可滿足問題.

定義1.診斷系統[15].一個系統可以形式地定義為一個三元組(SD,COMPS,OBS),其中：SD(system description)代表系統描述,是一階謂詞公式的集合;COMPS(system components)代表系統中元件的集合,是一個有限常量集合;而OBS(system observation)代表一觀測集合,是一階謂詞公式構成的有限集合.在下面我們使用一元謂詞AB(·)表示“Abnormal”,AB(c)為真當且僅當c反常,其中c∈COMPS.

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

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

一個元件集如果是極小沖突集,則其任意真子集都不是沖突集[10].

推論1.當元件集C是沖突集時,C除自身以外的任意超集都不是極小的沖突集[10].

推論2.當元件集C不是沖突集時,C的任意真子集與C具有同樣的沖突性質，也都不是沖突集[13].

SE-Tree是求解極小沖突集的基本邏輯存儲結構.利用SE-Tree求解極小沖突集的問題與元件個數呈指數級相關,所以對樹中每一個節點都調用SAT求解器判別沖突顯然是效率低下的,為了縮減搜索空間進一步減少求解次數,結合上述沖突集的概念以及推論可知,對沖突集的所有真超集以及非沖突集的所有真子集，可不必再對其進行沖突判定.

在命題可滿足問題中,用xi(i=1,2,…,n)表示布爾變量.xi及xi稱作稱作變量xi的正文字及負文字.X={x1,x2,…,xn}表示變量的集合.Ci(i=1,2,…,m)表示子句,每一個子句是由一組文字組成的析取式.Φ代表CNF公式,CNF公式是由子句Ci的合取構成,即合取范式CNF:Φ=C1∧C2∧…∧Cr,而命題可滿足問題就是尋找是否存在一組X的賦值,使其滿足CNF.命題可滿足問題又稱作SAT問題,即判斷一個命題公式Φ是不是可以被滿足的.

定義4.命題可滿足問題(propositional satis-fiability problem, SAT)[15].針對給定的一個命題公式Φ,X={x1,x2,…,xm}是該公式的變量集合,SAT問題可以描述為是否存在1組X的賦值使得給定的命題公式Φ的取值為真.如果能找到至少一組這樣的賦值,那么我們則稱命題公式Φ是可滿足的,若不存在這樣的賦值，則該命題公式是不可滿足的.

那么,要判斷一個元件集合S是否是某系統的一個沖突集,只需要假設S中的元件都為正常行為模式,將S中每一個元件正常狀態的行為描述、與該元件相關的系統描述以及觀測描述一起編寫成一個CNF文件,之后調用SAT求解器對當前CNF文件進行沖突判定.如果SAT求解器得到不可滿足,那么S是系統的一個沖突解，反之S為非沖突解.

2 MCS -SFFO方法

本節主要介紹當前求解極小沖突集問題效率較高的MCS -SFFO方法,并給出算法的一些相關概念與基本實現思想.

定義5.集合枚舉樹[16].S為一個集合,將S中各個元素不重復的所有組合映射為樹中的節點，并以樹的形式按一定順序枚舉排列出來,稱這樣的樹為集合枚舉樹.

定義6.故障輸出元件[14].對于一個電路的診斷系統{SD,COMPS,OBS},若存在元件c∈COMPS,c沒有后繼元件，且c的輸出是系統的輸出且是故障輸出,即該輸出與系統不一致,c為該系統的故障輸出元件.

定義7.故障輸出相關元件集[14].稱Rel為系統的一個故障輸出相關元件集,當且僅當Rel中每一個元件的輸出都會傳播到故障輸出(包含故障輸出元件c).

定義8.故障輸出無關元件集[14].Rel為系統的一個故障輸出相關元件集,稱集合COMPS-Rel為系統的故障輸出無關元件集.

MCS -SFFO方法提出與診斷系統故障輸出無關的元件集合的所有子集都不是沖突集,所以對SE-Tree中與故障輸出無關的電路元件的所有組合進行剪枝,縮小了SAT求解問題的規模.下面給出一些求解極小沖突集的相關概念及SE-Tree遍歷節點的剪枝規則.

設Node為SE-Tree中當前正在遍歷的節點,以下為剪枝規則及標識規則.

剪枝規則1[13].若Node是沖突集且Node是其父節點的最左孩子節點,則向上回溯判斷其父節點;否則,跳轉判斷Node的下一個兄弟節點的最左孩子節點;若Node沒有下一個兄弟節點,則跳轉判斷下一個葉節點.

剪枝規則2[14].若Node不是沖突集,且Node是由其子孫節點回溯的節點,(此時Node的最左孩子節點為極小沖突集)則跳轉判斷Node的左側下一個孩子節點的最左孩子節點;否則,跳轉判斷Node的下一個兄弟節點;若Node沒有下一個兄弟節點則跳轉至以同層非同根節點的最左孩子節點.

剪枝規則3[13].在對Node判斷其是否沖突之前,先判斷Node是否為非沖突集合簇中集合的子集.若是,則其一定是非沖突的，直接調用剪枝規則2跳轉判斷即可;否則,對Node調用SAT求解器.

標示規則[13].當Node是沖突集時,將Node加入到沖突集合簇中,將其標示“0”,并將沖突集合簇中Node的超集標示“1”.

下面給出MCS -SFFO方法的偽代碼.

算法1.MCS -SFFO.

輸入：SD.cnf、OBS.cnf、故障輸出相關元件集onABCompS、故障輸出無關元件集unOnABCompS;

輸出：極小沖突集合MCSRes.

① 初始化SE-Tree,CSRes=?,UCSRes=?,Node=?;

②Node=SE-Tree的最左節點;

③ While (Node≠?)

④ If (Node?unOnABCompS)

⑤ Break;

⑥ Else

⑦ If (Node是UCSRes元素的子集)

⑧ 剪枝規則3;

⑨ Else

⑩ If (Node是沖突集)

3 MCS -FLR方法

MCS -SFFO方法通過對故障輸出無關元件組合的所有子集進行剪枝減少了調用SAT求解器次數,使問題規模變小.結合實際問題進一步分析,與故障輸出端相關的電路元件集的超集都是沖突集,不必對其進行可滿足性判斷,且故障輸出相關元件真超集一定不是極小沖突集，故可以將故障輸出相關元件真超集剪枝，進一步減少SAT求解器調用次數.因此,提出結合故障邏輯關系的MCS -FLR方法對MCS -SFFO方法改進.

定理1.單元件非沖突集定理：在多元件電路中,任何單元件集合都不是沖突集.

證明.ci為診斷多元件電路中的任一單元件,ci∈COMPS.首先,根據沖突集的定義,判斷ci是否為沖突集,即判斷系統中SD∪OBS∪{AB(ci)}是否一致.然后將ci在系統中的觀測描述、ci元件正常行為的子句描述構成CNF文件,最后調用SAT求解器進行求解.已知在保證ci為正常行為的情況下,多元件電路中其他元件可以是故障模式,即存在一組賦值使CNF公式取值為真,SAT返回可滿足,進而可知SD∪OBS∪{AB(ci)}是一致的,元件集非沖突.得證單元件集合都不是沖突集.

證畢.

定理2.非極小沖突集定理：系統的故障輸出相關元件集的任意超集(包含自身)都是沖突集.

證明. 反證法.Rel為系統的一個故障相關元件集,ARel是Rel的任意一個嚴格超集.假設ARel不是沖突集,則根據推論2可以得出Rel也不是沖突集.已知Rel是故障相關的,即Rel是在所有元件正常情況下,與系統觀測及系統描述的輸出不一致的元件集合.由沖突集定義可知,Rel一定是沖突集.由此推出矛盾,假設不成立.得出ARel為沖突集,即故障相關元件集Rel的任意超集(包括自身)都是沖突集.進而可推出,Rel的任意真超集都不是極小沖突集.

證畢.

求解故障輸出無關元件集方法是通過給定的CNF文件,先調用SAT求解器求得預計的正常輸出,然后根據輸入將實際輸出與正常輸出中的元素一一比較,與正常輸出不一致的輸出即為故障輸出端,進而可以從故障輸出的輸入推出與之相聯系的元件集合.

Fig. 1 C17 circuit圖1 C17電路

例1.在圖1所示的C17電路中,輸出端口12異常,端口13正常,如圖1所示,與13端相聯系的元件集合為{c2,c3,c5,c6},因為它們的輸出都會傳播到13端.其中c2,c3的輸出既傳播到12端又傳播到13端,故無法確定是否為故障輸出無關,而c5與c6元件的輸出僅傳播到13端,則可以明確判斷{c5,c6}為故障輸出無關元件集.故根據定義9可知{c1,c2,c3,c4}為故障輸出相關集合.由此我們可以得到,{c5,c6}是非沖突的,且它的任意子集都是非沖突集,{c1,c2,c3,c4}是沖突的,根據定理2可知,它的任意超集也是沖突集.對于已經明確該集合是否沖突時,不必再調用SAT求解器對其求解.

在同一實例上分別執行MCS -SFFO方法及MCS -FLR方法,將通過這2種方法剪枝后的待遍歷節點數進行對比來說明MCS -FLR方法求解效率的提高.已知在當前系統中,有元件集{c1,c2,c3,c4,c5},根據故障輸出可以得到,其中{c2,c4}為故障輸出相關元件集,{c1,c3,c5}為故障輸出無關元件集.

圖2為完整的SE-Tree,非空節點31個.圖3為MCS -SFFO方法將故障輸出無關集合{c1,c3,c5}及其子集剪枝后的枚舉樹,非空節點23個.圖4為MCS -FLR方法在MCS -SFFO方法基礎上將單元件集合{c2}及{c4}、故障輸出相關集合{c2,c4}真超集剪枝后的枚舉樹,非空節點15個.圖2及圖3是未執行剪枝規則前初始化的枚舉樹.由此可以看出,MCS -FLR方法在MCS -SFFO方法的基礎上減少了近12的待遍歷節點,進而減少大量求解次數,使得求解效率更高.下面給出MCS -FLR方法的偽代碼.

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

Fig. 3 SE-Tree after pruning by MCS -SFFO method圖3 MCS -SFFO方法剪枝后的SE-Tree

Fig. 4 SE-Tree after pruning by MCS -FLR method圖4 MCS -FLR方法剪枝后的SE-Tree

算法2.MCS -FLR.

輸入：系統觀測文件circuit.cnf、故障相關元件集合Rel、故障輸出無關元件集合UnRel;

輸出：極小沖突集合MCSes.

① 初始化沖突集CS=?,非沖突集UCS=?,當前遍歷節點Node=?;

② 生成集合{Rel[0],…,Rel[N1-1],UnRel[0],…,UnRel[N2-1]}的集合枚舉樹CSTree.其中,NUM1是故障輸出相關的元素個數,NUM2是故障輸出無關的元素個數;

③Node賦值為CSTree的最左節點;

④ While (Node≠?)

⑤ If (Node是故障輸出無關集合的子集‖Node為單元件集合)

⑥ 將Node及其子集加入到UCS中；

⑦ Break;

⑧ EndIf

⑨ If (Node是故障輸出相關集合的超集)

⑩ 將Node及其超集加入到CS中;

算法2是以輸入的circuit.cnf,Rel,UnRel構造集合枚舉樹,并用CS存放沖突集,UCS存放非沖突集(行①),Node為當前遍歷的枚舉樹中的最左節點(行③).當枚舉樹中仍有節點沒有被遍歷時,對當前Node節點進行判斷,分為4種情況：1)若為故障輸出無關元件集子集或單元件集合,則其可滿足性已知，不必再判斷(行⑤～⑧);2)若為故障輸出相關集合的超集,則直接將其加入沖突集合CS,調用剪枝規則1(行⑨～);3)若為非沖突集的子集,則不進行判斷,直接將其加入UCS,按照剪枝規則3對其賦值(行);4)若以上3種情況都不滿足，則利用SAT求解器判斷,若其是沖突集,按照剪枝規則1對其賦值(行～),否則若其是非沖突集,按照剪枝規則2對其賦值(行～).SE-Tree遍歷完成后,將CS中所有標示為“0”的節點加入MCSes,得到所有極小沖突集(行～).

根據算法2的描述可知,MCS -FLR方法為完備算法,除了被剪枝掉的節點,其余節點均被遍歷到,且在整棵SE-Tree遍歷完成之后會得到所有的極小沖突集.

MCS -FLR方法與MCS -SFFO算法的主要區別在于MCS -SFFO方法是結合故障輸出無關集合特征的無解剪枝,MCS -FLR方法是在MCS -SFFO方法的基礎上,又結合故障輸出相關集合邏輯關系新增有解及無解剪枝.MCS -FLR方法提出了非極小沖突集定理以及單元件非沖突定理,將大量單元件集合和故障輸出相關元件真超集剪枝,不必對故障輸出相關元件的真超集及單元件集合調用SAT求解器,使得調用SAT求解器次數大大減少,求解效率明顯提高.

4 實驗結果

本節將對MCS -FLR方法與MCS -SFFO方法進行比較,并給出2種方法在同樣測試用例下的實驗結果.實驗平臺為64 b Ubantu 16.04.3 LTS系統,Intel?CoreTMi5-3337U CPU@1.80 GHz×4.MCS -FLR方法與MCS -SFFO方法同時調用的求解器均為Picosat[17].

本次測試的用例[10-11]包括c17,FullAdd_1,FullAdd_2,Polybox_5,Polybox_9,FullAdd_3,FullAdd_4,FullAdd_8.實驗對每一個電路設置多觀測進行測試,同時每組測試都存在沖突.在使用MCS -FLR方法及MCS -SFFO方法求解時,首先根據CNF文件獲取系統描述和系統觀測,求出故障輸出相關元件集Rel與故障輸出無關元件集UnRel,然后將其作為輸入構造SE-Tree,作為實現MCS -FLR方法以及MCS -SFFO方法求解極小沖突集的預處理.

表1中列1為實例名稱,列2,3分別是MCS -SFFO方法與MCS -FLR方法在求解用例時平均調用SAT求解器的次數(多個不同故障電路測試用例調用求解器的總次數故障電路個數),其中每個輸出端口都會被設定為故障輸出,分別求得一個故障電路.列4是MCS -SFFO方法與MCS -FLR方法調用求解器次數之差,差值越大說明節省的求解器調用次數越多,效率提高越多.列5是MCS -FLR方法較MCS -SFFO方法減少的求解次數百分比,即Difference Ratio=(列2-列3)列2×100%.以C17電路為例說明,MCS -FLR方法節省了MCS -SFFO方法22.884 4%的求解器次數.可以看出,在所有測試用例中MCS -FLR方法都較MCS -SFFO方法有提高,求解器次數有或多或少的減少,甚至在實驗效果較好的用例中(如FullAdd_1,Polybox_5)中,MCS -FLR方法節省了MCS -SFFO方法13的求解器調用次數,求解效率大大提高.不同的電路結構以及同一電路中設置故障輸出端口的不同都是影響MCS -FLR方法優化程度的因素.例如在FullAdd_5電路中,故障輸出端口的相關元件個數較多,可剪枝的故障輸出相關元件真超集的個數較少,故效率提高不明顯.在FullAdd_1電路中,由于故障輸出端口的相關元件個數較少,所以剪枝掉的故障輸出相關元件真超集的個數較多,求解效率提高明顯.

Table 1 Average Number of Calls to SAT Solver and its Difference Ratio 表1 平均調用SAT求解器次數及其加速比

表2是MCS -SFFO方法與MCS -FLR方法求解極小沖突集的時間對比結果.列1為實例名稱；列2為測試的組數,即賦值的次數,例如對于C17電路來說,共有5個輸入端口,則有25,共計32組賦值.為了保證測試的時限,將測試次數作為輸入參數來控制算法的執行,例如FullAdd_5電路中,輸入端口共有10個,即應有210,共計1 024組賦值,程序運行時間過長,可以截取一部分結果作為比較的衡量,故設置測試次數為50;列3,4分別為MCS -SFFO方法及MCS -FLR方法的求解時間,本文所有數據均保留4位小數；列5為MCS -SFFO方法與MCS -FLR方法的加速比,是列3求解時間與列4求解時間的比值.加速比越大說明時間效率提高越多;列6為差值加速比,即使用MCS -FLR方法減少了MCS -SFFO方法的時間占MCS -SFFO方法總時間的比,例如在FullAdd_2用例中,MCS -FLR方法減少了MCS -SFFO方法41.666 7%的時間使用.顯然,節省求解器次數越多的用例兩項加速比也越高,MCS -FLR方法求解極小沖突集的效率也越高.但也存在特殊情況,比如在Polybox_9用例中,節省的求解器次數百分比為9.881 8%,但節省時間百分比卻高達54.545 5%,這是因為SAT求解器對元素個數較多的子集判斷其是否滿足時會更加耗時.

Table 2 Running Time and its Difference Ratio表2 求解時間及其差值加速比

5 結束語

極小沖突集問題是模型診斷問題中的重要分支.MCS -SFFO方法是目前求解極小沖突集效率較好的方法.本文在深入研究分析MCS -SFFO方法無解剪枝方法的基礎上,結合故障的邏輯關系，在SE-Tree上做進一步的無解空間以及大量有解空間的剪枝.提出針對單元件進行無解剪枝以及對故障輸出相關元件集的真超集進行有解剪枝的MCS -FLR方法.該方法首先提出了單元件非沖突集定理,推證出單元件構成的集合節點一定是非沖突的,故不進行可滿足性判斷.之后,提出非極小沖突定理，即系統故障輸出相關元件集的超集都是沖突集,且其真超集都非極小沖突，根據此定理將故障輸出相關元件集的真超集剪枝,直接加入沖突集中,減少大量求解器調用次數,降低了算法的時間消耗.實驗結果表明:在故障輸出相關元件占元件總數較大時,剪枝次數較少,效果一般,但調用SAT求解器次數已明顯減少.若故障輸出相關元件占元件總數比例較小時,其超集個數較多,有解空間剪枝次數較多,求解器效率對比與MCS -SFFO方法提升近13,算法效率提高明顯.并且,在大規模電路中,有解剪枝的節點個數大幅增加,MCS -FLR方法有更好的剪枝效果.