結合DOEC極小化策略的SAT求解極小碰集方法

王榮全 歐陽丹彤 王藝源 劉思光 張立明

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

人工智能專家Console等人[1]指出基于模型診斷(model based diagnosis, MBD)的研究對整個人工智能領域的研究有著重要的作用.學者Struss[2]稱基于模型診斷是人工智能領域極富有挑戰性和具有檢驗性的課題.基于模型診斷的核心步驟是根據系統的描述和觀測，得到極小沖突集合簇[3]，然后以其為輸入并利用碰集(hitting set, HS)的求解方法計算得到系統所對應的極小診斷解即極小碰集(minimal hitting set, MHS)，因此求解MHS問題是模型診斷中比較核心的問題之一[4].此外很多的實際和理論問題都可以轉化為MHS問題[5-6]，如極小集合覆蓋和極小頂點覆蓋等極小覆蓋問題均是極小碰集的特殊形式、師生選課問題、蘊涵推理問題以及智能規劃的核心問題.

碰集(hitting set, HS)問題最早是由加州大學伯克利分校的計算機專家Karp在1972年提出，隨后MBD專家Reiter[7]首次提出了一種求解極小碰集的方法HS-Tree，但該方法基于枚舉樹并遍歷整棵枚舉樹導致效率較低，且會因剪枝丟失解.因此，Greiner等人[8]提出HS-DAG方法，優化并改進了HS-Tree方法的剪枝策略，雖然解決因剪枝而丟失解，但因新的剪枝規則的應用導致計算復雜度大幅度增加.隨著對極小碰集問題的深入探索研究，許多新的求解方法陸續被提出.2001年，Wotawa[9]通過改進HS-Tree方法提出了HST-Tree方法，雖然效率提升，但其通用性降低，并未徹底解決丟解的問題，空間復雜度較高；2003年，姜云飛等人[10]提出布爾代數方法，從解的完備性和方法的高效性來看，該方法是目前較好的求解方法之一，因為其不需要建立較復雜的樹結構，只需遞歸計算字符串操作，比之前所有的方法在空間復雜度和時間復雜度都有降低，在提高求解效率的同時簡化了數據結構；2004年，歐陽丹彤等人[11]改進了HS-DAG方法，通過剪枝無解空間達到提高效率，但因數據結構復雜使方法實現繁瑣；2006年，趙相福等人[12]提出了HSSE-Tree方法，其利用與元素相關聯的沖突集個數來計算碰集并在標準的SE-tree上對節點種類進行標識，從而提高搜索效率；2010年，陳曉梅等人[13]提出了BNB-HSSE方法，采用分支定界法與集合枚舉法相結合的方法來降低求解規模；2011年，張立明等人[14]提出了基于動態極大度的DMDSE-Tree方法，其通過結點度概念較早地生成極小碰集，減少了生成結點的數量；2012年，Pill等人[15]對布爾代數方法改進了部分規則，有效提升了該方法對特定問題的求解效率；2015年，王藝源等人[16]提出了利用CSP求解器求解極小碰集的CSP-MHS方法，其思想是通過將求解極小碰集問題轉為約束滿足問題，然后調用CSP求解器進行求解，并根據約束可滿足問題的特點去求解具有某些特征的極小碰集.

以上是求解MHS的完備方法，隨著近似求解策略的不斷產生和完善，眾多的非完備極小碰集求解方法也陸續被提出[17-18].其中大多采用的是隨機搜索策略，其特點是犧牲了解的完備性從而能針對規模較大的問題可以在較短時間進行求解.此外，隨著并行和分布式的發展，很多學者也開始投入到用并行或分布式的方法去求解極小碰集問題[19-20].

本文在對SAT問題的深入理解與分析的基礎上并與極小沖突集合簇求解極小碰集過程的本質相結合，提出利用目前較為成熟的SAT求解器進行碰集求解，把極小沖突集合簇轉換表示成SAT求解器的可求解的CNF形式.在每次求解出一個碰集之后利用首次提出的DOEC極小化策略進行極小化，在每次極小化的過程中，先把碰集通過元素覆蓋集合度的勢找出其中所有的冗余元素，并對其進行刪除，從而高效地實現碰集極小化.最后把已經極小化產生的極小碰集以取反的隔離子句的形式添加到CNF中并繼續調用SAT求解器進行求解，直到SAT求解器返回不滿足，即問題求解.由于每個求出的碰集都被極小化過，并以取反的隔離子句的形式添加到求解器的CNF中，所以在下次求解的過程中不會求解極小化后的極小碰集的求解空間，從而實現了對部分求解空間的屏蔽.但該方法不會屏蔽極小解，從而保證求出所有的解，保證了解的完備性.這種方法的主要優點是：1)因采用寬度優先求解方式，與上述提到的方法相比能較快地得到解；2)減少了對大量非極小化碰集的無用求解，大幅提高方法效率；3)根據SAT求解器的是否滿足即可判斷求解是否結束；4)僅使用樹結構來描述分析問題，實現過程中僅使用數據結構簡單的數組描述，所以實現容易.

1 預備知識

在本節，首先介紹下基于模型診斷的基本概念及其相關的基礎知識.

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

定義1[7]. 一個系統可定義為一個三元組(SD,COMPS,OBS)，其中：

1)SD為系統描述，是一階謂詞公式集合，SD描述了待診斷系統的相關背景知識;

2)COMPS是系統組成部件的集合，是一個有限常量集；

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

定義2[7]. 沖突集CS是一個部件集{c1,c2,…,cn}?COMPS當且僅當SD∪OBS∪{AB(c1),AB(c2),…,AB(cn)}是不一致的.其中AB為一元謂詞，表示“abnormal”.AB(c)為真，當且僅當c異常，且c∈COMPS.

稱沖突集是極小沖突集(MCS)，當且僅當該沖突集的任意真子集都不是沖突集.

定理1[7].Δ是(SD,COMPS,OBS)的一個極小診斷，當且僅當Δ是(SD,COMPS，OBS)的極小沖突集的極小碰集.

1.2 SAT問題的相關定義

可滿足問題的一些基本定義如下：

定義3[21]. 文字.對于變量集合X={x1,x2,…,xn}，文字lj是變量xi或者它的否定-xi.

定義4[21]. 子句.子句Cj是文字lj的析取，Ci=l1∨l2∨…∨lm.

定義5[21]. 合取范式(conjunctive normal form, CNF). CNFC是子句的合取，C=C1∧C2∧…∧Ck.

定義6[21]. SAT問題的定義如下：對于n個布爾變量X={x1,x2,…,xn}，找到一組變量的賦值，滿足在各個子句中都存在一個文字取真，并且這組賦值使得所有的子句都能取真.若找到這樣的賦值，則稱該SAT問題是可滿足的(SAT)；如果沒有任何一組變量賦值使得SAT可滿足，則稱該SAT問題是不可滿足的(UNSAT).

2 集合極小化方法

集合極小化方法在模型診斷中有著舉足輕重的作用并且是必備的求解步驟.在模型診斷中的診斷解的求解過程中，其占據大部分求解時間.目前對該問題的求解策略還主要停留在求解效率和時間較為復雜的SSDM極小化策略，因此提出新的極小化策略會在很大程度上提高診斷求解時間和效率.本節提出DOEC極小化策略來進行極小化處理，該策略的優點是其求解復雜性和效率不會隨著要求解的問題的碰集個數增加而導致極小性判定時間急劇增加，而是只與待求解的初始極小沖突集合簇的大小相關.

2.1 相關定義

首先給出一些與極小化策略相關的定義.

定義7[10]. 設F是一個集合簇,F={S1,S2,…,Si,…,Sn},稱H為F的一個碰集(HS)，如果H滿足2個條件：

2) 對于任意一個Si∈F，都有HS∩S≠?.

稱F的一個碰集H為極小碰集(MHS)，當且僅當H的任意真子集都不是F的碰集.

定義8. 若num∈Si，則稱元素num覆蓋集合Si.元素num覆蓋集合Si記為Cover(num,Si)={num|num∈Si,num∈H}.含有元素num的碰集H和沖突集合Si取交集后共有的元素個數稱為元素num覆蓋集合Si的度，簡稱元素覆蓋集合度，記為DOEC(Cover(num,Si))={num|num∈(Si∩H)}.

定義9. 對于碰集H中的元素num，如果其覆蓋的所有的Si，均有DOEC(Cover(num,Si))≥2，則稱此num是該H的冗余元素.

根據以上定義，我們易得以下推論：

推論1. 如果碰集中不存在冗余元素，則該碰集是極小碰集.

證明. 假設極小碰集中存在冗余元素，則根據冗余元素定義，可知元素覆蓋的所有Si，均有DOEC(Cover(num,Si))≥2，即此元素所覆蓋的集合也被極小碰集中其他元素覆蓋，即當前極小碰集刪除此元素后仍為碰集，與極小碰集定義矛盾.

證畢.

針對上面的定義和推論，我們通過實例對提到的元素集合覆蓋度、冗余元素、碰集和極小碰集的概念進行進一步說明和闡述.

例1. 沖突集合簇CS={{2,4,5},{1,2,3},{1,3,5},{2,4,6},{2,4},{2,3,5},{1,6}}，要求求其所有極小碰集.首先要極小化，將CS中為某些沖突集合的超集的集合刪除，即刪除{2,4,5}和{2,4,6},因為它們是集合{2,4}的超集，這樣得到一個新的極小化的沖突集合簇CS={{1,6},{2,4},{1,2,3},{1,3,5},{2,3,5}}.通過去除超集，這樣可以減少方法處理的節點數目和沖突集的數量，從而進一步提高求解效率.該集合簇的所有的碰集為HS={{1,2},{1,3,4},{1,4,5},{2,3,6},{2,5,6},{2,3,4,5,6},{2,4,5,6},{3,4,6},{3,4,5,6}}.其中{2,3,4,5,6},{2,4,5,6},{3,4,5,6}為非極小碰集，其余的為極小碰集.

例如以是碰集但是是非極小碰集的{2,4,5,6}來說明解析，首先對該非極小碰集進行元素集合覆蓋度初始化并計算，計算的覆蓋度如下：{1,6}：1，{2,4}：2，{1,2,3}：1，{1,3,5}：1，{2,3,5}：2，然后對{2,4,5,6}的每個元素進行覆蓋度訪問.

對元素2來說，它覆蓋的集合有{2,4},{1,2,3},{2,3,5}其中{1,2,3}的覆蓋度為1小于2，所以元素2不是冗余元素，不能將其刪除；接著是4，它覆蓋的集合只有{2,4}且覆蓋度為2，所以根據冗余元素定義，其是冗余元素，可以將其刪除；接著是5，它覆蓋的集合有{1,3,5}：1，{2,3,5}：2，其中{1,3,5}的覆蓋度為1小于2，所以元素2不是冗余元素，不能將其刪除；最后是元素6，它覆蓋的集合有{1,6}且覆蓋度為1，所以不能將其刪除.所以將{2,4,5,6}中唯一的冗余元素4刪除之后，該碰集為極小碰集.

2.2節對結合元素覆蓋集合度的DOEC碰集極小化策略進行詳細介紹，然后在第4節對這2種極小化策略實驗結果進行比較.

2.2 結合DOEC的碰集極小化策略

本節將給出DOEC的極小化策略，該方法的主要思想是：檢查待檢測碰集中的每個元素的集合覆蓋情況，如果它覆蓋的所有原始沖突集合已經都被該碰集中的其他元素覆蓋過了，即它所覆蓋集合的覆蓋度均大于1，則該元素是冗余元素，可以將其刪除.不斷的繼續檢查碰集中的每個元素覆蓋集合的覆蓋度情況，直到被檢測的碰集的所有元素都被檢測完畢，剩下元素構成新的碰集一定是極小碰集.

算法1. DOEC.

輸入:HS={e1,e2,…,ei,…,en};

MHSs={MHS1,MHS2,…,MHSm};

輸出:極小化后的碰集HS.

①Covers?;

② for eachei∈MHSjdo

③Covers(MHSj)0;

④ end for

⑤ for eachei∈HSdo

⑥ if (ei∈MHSj) then

⑦Covers(MHSj)+ +;

⑧ end if

⑨ end for

該方法使用數組保存每個原始的極小沖突集合(MHSj)被當前HS中元素覆蓋的情況(行①～④)；對被檢測的HS中每個元素的集合覆蓋度進行統計，以便后續判斷該HS中該元素是否為冗余元素(行⑤～⑨)；然后對被檢測的HS中每個元素所覆蓋集合度的情況進行統計，根據不同的集合覆蓋度情況加以相應的處理(行⑩～).其中行～是對集合覆蓋度小于2的元素即非冗余元素進行跳過處理，行～是查找冗余元素并對其從當前待檢測碰集中執行刪除操作，行～是把對應的冗余元素的相應覆蓋的集合的覆蓋度進行更新操作，行是輸出碰集經過極小化方法后得到的極小碰集.

該方法和以前SSDM的極小化策略相比，其優點是碰集極小化判定時間不會隨著極小碰集個數的增加，極小化時間隨之急劇增加，而是只與輸入的極小沖突集合簇的大小有關，大大提高了極小化求解效率.實驗數據結果對比見4.1節.

3 利用SAT求解極小碰集的方法

3.1 將求解碰集問題轉換成SAT問題

本節將介紹如何將極小沖突集合簇轉換成CNF的形式.

要想把碰集問題轉換成SAT問題，首先是如何把要解決的集合形式化表示成SAT問題求解器能夠讀取和處理的CNF形式，實質上，只要把所有的沖突集合簇表示成CNF形式，然后把每個沖突集合中的元素用SAT中的文字來表示，每個沖突集合用一個子句來表示，舉例說明如下:

例2. 以極小沖突集合簇MCS={{1,6},{2,4},{1,2,3},{1,3,5},{2,3,5}}為例，介紹一下如何對極小沖突集合簇進行形式化表示，得到相對應的CNF文件描述.

沖突集合簇(MCS)形式化CNF描述如下：

① p cnf 6 5

② 1 6 0

③ 2 4 0

④ 1 2 3 0

⑤ 1 3 5 0

⑥ 2 3 5 0

上述CNF描述例子語法解釋如下：

行①中的“p cnf”是關鍵字，“6”代表集合變量元素的個數，“5”代表對應的極小沖突集合的個數.行②～⑥中每行是一個極小沖突集合，其中除0以外的數字代表極小沖突集合中存在的元素且均為正，每行的結尾數字0代表極小沖突集合結束符.

碰集的定義要求碰集覆蓋所有的極小沖突集合簇，此點和SAT問題中的所有的析取范式都必須為真然后構成一個合取范式為真是相同的.可見碰集問題和SAT問題的實質是集合覆蓋問題，只是有些概念的定義范圍略有不同，所以可以將一個碰集的求解問題轉化為SAT問題進行求解.

3.2 方法核心描述

首先簡單介紹一下隔離子句[21]，其定義是將可滿足性求解器所得到的解中所有變量的邏輯賦值取反，作為新的子句加入到SAT子句庫中.

例3. 如用可滿足性求解器得到一個解為

v1,-v2,v3,-v4.

上式表示，當變量v1,v3的邏輯取值為true(1),而變量v2,v4的邏輯取值為false(0)時，輸入的合取范式能夠被滿足.此時，我們將這些變量的邏輯值取反作為它們各自對應文字的邏輯符號，就構成了SAT求解器所需要的隔離子句：

-v1,v2,-v3,v4.

本文SAT-MHS方法法采用的是循環迭代求解方法，該方法主要思想是在調用SAT求解極小碰集的過程中，把之前每次求解的碰集極小化后取反添加到CNF中.屏蔽對該解和非極小解及部分無用搜索空間求解，達到縮減求解空間，提高求解效率.每次求解判斷是否為可滿足，當不可滿足則終止求解.

3.3 SAT-MHS方法實現

算法2. SAT-MHS.

輸入：CONFLICT={CF1,CF2,…,CFj,…,CFM};

輸出：MHSs.

①Trans_CNF(CONFLICT，CNFs);

② 初始化MarkUNSATISFIABLE；

③MarkIS_SATISFIABLE(CNFs);

④ if(Mark= =UNSATISFIABLE) then

⑤ return;

⑥ else

⑦ while (Mark==SATISFIABLE) do

⑧New_HS=Picosat_Sat(CNFs);

⑨ClauseIS_MHS(New_HS);

⑩MHSs←MHSs∪Clause;

算法2首先把輸入極小沖突集合簇轉化為SAT求解器能夠讀取的CNF文件(行①)，初始化可滿足性變量Mark(行②).然后首次調用SAT求解器對CNF文件進行可滿足性求解并對其值為不可滿足時則返回，結束算法(行③～⑤)；否則，把可滿足的賦值進行極小化處理得到的極小碰集添加到極小碰集集合簇中，并對求解的極小碰集以取反的隔離子句的形式添加到原始的CNF中，屏蔽掉該極小碰集對應的求解空間(行⑧～).最后對是可滿足的CNF不斷循環迭代的求解，直到得到不可滿足(行⑦～)，結束while循環并得到所有的極小碰集MHSs(行).

下面主要對SAT-MHS方法最關鍵的DOEC極小化策略舉例說明其應用效果.

對于例1中的沖突集合簇對應的HS，假設該方法當前得到碰集{2,3,4,5,6}，如果不使用DOEC極小化策略對其進行處理，而是直接以隔離子句形式將其加入到SAT的CNF文件中，則只是剪枝屏蔽掉了{1,2,3,4,5,6}這一個解，其剪枝效果如圖1(a)所示.但如果使用DOEC極小化策略對求解出碰集{2,3,4,5,6}進行極小化處理后得到極小碰集{3,4,6}，然后再把其以隔離子句的形式加入到SAT的CNF文件中，可以從圖1(b)中看出其把結點{3,4,6}所應的超集剪枝掉，從而有效地避免了對非碰集和非極小碰集的求解，減少調用SAT求解的次數，使方法更加高效.

4 實驗與結果

實驗所用的所有實驗用例均是隨機生成，輸入參數有元素個數n、集合簇中集合個數m以及元素在一個集合中出現的概率p.在同一個用例中，所有元素的p均相等，每個集合包含元素的平均個數約等于np.本文使用的實驗用例共有4組，分別為30,25,20,15.每組都是包含概率為p的用例，p為從0.05～0.94的19個概率分布數據，每組集合個數都是200.本文所有實驗數據均為使用相同參數下獨立生成的10個用例所得結果，然后對其取平均值.本文的實驗平臺均為：系統硬件配置是Intel Core I5-4590 CPU@3.30 Hz x4，8 GB RAM,C語言.

4.1 SSDM和DOEC極小化策略實驗結果分析比較

本節使用隨機生成測試用例的25和30這2組較難的包含概率為p的用例，p取值從0.20～0.80的14個概率分布數據進行實驗，實驗數據均為使用相同參數下獨立生成的10個用例以SAT-MHS方法為基礎進行實驗所得結果并對其實驗結果取平均值，詳細如表1所示.

從表1可以看出,對于元素個數N=25的測試用例，DOEC極小化策略是SSDM極小化策略求解速度的1～40.3倍;而對于N=30的測試用例，DOEC極小化策略是SSDM極小化策略求解速度的21～55.1倍之間，可見DOEC極小化策略對于較大規模測試用例的高效性.除此之外，DOEC極小化策略會隨著碰集個數的增多和元素個數的增多，

Fig. 2 The performance comparison of SAT-MHS and Boolean圖2 SAT-MHS方法與Boolean方法實驗結果比較

其求解的效率也會隨之增加.所以，DOEC極小化策略會隨著待求解問題規模的增大，其求解效率也會隨之增加.

4.2 SAT-MHS方法與Boolean方法對比分析

本節使用SAT-MHS方法與目前求解效率較高的Boolean方法進行比較，并給出2種方法在隨機生成測試用例的實驗結果.

從圖2中可以看出，對于元素個數m=15的測試用例，因其碰集個數和元素個數較少，所以其求解耗時較少，但SAT-MHS方法還是略比Boolean方法用時少.對于元素個數較多的用例m=20,25,30,SAT-MHS方法的優勢就較為明顯.隨著所要求解的極小碰集的個數不斷增加，SAT-MHS方法的優勢越來越明顯，求解時間的差距也越來越大，所以對于碰集個數較大的問題其擁有較大優勢.尤其對于耗時較長的用例來說，SAT-MHS的求解效率為Boolean方法的30倍左右.不難發現，對比Boolean方法，SAT-MHS方法在耗時越長的測試用例中其優勢越明顯.

從圖3可以看出，對于所需求解的極小碰集的個數較少的測試用例，當兩者的求解時間在10-3s以下，SAT-MHS方法的求解時間大于Boolean方法,因為調用SAT求解器需要一些初始化時間;但隨著求解規模的增大，當求解時間在10-3～10-2s之間時，可以看出兩者的求解時間逐漸接近；當求解時間在10-2～100s之間，SAT-MHS方法的求解效率明顯是Boolean方法的3～7倍之間；當求解時間在100～102s之間，其求解效率甚至高達10～20倍；當求解時間在102～104s之間，SAT-MHS方法的求解效率基本是Boolean方法的10倍以上.綜合對比圖2和圖3可以看出，SAT-MHS方法與Boolean方法相比，在求解極小碰集的規模大及復雜性高的問題，其基本求解效率在10倍以上.

Fig. 3 The comparison results of efficiency between SAT-MHS and Boolean 圖3 SAT-MHS方法與Boolean方法實驗求解效率比較

此外，從圖3可以看出，在求解小規模問題時，Boolean沒有初始化過程，而SAT-MHS求解時需要初始化，因此其求解時間比Boolean多些.但當問題規模越大時，產生的碰集個數增多，需要花費大量的時間處理極小化問題，可見SAT-MHS更有優勢.

5 總 結

極小碰集在現實生活中有重要的實際應用價值，目前主流完備的碰集極小化策略是SSDM，但其不足是其極小化效率會隨著極小碰集的數量增加而使極小化的耗時也隨之急劇增多.通過把碰集求解問題轉化為SAT問題，然后在DOEC極小化策略的基礎上提出了一種新的碰集求解方法SAT-MHS.該極小化策略極小化耗時和已求得的極小碰集規模脫離關系，只與最初的極小沖突集合簇的大小有關，不會隨著求解的極小碰集數量的增加而迅速增加.

SAT-MHS方法把極小沖突集合簇轉化為SAT求解器能處理的CNF文件，并調用較為成熟的SAT求解器進行循環迭代的碰集求解；每次可滿足的文字變量賦值就是SAT求解器求解得到的一個碰集.然后對得到的非極小碰集用DOEC極小化策略進行極小化，并把處理得到的極小碰集以隔離子句的形式添加到CNF文件中，從而屏蔽待搜索求解空間，提高求解效率.與目前求解效率較高的Boolean方法相比，可以看到該方法的高效性，尤其對求解問題規模和碰集個數較多的問題實例，該方法的求解效率至少在10倍以上.未來的工作是使用啟發式求解策略[22-24]求解更大規模的極小碰集問題.

[1]Console L, Dressler O. Model-based diagnosis in the real world: Lessons learned and challenges remaining[C]Proc of the 16th Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 1999: 1393-1400

[2]Struss P. Knowledge-based diagnosis: An important challenge and touchstone for AI[C]Proc of the 10th European Conf on Artificial Intelligence. New York: John Wiley & Sons, 1992: 863-873

[3]Hamscher W. Readings in model-based diagnosis[OL]. 1992 [2017-06-17]. http:www.citeulike.orggroup14148article8042710

[4]De Kleer J. Diagnosing multiple persistent and intermittent faults[C]Proc of the 21st Int Joint Conf on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2009: 733-738

[5]Wang Yiyuan, Yin Minghao, Ouyang Dantong, et al. A novel local search algorithm with configuration checking and scoring mechanism for the setk-covering problem[J]. Int Trans in Operational Research, 2017, 24(6): 1463-1485

[6]Wang Yiyuan,Ouyang Dantong, Zhang Liming, et al. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity[J]. Science China Information Sciences, 2017, 60(6): 062103

[7]Reiter R. A theory of diagnosis from first principles[J]. Artificial Intelligence, 1987, 32(1): 57-95

[8]Greiner R, Smith B A, Wilkerson R W. A correction to the algorithm in Reiter’s theory of diagnosis[J]. Artificial Intelligence, 1989, 41(1): 79-88

[9]Wotawa F. A variant of Reiter’s hitting-set algorithm[J]. Information Processing Letters, 2001, 79(1): 45-51

[10]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)

[11]Ouyang Dantong, Ouyang Jihong, Cheng Xiaochun, et al. A method of computing hitting set in model-based diagnosis[J]. Chinese Journal of Science Instrument, 2004, 25(4): 605-608 (in Chinese)(歐陽丹彤, 歐陽繼紅, 程曉春, 等. 基于模型診斷中計算碰集的方法[J]. 儀器儀表學報, 2004, 25(4): 605-608)

[12]Zhao Xiangfu, Ouyang Dantong. A method of combing SE-Tree to compute all minimal hitting sets[J]. Progress in Natural Science, 2006, 16(2): 169-174

[13]Chen Xiaomei, Meng Xiaofeng. Qiao Renxiao. Method of computing all minimal hitting set based on BNB-HSSE[J]. Chinese Journal of Science Instrument, 2010, 31(1): 61-67 (in Chinese)(陳曉梅, 孟曉風, 喬仁曉. 基于BNB-HSSE計算全體碰集的方法[J]. 儀器儀表學報, 2010, 31(1): 61-67)

[14]Zhang Liming, Ouyang Dantong, Zeng Hailin. Computing the minimal hitting set based on dynamic maximum degree[J]. Journal of Computer Reach and Development, 2011, 48(2): 209-215 (in Chinese)(張立明, 歐陽丹彤, 曾海林. 基于動態極大度的極小碰集求解方法[J]. 計算機研究與發展, 2011, 48(2): 209-215)

[15]Pill I, Quaritsch T. Optimizations for the Boolean approach to computing minimal hitting sets[C]Proc of the 20th European Conf on Artificial Intelligence. Amsterdam: IOS Press, 2012: 648-653

[16]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)

[17]Yang Kun, Bai Hongjun, Ouyang Qi, et al. Finding multiple target optimal intervention in disease-related molecular network[J]. Molecular Systems Biology, 2008, 4(1): 228

[18]Zhou Gan, Feng Wenquan, Jiang Bofeng, et al. Computing minimal hitting set based on immune genetic algorithm[J]. Int Journal of Modelling, Identification and Control, 2014, 21(1): 93-100

[19]Jannach D, Schmitz T, Shchekotykhin K. Parallelized hitting set computation for model-based diagnosis[C]Proc of the 24th AAAI Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2015: 1503-1510

[20]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal hitting sets based on join relation[J]. IEEE Trans on Systems, Man, and Cybernetics: Systems, 2015, 45(7): 1063-1076

[21]McMillan K L. Applying SAT methods in unbounded symbolic model checking[C]Proc of Conf on Computer Aided Verification. Berlin: Springer, 2002: 250-264

[22]Wang Yiyuan, Cai Shaowei, Yin Minghao. Local search for minimum weight dominating set with two-level configuration checking and frequency based scoring function[J]. Journal of Artificial Intelligence Research, 2017, 58(1): 267-295

[23]Wang Yiyuan, Cai Shaowei, Yin Minghao. Two efficient local search algorithms for maximum weight clique problem[C]Proc of the 13th AAAI Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2016: 805-811

WangRongquan, born in 1992. Master candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning.

OuyangDantong, 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).

WangYiyuan, born in 1988. PhD candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning (yiyuanwangjlu@126.com).

LiuSiguang, born in 1988. Master candidate at Jilin University.His main research interests include model-based diagnosis,SAT problem and automated reasoning (lsgmliss@163.com).

ZhangLiming, born in 1980. PhD, post-doctor in Jilin University. His main research interests include model-based diagnosis,SAT problem and automated reasoning.