結(jié)合故障邏輯關(guān)系的極小沖突集求解方法

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

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

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

隨著SAT(propositional satisfiability problem)求解器應(yīng)用研究的擴(kuò)展,部分學(xué)者發(fā)現(xiàn)可以把求解沖突集問題轉(zhuǎn)化為命題可滿足問題.沖突元件集從命題可滿足問題角度可以解釋為：在該集合內(nèi)所有元件均假設(shè)為正常行為的模式下，不能找到一組賦值使得系統(tǒng)是一致可滿足的.于是可以調(diào)用SAT求解器判斷該集合中元件均正常的邏輯表示公式是否與系統(tǒng)是可滿足的.首次使用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]在求解診斷問題時(shí),先調(diào)用SAT求解器識(shí)別沖突后，由所有沖突集的極小碰集得到診斷解;劉伯文等人[13]提出反向深度遍歷SE-Tree,并用SAT求解器判別沖突集的方法CSRDSE;徐旖旎等人[14]在對(duì)比正常輸出與實(shí)際輸出情況后，結(jié)合故障輸出特征提出MCS -SFFO(minimal conflict set-structural feature of fault output)方法,將故障無關(guān)元件集及其子集剪枝,求解效率提高.

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

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

本節(jié)首先介紹診斷的相關(guān)定義,然后介紹命題可滿足問題的基本概念,并將診斷相關(guān)問題轉(zhuǎn)化為命題可滿足問題.

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

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

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

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

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

推論2.當(dāng)元件集C不是沖突集時(shí),C的任意真子集與C具有同樣的沖突性質(zhì)，也都不是沖突集[13].

SE-Tree是求解極小沖突集的基本邏輯存儲(chǔ)結(jié)構(gòu).利用SE-Tree求解極小沖突集的問題與元件個(gè)數(shù)呈指數(shù)級(jí)相關(guān),所以對(duì)樹中每一個(gè)節(jié)點(diǎn)都調(diào)用SAT求解器判別沖突顯然是效率低下的,為了縮減搜索空間進(jìn)一步減少求解次數(shù),結(jié)合上述沖突集的概念以及推論可知,對(duì)沖突集的所有真超集以及非沖突集的所有真子集，可不必再對(duì)其進(jìn)行沖突判定.

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

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

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

2 MCS -SFFO方法

本節(jié)主要介紹當(dāng)前求解極小沖突集問題效率較高的MCS -SFFO方法,并給出算法的一些相關(guān)概念與基本實(shí)現(xiàn)思想.

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

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

定義7.故障輸出相關(guān)元件集[14].稱Rel為系統(tǒng)的一個(gè)故障輸出相關(guān)元件集,當(dāng)且僅當(dāng)Rel中每一個(gè)元件的輸出都會(huì)傳播到故障輸出(包含故障輸出元件c).

定義8.故障輸出無關(guān)元件集[14].Rel為系統(tǒng)的一個(gè)故障輸出相關(guān)元件集,稱集合COMPS-Rel為系統(tǒng)的故障輸出無關(guān)元件集.

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

設(shè)Node為SE-Tree中當(dāng)前正在遍歷的節(jié)點(diǎn),以下為剪枝規(guī)則及標(biāo)識(shí)規(guī)則.

剪枝規(guī)則1[13].若Node是沖突集且Node是其父節(jié)點(diǎn)的最左孩子節(jié)點(diǎn),則向上回溯判斷其父節(jié)點(diǎn);否則,跳轉(zhuǎn)判斷Node的下一個(gè)兄弟節(jié)點(diǎn)的最左孩子節(jié)點(diǎn);若Node沒有下一個(gè)兄弟節(jié)點(diǎn),則跳轉(zhuǎn)判斷下一個(gè)葉節(jié)點(diǎn).

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

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

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

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

算法1.MCS -SFFO.

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

輸出：極小沖突集合MCSRes.

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

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

③ While (Node≠?)

④ If (Node?unOnABCompS)

⑤ Break;

⑥ Else

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

⑧ 剪枝規(guī)則3;

⑨ Else

⑩ If (Node是沖突集)

3 MCS -FLR方法

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

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

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

證畢.

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

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

證畢.

求解故障輸出無關(guān)元件集方法是通過給定的CNF文件,先調(diào)用SAT求解器求得預(yù)計(jì)的正常輸出,然后根據(jù)輸入將實(shí)際輸出與正常輸出中的元素一一比較,與正常輸出不一致的輸出即為故障輸出端,進(jìn)而可以從故障輸出的輸入推出與之相聯(lián)系的元件集合.

Fig. 1 C17 circuit圖1 C17電路

例1.在圖1所示的C17電路中,輸出端口12異常,端口13正常,如圖1所示,與13端相聯(lián)系的元件集合為{c2,c3,c5,c6},因?yàn)樗鼈兊妮敵龆紩?huì)傳播到13端.其中c2,c3的輸出既傳播到12端又傳播到13端,故無法確定是否為故障輸出無關(guān),而c5與c6元件的輸出僅傳播到13端,則可以明確判斷{c5,c6}為故障輸出無關(guān)元件集.故根據(jù)定義9可知{c1,c2,c3,c4}為故障輸出相關(guān)集合.由此我們可以得到,{c5,c6}是非沖突的,且它的任意子集都是非沖突集,{c1,c2,c3,c4}是沖突的,根據(jù)定理2可知,它的任意超集也是沖突集.對(duì)于已經(jīng)明確該集合是否沖突時(shí),不必再調(diào)用SAT求解器對(duì)其求解.

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

圖2為完整的SE-Tree,非空節(jié)點(diǎn)31個(gè).圖3為MCS -SFFO方法將故障輸出無關(guān)集合{c1,c3,c5}及其子集剪枝后的枚舉樹,非空節(jié)點(diǎn)23個(gè).圖4為MCS -FLR方法在MCS -SFFO方法基礎(chǔ)上將單元件集合{c2}及{c4}、故障輸出相關(guān)集合{c2,c4}真超集剪枝后的枚舉樹,非空節(jié)點(diǎn)15個(gè).圖2及圖3是未執(zhí)行剪枝規(guī)則前初始化的枚舉樹.由此可以看出,MCS -FLR方法在MCS -SFFO方法的基礎(chǔ)上減少了近12的待遍歷節(jié)點(diǎn),進(jìn)而減少大量求解次數(shù),使得求解效率更高.下面給出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.

輸入：系統(tǒng)觀測文件circuit.cnf、故障相關(guān)元件集合Rel、故障輸出無關(guān)元件集合UnRel;

輸出：極小沖突集合MCSes.

① 初始化沖突集CS=?,非沖突集UCS=?,當(dāng)前遍歷節(jié)點(diǎn)Node=?;

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

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

④ While (Node≠?)

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

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

⑦ Break;

⑧ EndIf

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

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

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

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

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

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

本節(jié)將對(duì)MCS -FLR方法與MCS -SFFO方法進(jìn)行比較,并給出2種方法在同樣測試用例下的實(shí)驗(yàn)結(jié)果.實(shí)驗(yàn)平臺(tái)為64 b Ubantu 16.04.3 LTS系統(tǒng),Intel?CoreTMi5-3337U CPU@1.80 GHz×4.MCS -FLR方法與MCS -SFFO方法同時(shí)調(diào)用的求解器均為Picosat[17].

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

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

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

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

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

5 結(jié)束語

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