基于子集一致性檢測的診斷解極小性判定方法

田乃予 歐陽丹彤 劉 夢 張立明

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

基于模型診斷(model-based diagnosis， MBD)是人工智能(artificial intelligence, AI)領域中一個十分活躍的研究分支，對整個AI領域的研究起著重要推動作用[1].其是為克服第1代診斷專家系統的嚴重缺陷而提出的智能推理方法，廣泛應用于通信、網絡、交通、電子設備、航天等諸多領域.

一方面，AI領域的其他分支(如知識表示、機器學習、約束求解等)中許多研究成果可以在MBD問題中得到應用，促進了MBD的發展.例如MBD問題與數據挖掘中的頻繁項集挖掘和子句模式挖掘[2-3]中解的部分特征具有一定的相似性，許多方法策略可以互相應用，相互促進發展.另一方面，MBD的研究暴露了許多AI技術中存在的問題，激發了研究者的研究熱情.例如可以利用MBD改進軟件測試[4].

20世紀60年代，源自航天、軍工等高可靠性工程的迫切需要，在AI領域逐漸形成了診斷推理這一研究熱點.診斷一直是人工智能的一個挑戰，在過去的20年中，研究主要集中于基于模型的診斷，通過利用模型代表物理系統的結構和行為來進行診斷.該方法通過建立真實系統對應的模型，利用系統輸入得到系統的預期行為，然后以預期行為與觀測行為的差異作為診斷算法的輸入，進而計算能夠解釋這種差異的診斷解.

1987年首個MBD方法HS-tree (hitting-set-tree)方法由Reiter[5]提出.其結合Dekleer[6]提出的沖突集概念，通過求解電路所有極小沖突集的極小碰集得到整個電路的所有極小診斷解.雖然該方法保證了解的正確性，但卻存在因剪枝而丟失正確解的可能.1989年Greiner等人[7]對此方法進行改進，提出了HS-DAG(hitting-set directed acyclicgraph)方法.之后國內外學者對間接求診斷方法，即基于沖突的診斷方法進行了大量研究，由于極小碰集求解是基于沖突的診斷方法的關鍵步驟，因此許多研究都集中于極小碰集算法.姜云飛等人[8]提出BHS-tree(binary-hitting-set-tree)方法，該方法基于HS-tree方法，利用枚舉樹結構求解極小碰集，即極小診斷解，解決了HS-tree算法剪枝丟解的情況，并且可以增量求解；趙相福等人[9]提出基于集合勢的CHS-tree(cardinality-based hitting-set-tree)方法，每次選擇當前集合簇中勢最小的集合擴展，并結合集合簇中元素出現的頻率，將大問題分解成子問題，進而得到不包含該擴展集合中各元素的集合簇的所有極小碰集；歐陽丹彤等人[10]提出基于動態極大度的極小碰集求解方法，提出未擴展元素度和結點度的概念，盡早生成集合簇的碰集，減少枚舉樹生成結點的個數，提高了求解效率.Jannach等人[11]通過并行化枚舉樹的結構計算碰集，更好地利用計算資源而不會丟失任何診斷解.

間接求解的診斷方法由于求解過程分為求極小沖突集和求極小碰集2個步驟，求解效率受到2部分所使用算法的共同制約.隨著對MBD 問題研究的深入與計算機硬件的發展，許多學者對直接求解 MBD 的方法進行了研究[12].其中，基于SAT(satisfiability)的診斷方法吸引了大量研究者的關注.

SAT問題是首批被證明的NP-完全問題[13]，具有重要的理論和實用價值，長久以來吸引著國內外學者的關注，其求解過程的研究一直是人工智能領域的核心難題之一.近些年來對SAT問題的研究取得了很大的進步，很多已有算法得到了有效地優化改進，同時許多創新方法不斷被提出.將MBD 問題轉化為 SAT 問題進行求解，能夠克服診斷問題復雜性不斷增加的難題，因而得到眾多學者的廣泛關注[14].

Smith等人[15]首次提出了基于SAT求解的多故障診斷與定位算法，為之后基于SAT的模型診斷研究提供了基礎.Metodi等人[16]提出把復雜的MBD預處理問題和SAT編譯技術結合在一起的編譯方法，進而達到簡化合取范式(conjunctive normal form, CNF)的目的.之后，Metodi等人[17]提出基于求極小勢診斷的新編譯方法，該方法進一步對CNF進行了簡化.Koitz等人[18]提出將故障信息轉化為用于溯因模型診斷中的Horn子句，利用一個映射函數自動化建模過程.一些直接求解診斷方法和求極小碰集問題相似，都是元素對應超圖中集合遍歷問題.而由于超圖數據結構復雜，在求解時多采用集合枚舉樹(set-enumerations-tree, SE-tree)[19]形式化方法遍歷超圖中的集合.趙相福等學者提出了基于枚舉樹的CSSE-tree(conflict-set based on set-enumerations-tree)[20]方法，將被診斷系統的模型和觀測結果用CNF描述并利用 SAT求解器求取診斷解.歐陽丹彤等人[21]基于問題的結構特征，對CSSE-tree方法進行改進，有效地實現了對診斷的無解空間進行剪枝，并對部分集合枚舉樹從底層結點到根結點進行反向搜索，構建了LLBRS-tree(last-level based on reverse search-tree)方法.該方法減少了SAT求解次數，縮減了求解問題規模，是一種求解效率較高的方法.劉夢等人[22]在LLBRS-tree方法的基礎上，使用電路分解并利用非故障輸出子電路組件間組合形成的結點肯定不是診斷解的特性，縮減了問題規模，提出結合問題特征的分解式方法GD(grouped diagnosis)方法.劉伯文等人[23]提出電路分塊診斷方法ACDIAG(abstract circuit diagnosis)方法，通過對電路分塊縮減了電路規模，并利用LLBRS-tree方法對分塊后的電路求解得到極小塊診斷解；結合抽象電路的結構特征，利用診斷解拓展方法對極小塊診斷解擴展得到原電路全部極小診斷解.

為保證最終得到診斷解是極小的，診斷解的極小性檢測是求解基于模型診斷問題的關鍵步驟.之前的研究多集中于碰集極小性的研究，劉思光等人[24]提出基于元素獨立覆蓋度檢測的碰集極小性判定方法ICC(independent coverage checking)方法并通過深入分析增量求解過程中非極小碰集的產生原因，給出ICC方法的增量判定形式IICC(incre-mental independent-coverage-checking)方法，提高了碰集求解的效率.王榮全等人[25]提出將碰集求解問題轉換成SAT問題進行迭代求解，并給出結合元素覆蓋集合度的極小化策略的高效極小碰集求解方法.碰集的極小化策略可應用于基于沖突的診斷方法.但目前研究多集中于更為高效的直接求解診斷方法.本文在對LLBRS-tree, GD, ACDIAG這3種方法充分研究的基礎上，發現其使用的診斷解極小性檢測方法存在的不足：原有極小性檢測方法隨著求解過程中得到的診斷解數量增多，檢測難度逐漸提高，耗時也隨之增大.若能對此進行優化，減小診斷解極小性檢測過程的耗時，將對現有算法效率有所提高.針對此問題，本文提出一種基于子集一致性檢測的診斷解極小性判定方法.該方法無需同已得到的診斷解進行比較，通過對得到的診斷解自身進行檢測來判斷其真子集中是否含有診斷解，進而進行極小性判定，避免了傳統診斷解極小性檢測方法的不足.該方法避免了求解過程中診斷解集合增大對效率的影響，進而提高了診斷算法的整體求解效率.

1 預備知識

本節將介紹基于模型診斷和SAT問題的相關概念及定義，同時給出使用SAT方法求解模型診斷問題過程中將問題對應的電路模型轉化成CNF文件的方法.

1.1 基于模型的診斷

下面給出基于模型的診斷問題的相關定義.

定義1.診斷系統[5]. 一個MBD系統定義為一個三元組SD,COMPS,OBS，其中：

1)SD(system description)為系統描述，是一階謂詞公式的集合；

2)COMPS(system components)為系統的組成部件集合，是1個有限的常量集；

3)OBS(system observation)為觀測集，是一階謂詞公式的有限集.

定義2.診斷問題[5].基于一個待診斷系統SD,COMPS,OBS，產生一個診斷問題，當SD∪{AB(c)|c∈COMPS}∪OBS不一致時.

定義3.診斷[5]. 基于一個MBD系統SD,COMPS,OBS，Δ?COMPS是一個診斷，當SD∪{AB(c)|c∈Δ}∪{AB(c)|c∈COMPS-Δ}∪OBS一致時.

定義4.極小診斷[5]. 基于一個MBD系統SD,COMPS,OBS，Δ?COMPS是一個極小診斷當且僅當不存在子集Δ′?Δ是一個診斷.

在系統的SD,COMPS,OBS所組成的觀測行為與預期行為發生沖突之時診斷問題產生.基于模型診斷問題的目的是找到可以解釋這種差異的診斷解.

1.2 SAT問題

SAT問題，一直以來都是理論計算機科學和人工智能領域的著名問題.給定一個布爾公式，求解SAT問題的目的是，確定是否存在一組變量賦值使得公式真值為真，若存在，需要返回一組滿足條件的變量賦值.SAT問題在模型檢驗、邏輯電路優化等應用方面有著非常重要的作用.著眼于SAT問題的理論意義和實際應用價值，其相關研究已成為國內外熱點之一.下面給出SAT問題的相關定義.

定義5.文字[16]. 給定n個布爾變量l1,l2,…,ln,0≤i≤n，其中li或li的否定稱為文字.

定義6.子句[16]. 稱文字用析取符號連接而成的公式為子句.

定義7.合取范式[16]. 將子句用合取符號連接而成的公式稱為合取范式.

定義8.可滿足不可滿足[16]. 對某一CNF公式，如果存在使其公式計算值為真的變量賦值，則稱該CNF公式是可滿足的；反之，如果不存在這樣的賦值，則稱該CNF公式是不可滿足的.

例1.給出CNF范式：

C={1:(a),2:(a),3:(a∨b),4:(b)},

C是不可滿足的，因為子句1和子句2無法同時為真，同樣也找不到一組賦值使子句1,3,4同時為真.

1.3 集成電路轉化為CNF

3=1∧2,

3?1∧2,

(3→1∧2)(1∧2→3),

最終化簡后的結果即是:

Fig. 1 Symbol of AND gate圖1 與門符號

將系統的相應描述以CNF 文件的形式表示.主要包含電路邏輯和電路觀測2部分.

CNF文件的格式為：CNF文件中每行為1個對應系統相關描述的子句，最后以0結尾.

以圖2中國際標準測試電路ISCAS-85中的c17電路為例，電路邏輯對應的相關CNF 文件如圖3所示.

Fig. 2 Logic circuit of c17圖2 c17邏輯電路

p cnf 17 18-7 -8 -14 1 07 14 1 08 14 1 0-8 -9 -15 2 08 15 2 09 15 2 0-15 -10 -16 3 015 16 3 010 16 3 0-15 -11 -17 4 015 17 4 011 17 4 0-14 -16 -12 5 014 12 5 016 12 5 0-16 -17 -13 6 016 13 6 017 13 6 0

Fig. 3 CNF file of c17
圖3 c17邏輯電路對應的CNF 文件

圖3中第1行p cnf 17 18表示該電路系統轉化為CNF 文件格式后有17個變量、18條子句，p cnf為關鍵字.

將系統描述SD和系統觀測OBS轉換為CNF文件后，就可以作為SAT求解器的輸入對待診斷系統進行求解.

2 MBD相關算法

本節將介紹基于模型診斷的相關算法，主要介紹LLBRS-tree方法以及基于該方法的優化：分解式GD方法和電路分塊ACDIAG方法.這些方法都是目前效率較高的診斷求解方法，同時，它們都采用了相同的診斷解極小性檢測方法.

2.1 基于SE-tree調用SAT的診斷方法

基于SE-tree調用SAT的診斷方法是將集合枚舉樹應用于MBD問題上，這種樹模型可以以一種有結構的方式枚舉出給定集合的冪集.

該方法對待診斷系統組件集COMPS對應的SE-tree進行遍歷，同時對所遍歷到的結點是否為診斷解進行判定，當遍歷完成時，便可得到待診斷系統的所有診斷解.結點判定的基本思想是假設結點中的元件為故障并將其余元件都置為正常，將結點對應的單元子句加入到之前由系統描述SD和系統觀測OBS轉換而來的CNF文件中，作為SAT求解器的輸入，進行一致性檢測.若可滿足，則該結點是一個診斷解，將此診斷解保存.

2.2 LLBRS-tree方法

LLBRS-tree方法對診斷的無解空間進行剪枝,并對部分集合枚舉樹從底層結點到根結點進行反向搜索.該方法減少了SAT求解次數，縮減了求解問題規模，是一種求解效率較高的方法.下面給出相關定義.

定義9.有解剪枝[21].在遍歷某一待診斷系統組件集對應的集合枚舉樹時，對于樹中的某一結點，其父結點或祖先結點如果是可滿足的，即是診斷解.那么該結點一定不是極小診斷解，可以跳過對枚舉樹中此類結點的判斷，稱這一操作為有解剪枝.

定義10.無解剪枝[21].遍歷一棵集合枚舉樹，對于樹中的某一結點，其子結點或者子孫結點如果是不可滿足的，即不是診斷解，那么該結點一定不是診斷解，跳過對枚舉樹中此類結點的判斷過程，這叫做無解剪枝.

定義11.反向搜索[21].針對一棵集合枚舉樹，當已知枚舉樹的層數時，稱從枚舉樹的最后一層向枚舉樹的根結點搜索的過程為樹的反向搜索.

LLBRS-Tree方法主要是基于定義9～11，對集合枚舉樹以反向搜索的過程遍歷，同時調用SAT求解器對樹上的結點是否為診斷解進行判定：

1) 如果結點可滿足，則對結點進行極小性檢測，并根據檢測結果對診斷解集進行相應操作.根據定義9，可以將該結點未訪問的子孫結點減掉，即有解剪枝.第2步將判斷該結點的父結點.

2) 如果結點不可滿足.根據定義10，可以將該結點的父結點減掉，即無解剪枝.下一步判斷該結點右邊的結點.

LLBRS-tree方法利用有解剪枝和無解剪枝的策略，減小求解問題規模從而提高診斷求解效率.

2.3 GD方法

GD方法通過對電路進行分解并利用非故障輸出子電路組件間組合形成的結點肯定不是診斷解的特性，縮減診斷問題規模，從而提高求解效率.

定義12.輸出組件集[22]. 設某個待診斷系統可表示為SD,COMPS,OBS，稱O?COMPS為輸出組件集，當對于所有組件c∈O，其輸出為該待診斷系統的輸出.

定義13.故障輸出組件集[22]. 設某個待診斷系統可表示為SD,COMPS,OBS，稱ABCompS?O是故障輸出組件集，當組件c∈ABCompS的輸出是該待診斷系統的故障輸出.

定義14.可達通路[22]. 診斷問題中，組件c1到組件c2有可達通路表示組件c1到電路輸出的路徑上經過組件c2，此時path(c1,c2)為真.

定義15.故障輸出子電路組件集[22]. 設某個待診斷系統可表示為SD,COMPS,OBS，其中故障輸出組件集ABSubCircuitCompS?COMPS是一個故障輸出子電路組件集,當{c|c∈ABCompS∨path(c,c0)}，其中，c0∈ABCompS.即子電路中組件c是ABCompS中組件或者到ABCompS中某一組件有可達通路.

GD方法根據輸出觀測與預期的差異，將輸出分為故障輸出與非故障輸出.以此為條件對電路進行分解，分為故障輸出子電路和非故障輸出子電路.

對于非故障輸出子電路組件，由于非故障輸出子電路組件集中的任意元素組成的集合不可能是診斷解，因此GD方法將非故障子電路集中的組件放在待枚舉元素的后半部分，并將其對應的子樹剪掉.而故障輸出子電路組件則使用枚舉樹并利用LLBRS-tree算法進行求解.

GD方法結合問題特征和電路邏輯電路組件進行分解，縮減問題規模，進而減少求解過程中調用SAT求解器的次數，提高診斷求解效率.

2.4 ACDIAG方法

ACDIAG方法是對電路進行抽象分塊來縮減電路規模的高效診斷算法.

定義16.起始元件[23]. 對于一個待診斷系統，稱滿足3個條件之一的元件為起始元件：

1) 元件為系統輸出元件；

2) 元件的輸出是2個或2個以上元件的輸入；

3) 元件是多輸入元件，即元件輸入端個數大于2.

結合電路結構特征，給出對電路的分塊規則[23]：

1) 找出電路中所有起始元件a1,a2,…,ak即將電路劃分為k塊；

2) 對每個起始元件ai(1≤i≤k)進行拓展，若元件b的輸出作為元件ai的輸入，并且元件b不是起始元件，則將元件b擴展到ai所代表的分塊中.

以此分塊規則得到的抽象電路，每個子電路塊有且僅有一個輸出，并且由該輸出元件代表.

ACDIAG方法利用LLBRS-tree方法對分塊后的抽象電路求得極小診斷解，稱作極小塊診斷解.再利用診斷解拓展方法，對極小塊診斷解進行拓展，從而得到原電路的全部極小診斷解.

ACDIAG方法前期通過縮減電路規模減少了利用LLBRS-tree方法求取診斷解的時間，再利用拓展方法得到全部解，實驗表明其拓展所需時間遠小于極小塊解求解時間，因此大大提高了求解效率.

3 診斷解極小性判定過程

3.1 原有診斷解極小性判定過程

判定診斷解的極小性是MBD相關算法中至關重要的一步.根據定義4可知，Δ是一個極小診斷當且僅當不存在子集Δ′?Δ是一個診斷，即不存在Δ的任何真子集也是待診斷MBD系統的一個基于一致性診斷.極小性判定過程必須基于此定義.下面給出LLBRS-tree方法極小性判定過程的具體方法，GD方法和ACDIAG方法是基于LLBRS-tree方法的，其極小性判定過程也應用了相同的方法.

算法1.診斷解極小性檢測算法.

函數:MinialDiag_Checking(Diag,DigRes)

輸入:診斷解Diag、極小診斷解集合DigRes={Diag1，Diag2，…，Diagn};

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

Begin

① for (i=1;i≤n;i++)

② ifDiag?Diagi

③DigRes.Remove(Diagi);

④ end if

⑤ else ifDiagi?Diag

⑥ return;

⑦ end if

⑧ end for

⑨DigRes←DigRes∪{Diag};

End

在這一過程中，被檢測為診斷解的組件集作為輸入，若在已有診斷解集中發現新得到診斷解的真超集，則說明該超集必不為待診斷系統的極小診斷解將其從極小診斷集中刪去(行③);若發現新得到診斷解的子集，則新得到診斷解必不是極小診斷，將該解丟棄，結束比較過程(行⑥);若比較過程結束時都未發現新得到診斷解的真子集，則將該診斷解暫時加入極小診斷解集中(行⑨).

當對集合枚舉樹的遍歷結束時，即診斷求解算法終止時，極小診斷解集中保留的診斷解即是待診斷系統的全部極小診斷解.需要注意的是，在算法運行的過程中，極小診斷解集中保留的診斷解并不一定是極小的，即可能保留了大量冗余解.

這種方法存在的主要問題是，極小診斷解集的規模會隨著診斷求解算法的進行而不斷變大，新得到診斷解的極小性判定時間也會隨之增加.因為每當得到一個新的診斷解，都需要將它與極小診斷解集中部分甚至全部診斷解進行比較.由于此方法的耗時往往與診斷解集的大小正相關，當問題后期診斷解集規模較大時，使用此極小性判定方法逐一比較會帶來較多的時間開銷，影響求解效率.而下面提出的基于子集一致性檢測的診斷解極小性判定方法則避免了此問題.

3.2 基于子集一致性檢測的診斷解極小性判定方法

本文提出的基于子集一致性檢測的診斷解極小性判定方法完全遵循定義4，即如果一個診斷解的所有真子集都不是診斷解，那么這個診斷解就是關于MBD系統的一個極小診斷解.為避免3.1節所給出的傳統診斷解極小性判定過程存在的不足，基于子集一致性檢測的診斷解極小性判定方法在求得診斷解之后僅針對診斷解自身進行檢測，即檢測其真子集中是否含有診斷解，按照此方法加入診斷解集合中的診斷解全部是極小的，避免了比較的過程.

對已求得診斷解的所有真子集進行判斷，可以檢查其真子集中是否含有診斷解，但如果對每個子集進行檢測，則調用SAT求解器次數過多，會消耗較多的時間，而我們可以利用SAT求解器判定某一狀態下系統邏輯和觀測行為的一致性來達到同樣的目的.下面首先給出算法2來介紹如何利用SAT求解器來判斷一個組件集合是否是待診斷系統的診斷解.

算法2.診斷解判斷算法.

函數:Is_Sol(ps[])

輸入:待判定組件集ps、系統描述文件SD.cnf、系統觀測文件OBS.cnf；

輸出:bool類型值(如果組件集ps是系統的診斷解，則返回1;否則返回0).

①SD.cnf.add(clause∈OBS.cnf);

②SD.cnf.add(ps中每個組件對應的反常單元子句);

③SD.cnf.add(COMPS-ps中每個組件對應的正常單元子句);

④isSAT←SATsolver(SD.cnf);

⑤ ifisSAT=SAT

⑥ return 1;

⑦ else

⑧ return 0;

⑨ end if

算法2首先將系統觀測文件OBS.cnf中的子句加入到表示系統描述的SD.cnf文件中(行①).對于待判定的組件集合ps中的組件，將其對應的反常單元子句即用正文字描述，加入到SD.cnf文件中(行②)，以此假設這些組件均是故障組件.對于系統組件集中除去待判定組件集的剩余元素，使用負文字描述，即將COMPS-ps中每個組件對應的正常單元子句加入到SD.cnf文件中(行③)，以此假設這些組件均是非故障組件.例如假設系統總共有7個組件COMPS={C1,C2,C3,C4,C5,C6,C7}，待判定組件集ps={C1,C2,C3,C4}時，那么加入系統描述SD.cnf文件中的子句應為：

1 0

2 0

3 0

4 0

-5 0

-6 0

-7 0

然后調用SAT求解器對SD.cnf文件進行可滿足性判斷.如果可滿足，則表明在組件集ps中的組件均為故障組件而COMPS-ps中的組件均為正常組件的情況下，系統當前的觀測行為是可以解釋的.根據診斷解的定義可知，組件集ps是診斷解，返回1;否則，組件集ps不是診斷解，返回0.

以此為基礎，我們發現可以利用SAT求解器檢查組件集ps是否存在為診斷解的真子集.

定理1.設某個待診斷系統可表示為SD,COMPS,OBS，Sub?COMPS為該MBD的一個診斷解，如果?S∈Sub，且SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是一致的，則?Sub′?Sub-{S}為待診斷系統的診斷解.

證明.

反證法.假設:

SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是一致的；且不存在Sub′?Sub-{S}為待診斷系統的診斷解.

Sub為已知為診斷解，如果不存在Sub′?Sub-{S}為診斷解，則說明若存在為Sub真子集的診斷解，該診斷解中必包含S，那么:

SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}不能推出一致，即假設S組件為正常同時限定診斷解為Sub真子集的情況下是無法解釋當前系統的行為.此時:

SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是不可滿足的.與上述條件矛盾，因此假設不成立.

證畢.

定理2.設某個待診斷系統可表示為SD,COMPS,OBS，Sub?COMPS為該MBD的一個診斷解，如果對?S∈Sub，SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是不一致的，則Sub為待診斷系統的極小診斷解.

證明.

因為對于S∈Sub，如果：

SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是不一致的，根據定理1可以得到不存在Sub′?Sub-{S}.所以如果對于:

?S∈Sub，SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}都是不一致的，則可說明不存在Sub′?Sub為診斷解，根據極小診斷的定義可證得Sub為待診斷系統的極小診斷解.

證畢.

基于定理1與定理2，給出利用SAT求解器進行基于子集一致性檢測的診斷解極小性判定的算法3.

算法3.基于子集一致性檢測的診斷解極小性判定算法.

函數:Is_MinimalSol(diag[])

輸入:診斷解diag={D1,D2,…,Dn}、系統描述文件SD.cnf、系統觀測文件OBS.cnf；

輸出:bool類型值(如果診斷解diag是系統的極小診斷解，則返回1;否則返回0).

①SD.cnf.add(clause∈OBS.cnf);

②SD.cnf.add(COMPS-diag中每個組件對應的正常單元子句);

③ for (j=1;j≤n;j++)

④CNF←SD.cnf;

⑤CNF.add(Dj對應的正常單元子句);

⑥isSAT←SATsolver(CNF);

⑦ if (isSAT=SAT)

⑧ return 1;

⑨ end if

⑩ end for

算法3可針對已知診斷解進行子集一致性檢查，輸入是通過算法2判定為診斷解的組件集.同算法2一樣，需將系統的觀測文件OBS.cnf中的子句添加到系統描述文件SD.cnf中(行①).依據定理1，對于已知診斷解diag中的每個組件，依次將它們與COMPS-diag中所有組件對應的正常單元子句加入到表示系統描述和觀測的CNF文件中，以此假設它們都是非故障組件.之后，調用SAT求解器判定CNF文件的可滿足性，對應定理1中判定:

SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}是否一致，從而判斷這種假設能否解釋當前系統的行為，即檢查子集的一致性(行②～⑥).如果可滿足，則說明存在diag′?diag-Dj為診斷解，即診斷解diag的真子集中存在診斷解，根據定義3可知診斷解diag不是待診斷系統的極小診斷解，跳出循環，算法結束(行⑦～⑩).依據定理2可知，如果循環結束沒有找到diag的真子集為診斷解，即對應定理2中對于?S∈Sub，SD∪OBS∪{AB(c)|c∈{S}∪(COMPS-Sub)}都是不一致的，則可以判定diag為待診斷系統的極小診斷解(行).

例2.假設系統總共有7個組件COMPS={C1,C2,C3,C4,C5,C6,C7}，已知組件集diag={C1,C2,C3,C4}是診斷解時，我們需要加入到表示系統描述和觀測的CNF文件中的子句為：

1) -1 0

-5 0

-6 0

-7 0

以此假定組件C1,C5,C6,C7為非故障組件.之后調用SAT求解器，判斷一致性，如果是可滿足的，則表明{C2,C3,C4}的子集中有診斷解，那么組件集{C1,C2,C3,C4}必不是極小診斷解，算法結束.否則，繼續將子句依次加入到CNF文件中并依次檢查CNF文件的可滿足性：

2) -2 0

-5 0

-6 0

-7 0

3) -3 0

-5 0

-6 0

-7 0

4) -4 0

-5 0

-6 0

-7 0

如果依次調用SAT求解器檢測加入以上子句的CNF文件，均為不可滿足，則表明組件集{C1,C2,C3,C4}的真子集中沒有診斷解，診斷解{C1,C2,C3,C4}是待診斷系統的極小診斷解.

下面給出一個實例來闡述算法3的執行過程.

例3.以圖2中國際標準測試電路ISCAS-85中的c17電路為例，該電路有6個組件COMPS={1,2,3,4,5,6}均為與非門，假設當前輸入觀測點“7”，“8”，“9”，“10”，“11”的觀測值分別為高電平、高電平、低電平、高電平、低電平.輸出觀測點“12”，“13”的觀測值為低電平、高電平.則系統觀測的CNF文件描述如下：

7 0

8 0

-9 0

10 0

-11 0

-12 0

13 0

因觀測行為與預期行為沖突，產生診斷問題.設已得到診斷解diag={1,3,6},需檢測其極小性.根據算法3，依次加入3組子句到表示系統描述和觀測的CNF文件中：

1) -1 0

-2 0

-4 0

-5 0

2) -3 0

-2 0

-4 0

-5 0

3) -6 0

-2 0

-4 0

-5 0

分別調用SAT求解器依次檢測加入以上子句的CNF文件，均為不可滿足，則根據定理2，可知組件集{1,3,6}的真子集中沒有診斷解，即組件集{1},{3},{6},{1,3},{1,6},{3,6}均不是診斷解，診斷解diag={1,3,6}是該系統的極小診斷解.

算法3避免了算法1隨著極小診斷解集規模的增大而導致診斷解極小性檢查耗時大幅增加的問題.通過針對已知診斷解子集一致性進行判斷，檢測其真子集中是否含有診斷解來進行極小性判定.同時，該方法調用SAT求解器的次數與待檢測診斷解中包含組件的個數線性相關，比對該診斷解全部真子集進行檢測要少得多.

復雜性.假設待檢測診斷解包含組件個數為n，當前已有診斷解個數為m. 算法3，即SCD(subset consistency detection)方法在最壞情況下最多需調用n次一致性檢查.而傳統極小性判定方法則需將此診斷解與m個診斷解判定子集關系，其復雜度為nm.

當m較大時，SCD方法復雜性明顯低于傳統極小性判定方法.而MBD問題隨著求解過程的進行，m必不斷增大，因此SCD方法的求解效率優于傳統方法.

完備性.本文提出的子集檢測方法針對的是求得的診斷解的極小性判定，不影響求解過程，因此不會存在丟解的情況，最終得到的是待診斷系統的全部極小診斷解.

因此，我們給出的方法不僅避免了原有方法的不足，同時也盡最大可能地減少了判定過程中SAT求解器的調用次數，最大程度上降低了診斷解極小性判定過程的耗時.

4 實驗結果

本部分對SCD方法的有效性進行實驗測試.將SCD方法應用于目前求解效率較高的GD方法和ACDIAG方法，并分別與應用原有診斷解極小性檢測方法的GD和ACDIAG方法進行對比,進而對SCD方法的實驗數據進行分析.采用的實驗環境為Intel?CoreTMi5-3470 CPU@3.20 GHz，Ubuntu 64位系統.

對于GD方法和ACDIAG方法以及SCD方法的診斷解極小性判定過程，調用開源SAT求解器Picosat[26]進行可滿足性檢測.

本文的測試用例來源于國際標準測試電路ISCAS-85，包含了電路c17,c432,c499,c880,c1355,c1908.時間限制為172 800 s(48 h)，超出此時間記為TO.

表1給出SCD方法應用于GD方法的實驗結果對比，表格第1行的l表示所求診斷解的長度；第1列表示測試所用電路實例；num表示求得診斷解個數.SCD與GD列分別表示將SCD方法應用于GD方法與原始GD方法求解耗時.可以看出對于較簡單電路如c432,c499,c880,當極小診斷長度小于等于3時，應用原有診斷解極小性檢測方法的GD方法與應用SCD方法的所用時間并無明顯差別.但當所求診斷長度達到4時，應用SCD方法的GD方法求解效率開始有明顯提高，以c432電路表現尤為明顯，求解時間縮短近50%，對c499和c880電路的求解效率也均有不同程度的提高.當所求診斷長度達到5時，應用SCD方法的優勢更為明顯，在原有算法無法在限制時間內得到結果的情況下，應用SCD方法可以求得診斷解.而對于較復雜的c1355和c1908電路，當診斷解長度達到3時，算法效率就已有一定提高.當所求診斷解長度較小時，診斷解個數較少，應用原有極小性檢測方法逐一比較的次數也較少，耗時不多，因此2個方法求解效率基本相同.當所求診斷長度較大時，隨著算法運行生成的診斷解個數逐漸增多，極小診斷解集規模不斷增大.此時，采用原有極小性檢測方法，每當得到一個診斷解，都需要將它與極小診斷解集中部分甚至全部診斷解進行比較，使得極小性檢測過程較為耗時.而應用SCD方法則可避免此問題，只需調用SAT求解器對新求得的診斷解子集一致性進行判定，在保證了每個加入極小診斷解集中的診斷解都是極小的同時，不用增加額外比較耗時，因此算法效率得到了提高.

我們也將SCD方法應用于ACDIAG方法進行了實驗，實驗結果對比如表2所示，SCD與ACD列分別表示將SCD方法應用于ACDIAG方法與原始ACDIAG方法求解耗時.可以看出SCD方法應用于ACDIAG方法同樣是有效果的.ACDIAG方法是將復雜電路抽象為較簡單電路進行求解，得到抽象電路的極小診斷后拓展得到全部診斷解，而SCD方法應用于抽象電路求得極小診斷解這一過程.因為是已簡化的抽象電路，前期求得診斷解個數較少，所以當極小診斷長度≤4時，應用SCD方法的ACDIAG方法與原始ACDIAG方法的效率基本無明顯差別，但對于較復雜電路c1355,當診斷長度達到4時，算法效率已提高40%;對于較簡單電路如c432,c499電路當診斷長度達到5時，算法效率提高了50%左右.這反映出傳統診斷解極小性檢測方法存在的問題：對極小診斷解集規模較為敏感,而SCD方法避免了這點不足.因此，隨著診斷解數量不斷增多，本文提出的SCD方法的優勢逐漸顯現.

Table 1 The Running Time of SCD Method Based GD表1 基于SCD方法的GD方法運行時間對比

Note: The time limit is 172800s (48 h). Timeout is denoted as TO.

Table 2 The Running Time of SCD Method Based ACDIAG表2 基于SCD方法的ACDIAG方法運行時間對比

Note: The time limit is 172 800 s (48 h). Timeout is denoted as TO.

表1、表2的實驗對比結果可以體現出SCD方法的有效性.本文以GD和ACDIAG方法為例，將SCD方法應用于這2個目前較高效的方法，算法效率均得到了一定的提高.實驗結果也與我們提出的改進思想吻合，當所求診斷長度越長時，應用SCD方法對算法效率的提升也就越大.

5 結束語

在人工智能領域，基于模型診斷問題的研究一直備受中外學者的關注.本文通過對診斷解的極小性與該診斷解子集關系的研究，提出基于子集一致性檢測的診斷解極小性判定方法——SCD方法.該方法通過對已知診斷解的部分子集進行一致性檢測，從而給出診斷解的極小性判定，避免了原有方法診斷解之間的比較過程，減少了診斷解極小性檢查過程的耗時.且SCD方法可應用于多個目前效率較高的基于模型診斷求解算法，如GD和ACDIAG方法.通過實驗對比，針對不同電路，應用SCD方法的診斷方法求解效率均有明顯提高，最高可提高約50%，并且由于傳統診斷解極小性檢測方法存在對診斷解集規模較為敏感的問題，隨著所求診斷解長度的增加，SCD方法帶來的優勢將更加顯著.