基于模型診斷的一種新編碼方法

周慧思 歐陽丹彤 田新亮 張立明

（吉林大學計算機科學與技術(shù)學院 長春 130012）

（吉林大學符號計算與知識工程教育部重點實驗室 長春 130012）（zhouhsi@163.com）

當預(yù)期的系統(tǒng)觀測和真實的系統(tǒng)觀測不一致時，這時系統(tǒng)就存在故障，需要對故障進行診斷.基于模型診斷 (model-based diagnosis， MBD)[1]是根據(jù)系統(tǒng)的描述利用基于推理的方法解釋系統(tǒng)觀測不一致的過程.幾十年來，MBD問題已經(jīng)廣泛應(yīng)用于的各個領(lǐng)域，包括調(diào)試關(guān)系規(guī)范[2]、診斷系統(tǒng)調(diào)試[3]、電子表格調(diào)試[4]和軟件故障定位[5]等領(lǐng)域.

文章的主要貢獻包括3個方面:

1) 提出利用觀測的扇入過濾邊和扇出過濾邊對邊進行過濾的約簡方法.這2種邊都是冗余的，因為它們的值在進行診斷求解過程中是必須進行傳播的值.

2) 提出利用觀測的過濾節(jié)點來進行過濾的約簡方法.對于基于觀察的過濾節(jié)點而言，它所有的扇入和扇出都是固定的，即它的扇入和扇出之間不存在沖突.

3) 在ISCAS85和ITC99基準測試實例上的實驗結(jié)果表明，提出的方法可以有效縮減MBD問題編碼時生成的子句規(guī)模，進而降低最大可滿足性問題(maximum satisfiability， MaxSAT)求解診斷問題的難度，有效地提高了診斷求解效率.

1 相關(guān)工作

近幾十年來，越來越多的研究者投入到MBD問題的研究中，提出了許多求解算法，其中包括單個觀測的MBD算法[6-11]和多觀測的MBD算法[12-15].目前用于解決單個觀測下的MBD問題算法為：隨機搜索算法[6,16]、基于編譯的算法[7]，基于廣度優(yōu)先搜索的算法[8]、基于可滿足性問題 (satisfiability，SAT)的算法[9-10]、基于沖突導向的算法[11]等[17-21].在這些算法中，基于廣度優(yōu)先搜索的算法及其改進算法利用了樹結(jié)構(gòu).此類算法檢查樹的每個節(jié)點是否表示最小診斷解，這類方法是完備的.顯然，只要有足夠的時間，這類方法可以得到所有的診斷解.然而，這類方法是相當耗時的，它們在解決大型現(xiàn)實實例問題時是不太現(xiàn)實的.隨著計算機處理器的快速發(fā)展，一些并行化技術(shù)也被用于MBD求解問題中，Jannach等人[8]通過并行地構(gòu)造碰集樹 (hitting set-tree， HS-Tree)返回所有診斷.基于編譯的方法通過利用給定的系統(tǒng)層次結(jié)構(gòu)和DNF編碼的方式[7]計算候選解的方法也顯示出它們的優(yōu)勢.SAFARI算法[6]證明了在MBD問題上隨機搜索算法的有效性.SAFARI隨機刪除一個組件，然后判斷候選解是否仍然是一個診斷，直到?jīng)]有組件可以刪除.顯然，SAFARI不能保證返回的診斷解是極小勢診斷.近年來，隨著SAT及MaxSAT求解器性能的大幅提升，使得基于SAT的診斷方法引起了廣泛的關(guān)注.Feldman等人[6]提出將診斷的電路編碼成MaxSAT問題，該方法比SAFARI運行時間更長.相比之下，Metodi等人[20]提出的SATbD考慮電路的直接統(tǒng)治者，并找出所有極小勢診斷.2015年，Marques-Silva等人[22]提出一種面向統(tǒng)治者的編碼 (dominator oriented encoding，DOE)方法，通過過濾掉一些節(jié)點和一些邊的方法將MBD編碼為MaxSAT.作為一種先進的編碼方法，DOE利用了系統(tǒng)的結(jié)構(gòu)屬性，有效地縮減了MBD問題編碼后子句集的規(guī)模.雖然DOE保證返回基數(shù)最小的診斷，但它沒有考慮與觀察有關(guān)的多余帶權(quán)重的合取范式 (weighted conjunctive normal form， WCNF).本文提出一種面向觀察的編碼(observation-oriented encoding， OOE)方法，該方法在將MBD編碼到Max-SAT時能有效減少子句集規(guī)模.此外，本文在調(diào)用相同的MaxSAT求解器情況下，將OOE方法與基礎(chǔ)編碼（basic encoding， BE）和 DOE 進行了比較.實驗結(jié)果表明，OOE方法有效提高了MBD問題的求解效率.

2 基于模型的診斷問題

本節(jié)主要介紹MBD問題的相關(guān)定義及概念.

2.1 基本定義

診斷問題可以被定義為一個三元組〈SD,Comps,Obs〉，其中，SD表示診斷問題的系統(tǒng)描述，Comps代表組件的集合，Obs代表一個觀測.假定所有組件的狀態(tài)是正常的情況下，當系統(tǒng)的模型描述和觀測出現(xiàn)不一致時，我們稱存在一個診斷問題.也就是:

其中，AB(c)=1代表組件c是故障的，相反，AB(c)=0代表組件c是正常的.下面我們給出診斷的定義.

定義1.診斷[1].給定一個診斷問題D=〈SD,Comps,Obs〉.一個診斷被定義為一組組件?的集合，其中??Comps，當

其中 ?是一個極小子集診斷當且僅當不存在當前診斷的一個子集 ?′??是一個診斷.診斷解的長度稱為診斷的勢，?是一個極小勢診斷當且僅當不存在另外一個診斷解 ?′滿足∣ ?∣>∣ ?′∣.

2.2 將診斷問題編碼為MaxSAT

許多MBD問題在求解時先被編碼為MaxSAT問題[14-15,22]，下面本文介紹編碼過程.當一個MBD問題被編碼為一系列WCNF子句集時，診斷系統(tǒng)中的組件和電路線分別用變量表示，它們的值用文字表示.下面我們分別表示有2個輸入的與非門(nand2)、與門(and2)、與或門(nor2)、或門(or2)的公式：

例如，對于一個NAND組件c而言，inand_c1和inand_c2分別代表組件c的輸入，onand_c是組件c的輸出.由一組組件組成的系統(tǒng)SD的表示公式為

此處，代表組件c的編碼.在一個觀測中，觀測可以表示為

Obsv.v和一個電路的邏輯值相關(guān)，當v=1代表電路邏輯值為正，當v=0代表電路邏輯值為負.

WCNF中的子句cl的權(quán)重用ω(cl)表示，我們分別設(shè)置SD，Comps，Obs相關(guān)的子句為：

1) 對于SD和Comps中的子句被設(shè)置為硬子句，ω(cl):=num(Obs)+1，其中num(Obs)代表觀測的數(shù)量;

2)Obs中的子句被設(shè)置為軟子句， ω (cl):=1.

在基于SAT的方法中，MBD問題被編碼為一組子句，然后通過迭代調(diào)用SAT或MaxSAT求解器來計算診斷.通過添加阻塞子句可以避免相同的診斷解被多次計算.利用診斷系統(tǒng)的結(jié)構(gòu)屬性是一種可行的方法，這種方法在許多基于SAT的診斷算法中得到了應(yīng)用[23-24].相應(yīng)地，診斷中的統(tǒng)治節(jié)點和頂層診斷(top-level diagnosis，TLD)也是重要的概念.

定義2.統(tǒng)治節(jié)點[20].給定一個組件G1和G2，如果從G1到電路的輸出的所有路徑都包含G2，則稱G2是G1的統(tǒng)治節(jié)點.換句話說，G1是被G2統(tǒng)治的節(jié)點.

定義3.頂層診斷解[20].稱 ?為一個頂層診斷解，如果它是一個極小勢診斷且不包含任何統(tǒng)治組件.

以圖1為例，由于N1到達系統(tǒng)輸出的路徑是唯一的，且包括N5，所以N1被N5統(tǒng)治.假定有觀測i1=i2=i3=i5=o1=o2=1,i4=0,N6是一個 TLD，因為N6不被任何組件統(tǒng)治.通過將統(tǒng)治組件編碼到硬子句中 (即申明這些組件是健康的)，就可以計算TLD.

Fig.1 C17 circuit圖1 C17 電路

3 求解基于模型的診斷問題的DOE方法

為了簡化MBD到MaxSAT的編碼過程，縮減被編碼的“門”生成的子句規(guī)模.DOE方法利用“門控制關(guān)系”，同時計算TLD.除此之外，一些曾在DOE方法中被提出的概念如阻塞連接及骨干組件，將在本節(jié)定義中給出解釋.

定義 4.骨架節(jié)點 (backbone node, B-Node)[22].我們稱一個組件為骨架節(jié)點當且僅當其是一個被統(tǒng)治的組件且它的扇出對于任何一個TLD有固定的值.

考慮圖1中組件N1，N1被N5統(tǒng)治，當給定一個觀測時，N1的所有輸入是固定的，也就是說，i1和i3有固定的值，當求解一個TLD時，N1的扇出就有固定的值，所以N1是一個B-Node.

定義 5.阻 塞 邊 (blocked edge，B-Edge)[22].我 們 稱組件的一個扇入邊E是一個阻塞邊，如果邊的值不會對該組件的扇出起作用.

考慮圖1中的N2，當給定一個觀測Obs={i4=0}，N2的輸出被確定為1，無論i3的值是什么，因此i3邊是一個阻塞邊.

定義6.過濾節(jié)點[22].我們稱組件B為一個過濾節(jié)點，如果它的所有扇出邊都是過濾邊.

定義7.過濾邊[22].我們稱邊E為一個過濾邊，如果它是一個B-Node或者它的扇出組件是一個過濾節(jié)點.

由于N1是一個被統(tǒng)治組件，給定一個觀測Obs={i1=1}，當z1的值 (z1=0) 被傳播后，z3的值將不會對N5的輸出起作用.也就是說，N5的輸出值是固定的.因此， 〈N3，N5〉是一個 B-Edge，因此， 〈N3，N5〉是一個過濾邊.假定 〈N3，N6〉也是一個過濾邊，這時N3的所有輸入邊都是過濾邊，那么組件N3是一個過濾節(jié)點.具體的DOE方法如算法1所示:

算法1.編碼MBD到MaxSAT的DOE方法[22].

輸入：SD，Comps，Obs；

輸出：編譯后的模型.

① repeat

②Dominators所有統(tǒng)治節(jié)點；

③BackboneComps所有骨架組件；

④BlockedConnections所有阻塞連接；

⑤ if 到達最大迭代次數(shù) then

⑥ break；

⑦ end if

⑧ untilNoMoreChanges；

4 OOE方法

文獻[22]中的實驗表明了DOE方法在求解MBD問題上的有效性.在本節(jié)中，我們將介紹OOE方法及該方法中為了改進基于MaxSAT的MBD編譯過程用到的其他過濾節(jié)點和過濾邊的概念.

定義8.基于觀測的扇入過濾邊.我們稱邊E為一個基于觀測的扇入過濾邊，如果它是一個系統(tǒng)的輸入或者它是一個統(tǒng)治組件的一個固定輸出邊.

此處繼續(xù)討論觀測Obs= {i1= 1,i2= 1,i3= 1,i4=1,i5= 1,o1= 1,o2= 1}， 在 第 1 次 迭 代 中 ，i1,i2,i3,i4,i5是基于觀測的扇入過濾邊.在DOE方法過濾了一些節(jié)點和邊之后，因為N1，N4，N3，N2依次成為統(tǒng)治節(jié)點之后， 〈N1，N5〉， 〈N3，N6〉， 〈N2，N4〉， 〈N4，N6〉變 成 了 基于觀察的扇入過濾邊.

定義9.基于觀測的扇出過濾邊.我們稱邊E為一個基于觀測的扇出過濾邊，如果它是一個系統(tǒng)的輸出.

給定觀測Obs={i1= 1,i2= 1,i3= 1,i4= 1,i5= 1,o1=1,o2= 1}，o1和o2均為基于觀測的扇出過濾邊.

定義10.基于觀測的過濾邊.我們稱邊E為一個基于觀測的過濾邊，如果它是一個基于觀測的扇出過濾邊或者它是一個基于觀測的扇入過濾邊.

初始狀態(tài)下，系統(tǒng)的輸入輸出是固定的.因此，任何基于觀測的邊緣邊都是固定的.

定義11.基于觀察的過濾節(jié)點.我們稱一個組件B為基于觀察的過濾節(jié)點，如果該組件的扇入和扇出都是固定的，并且扇出值與扇入值在邏輯上一致，或者該組件是一個B-Node.

給定一個觀測Obs= {i1= 1,i2= 1,i3= 1,i4= 1,i5=1,o1= 1,o2= 1}，在 DOE 編譯過程中，因為N1，N2，N3，N4都是B-Node，所以它們都是基于觀測的過濾節(jié)點.此外，N5也是一個基于觀測的過濾節(jié)點因為它有一個輸入值為0，這與它的輸出值1是一致的.

在OOE方法中，被統(tǒng)治的組件編碼為硬子句，這種設(shè)置與DOE方法中的設(shè)置是相同的.

在OOE編譯方法的預(yù)處理過程中，不僅過濾邊和過濾節(jié)點不被編碼為WCNF，而且基于觀測的過濾邊和基于觀測的過濾節(jié)點也不被編碼為WCNF.

命題1.假定ζ為使用DOE方法求解出的一個TLD，那么使用OOE方法可以求解出一個和ζ具有相同勢的 TLD，ζ’.

考慮觀測Obs= {i1= 1,i2= 1,i3= 1,i4= 1,i5= 1,o1= 1,o2= 1}，我們詳細解釋 DOE 方法和 OOE 方法在進行編碼時的約簡子句的細節(jié).在第1次迭代中，被統(tǒng)治節(jié)點為{N1,N4}.N1被N5統(tǒng)治，N4被N6統(tǒng)治.之后N1的輸出值0被傳播，N5的輸出值是固定的，所以 〈N3，N5〉是一個B-Edge.在第2次迭代時，因為過濾邊 〈N3，N5〉 ，所以N3被N6統(tǒng)治.隨后,N2由N6統(tǒng)治.除此之外，i2，i5被過濾，成為過濾邊.這就是所有的DOE方法的約簡過程及貢獻.剩余的組件{N5,N6}以及邊〈N1，N5〉， 〈N3，N6〉， 〈N4，N6〉均在 DOE 方法中沒有被考慮到.

在OOE方法中，為了考慮將更多的節(jié)點和邊進行約簡，基于觀測的過濾邊和基于觀測的過濾節(jié)點被提出用于減少生成的WCNF子句的數(shù)量.算法2概述了OOE方法的偽代碼.

算法2.編碼MBD到MaxSAT的OOE方法.

輸入：SD，Comps，Obs；

輸出：編譯后的WCNF子句.

① repeat

②Dominators所有統(tǒng)治節(jié)點；

③BackboneComps所有骨架組件；

④BlockedConnections所有阻塞連接；

⑤ if 到達最大迭代次數(shù) then

⑥ break；

⑦ end if

⑧ untilNoMoreChanges；

⑨edgeStack所有基于觀測的過濾邊；

⑩nodeStack所有基于觀測的過濾節(jié)點；

? whileedgeStack ≠NULL do

?eedgeStack中的棧頂元素；

?Propagation(e)；

?nodenodeStack中的棧頂元素；

?Propagation(node)；

? if 獲得一個新的基于觀測的過濾 then

?edgeStack；

? end if

? if 獲得一個新的基于觀測的過濾節(jié)點nodethen

?nodeStack←Push(node)；

? end if

? end while

算法2一直迭代至沒有發(fā)現(xiàn)新的基于觀測的過濾邊和過濾節(jié)點.其中，算法2的行①~⑧和文獻[22]中提出的DOE方法的預(yù)處理部分相同，經(jīng)過DOE預(yù)處理后，初步地，我們找到基于觀測的過濾邊和基于觀測的過濾節(jié)點.算法2在行⑨~⑩分別將初步得到的基于觀測的過濾邊和基于觀測的過濾節(jié)點壓入棧中.在行?~?，算法2找出所有的基于觀測的過濾邊和基于觀測的過濾節(jié)點，旨在減少生成的WCNF子句的數(shù)量.在行?和行?中，函數(shù)Propagation是一種單元傳播技術(shù)用于傳播行?和行?中的e和node變量的賦值.

給定觀測Obs= {i1= 1,i2= 1,i3= 1,i4= 1,i5= 1,o1= 1,o2= 1}，圖2 分別為算法 1 和算法 2 的編譯結(jié)果.在 圖2 中 ， 虛 線 表 示 過濾邊 (如 圖2(a)的 〈N3,N5〉)或基于觀測的過濾邊(如圖2(b)的 〈N1,N5〉).同樣地，虛線點表示的組件代表過濾節(jié)點或基于觀測的過濾節(jié)點(如圖2(a)的N1).過濾邊、過濾節(jié)點、基于觀測的過濾邊和基于觀測的過濾節(jié)點均將不會被編譯成WCNF子句.如圖2所示，僅有實線表示的元件和電路線被編碼為WCNF子句，虛線表示的元件和電路線不被編碼為WCNF子句.在這個例子中，在OOE方法之后，只有1個組件和3條電路線最終被編碼為WCNF子句，圖2(b)中用橢圓表示.

Fig.2 Comparison between DOE and OOE in reduction detail圖2 DOE方法和OOE方法在約簡細節(jié)的比較

5 實驗結(jié)果

在本節(jié)中，我們將在MBD中提出的預(yù)處理方法與目前最好的預(yù)處理方法DOE[22]及不用預(yù)處理過程的編碼方法BE進行了對比.在編碼為MaxSAT問題后求解診斷問題時，我們選擇了一種MaxSAT求解器——UwrMaxSAT[19]進行求解, UwrMaxSAT在 2020年MaxSAT評估中的加權(quán)組中表現(xiàn)最好.實驗分別在ISCAS85和ITC99這2組測試實例上執(zhí)行，這2組測試實例均在文獻[22]中使用.其中，第1組測試實例包含9 998個測試用例，第2個測試實例包含7 822個測試用例.本文提出的OOE方法用C++實現(xiàn)并使用G++編譯.我們的實驗是在 Ubuntu 16.04 Linux 和 Intel Xeon E5-1607@3.00 GHz, 16 GB RAM 上進行.

圖3和圖4分別給出OOE方法與BE方法和DOE方法在求解ISCAS85實例時，MaxSAT求解器求得一個診斷解的運行時間.在實驗中，我們設(shè)置MaxSAT求解的時間上限為0.1 s.如圖3和圖4所示，對于大多數(shù)測試實例，OOE和DOE方法可以在0.1 s內(nèi)通過MaxSAT求解器返回診斷結(jié)果.用BE方法求解時，有1 431個測試實例不能在時間限制內(nèi)得到一個診斷解；但是對于OOE和DOE方法，只有350個實例不能在0.1 s內(nèi)得到一個診斷解.此外，如圖4中所示，對于大多數(shù)測試實例，OOE方法要明顯優(yōu)于DOE方法.

Fig.3 Comparison of the run time of BE and OOE approaches on ISCAS85 benchmark圖3 BE和OOE方法在ISCAS85實例上的運行時間比較

Fig.4 Comparison of the run time of DOE and OOE approaches on ISCAS85 benchmark圖4 DOE和OOE方法在ISCAS85實例上的運行時間比較

Fig.5 The run time of BE and OOE approaches on ITC99 benchmark圖5 BE和OOE方法在ITC99實例上的運行時間比較

圖5和圖6分別顯示了在ITC99實例上OOE方法與BE及DOE方法在求解診斷問題時MaxSAT求解器運行時間方面的比較.我們設(shè)置MaxSAT求解器的時間限制為1 s.坐標軸上的點表示在給定時間內(nèi)無法求解的一些測試實例.使用OOE，DOE，BE方法不能得到一個解的測試實例的個數(shù)分別為4 939，5 197，6 669.在求解實例個數(shù)上OOE方法明顯優(yōu)于BE和DOE方法，除此之外，在大多數(shù)情況下，相比于BE和DOE方法，使用OOE方法能在更短的時間內(nèi)得到一個診斷解.

Fig.6 The run time of DOE and OOE approaches on ITC99 benchmark圖6 DOE和OOE方法在ITC99實例上的運行時間比較

在ITC99 實例和ISCAS85實例上的詳細實驗結(jié)果分別如表1和表2所示：

Table 1 Solved Results for ITC99 Benchmark表1 在ITC99實例上的求解結(jié)果

在2組表中，我們分別列出了4組數(shù)據(jù).第1列顯示電路名稱，第2列顯示測試實例的數(shù)量.第3~6列顯示OOE方法求解診斷時所用時間比競爭對手短的實例個數(shù).從表1和表2可以看出，對每一個電路進行診斷問題求解時，OOE方法都是可行的，且求解結(jié)果顯示，相比于DOE及 BE方法，OOE方法都有明顯的優(yōu)勢.特別是在c880電路上，OOE方法在所有1 182個測試實例中的實驗結(jié)果均優(yōu)于BE方法，有97.8%的實例的實驗結(jié)果優(yōu)于DOE方法.

Table 2 Solved Results for ISCAS85 Benchmark表2 在ISCAS85 實例上的求解結(jié)果

6 總 結(jié)

目前，很多基于SAT的MBD方法把MaxSAT編碼作為分析MBD問題的一個基本步驟.本文在面向支配者編碼的方法研究基礎(chǔ)之上，提出一種OOE的面向觀測的編碼方法，顯著減少了MBD編碼后子句的數(shù)量，進而降低了MaxSAT求解診斷的難度，提高了求解診斷的效率.本文提出了2種方法用于提高OOE的效率.首先，根據(jù)診斷系統(tǒng)的輸入觀測和輸出觀測對過濾邊進行約簡.其次，利用基于觀測的過濾節(jié)點，在編碼時對一些組件進行約簡，進而不被編碼到MBD問題的子句中.實驗結(jié)果表明，通過找到更多的基于觀測的過濾節(jié)點和基于觀測的過濾邊，能有效減少編碼后子句集規(guī)模，進而提高基于MaxSAT計算診斷解的效率.OOE方法在ISCAS85系統(tǒng)和ITC99系統(tǒng)的基準測試實例上求解診斷是高效的.在未來的研究中，將探索多觀測下OOE方法的擴展算法.

作者貢獻聲明：周慧思負責文章主體撰寫和修訂，文獻資料的分析、整理及文章寫作；歐陽丹彤負責確定綜述選題，指導和督促完成相關(guān)文獻資料的收集整理；田新亮負責文獻資料的收集以及部分圖表數(shù)據(jù)的繪制；張立明負責提出文章修改意見, 指導文章寫作.