結(jié)合互補度的基于擴展規(guī)則#SAT問題求解方法

歐陽丹彤　賈鳳雨　劉思光　張立明

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

?

結(jié)合互補度的基于擴展規(guī)則#SAT問題求解方法

歐陽丹彤賈鳳雨劉思光張立明

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

(ouyd@jlu.edu.cn)

摘要#SAT問題又稱模型計數(shù)(model counting)問題是人工智能領(lǐng)域的研究熱點之一，在人工智能領(lǐng)域被廣泛應(yīng)用.在對基于擴展規(guī)則的#SAT問題求解方法CER(counting models using extension rules)深入研究的基礎(chǔ)上，提出一種結(jié)合互補度的#SAT問題求解方法.在計算給定子句集的模型個數(shù)時，利用SE-Tree(set enumeration tree)形式化地表達計算過程，逐步生成需要計算的子句集合，并在SE-Tree中添加終止結(jié)點，避免大部分含互補文字子句集合的生成，且不會因剪枝而導(dǎo)致求解不完備.提出互補度的概念，在擴展SE-Tree結(jié)點時按照互補度由大到小的順序擴展，較早地生成含互補文字且長度較小的子句集合，有效減少枚舉樹生成的結(jié)點個數(shù)，進而減少對子句集合判斷是否含互補文字的計算次數(shù).實驗結(jié)果表明：與CER方法相比該方法效率較好，且進一步改進了CER方法在互補因子較低時求解效率低下的不足.

關(guān)鍵詞擴展規(guī)則；模型計數(shù)；CER方法；互補度；集合枚舉樹

命題可滿足問題(propositional satisfiability problem, SAT)是人工智能領(lǐng)域中關(guān)鍵研究問題，有著相當(dāng)廣泛的應(yīng)用，如在智能規(guī)劃領(lǐng)域?qū)⒁?guī)劃問題編譯成SAT問題進行求解[1]，同樣地其還被應(yīng)用于求解基于模型的診斷問題[2]以及模型檢測問題中[3].迄今為止，國內(nèi)外學(xué)者已對求解SAT問題的方法做了許多研究和改進[4-7].對SAT問題的求解算法主要分為基于DP(Davis-Putnam)[8]的完備性算法和基于局部搜索的非完備性算法.完備性算法雖然可以準確判定任意命題公式的可滿足性，但隨著問題規(guī)模的增大，求解時間也會隨之以指數(shù)級增加，其不適合于大規(guī)模的SAT問題求解.基于局部搜索的非完備性算法雖然不能判定命題公式不可滿足，但在可滿足的SAT問題中可以快速地得到一個解，對于大規(guī)模問題也有較好效率，因此近年來獲得了許多研究人員的關(guān)注.但對于局部搜索算法都面臨著一個共同的問題，即陷入局部最優(yōu).格局檢測策略(configuration checking)[9-10]可以有效地解決局部最優(yōu)問題，并且廣泛應(yīng)用于局部搜索算法中.

實際上，大部分計算復(fù)雜性是NP完全的問題，都可以在多項式時間內(nèi)轉(zhuǎn)化成SAT問題來求解，然而在人工智能領(lǐng)域存在著許多復(fù)雜性高于NP完全的問題，例如貝葉斯推理、概率規(guī)劃等問題[11-13]在轉(zhuǎn)換成命題公式后，只判斷是否可滿足是不夠的，還需要計算命題公式模型(可滿足賦值)的個數(shù).#SAT問題即是這樣的一類問題.它是SAT問題的重要擴展，需要計算出給定命題公式所有模型的個數(shù)，計算復(fù)雜性是#P完全的[14-15].如何高效求解#SAT問題對人工智能的很多領(lǐng)域都有深遠意義.

#SAT問題一直備受廣大研究人員的關(guān)注.1999年，Birnbaum和Lozinskii[16]提出一種基于DP過程的模型計數(shù)求解方法，稱為CDP(counting models using Davis-Putnam procedure)算法.在CDP算法的求解過程中，對具有n個布爾變量的搜索樹進行完全搜索，如果在搜索樹的某個分支上存在不滿足的子句則放棄這個分支的搜索，對其剪枝；否則，記錄該分支的所有可滿足賦值個數(shù).目前，許多求解#SAT問題的算法都是以CDP算法為基礎(chǔ)的.2000年，Bayardo和Pehoushek[17]將組件的思想加入到#SAT問題的求解中，將命題公式轉(zhuǎn)換成約束圖的形式來表示：圖中的頂點為出現(xiàn)在公式中的變量，若2個變量出現(xiàn)在同一子句中，則在圖中代表這2個變量的頂點之間就存在一條邊.通過這種方式可以將命題公式分解為多個不相關(guān)的子公式，并對這些子公式分別進行求解.然而，在求解各子公式過程中，可能出現(xiàn)之前已經(jīng)計算過的子公式，如果能在第1次計算時將結(jié)果記錄下來，則在后續(xù)的求解過程中遇到相同的子公式，可以直接使用已經(jīng)記錄的結(jié)果，避免重復(fù)計算.基于此，Bacchus等人[18]將高速緩存技術(shù)引入到了#SAT問題求解中提高了求解效率.Sang等人[19]提出的Cachet方法同時使用了組件緩存和子句學(xué)習(xí)2種策略.此后Davies和Bacchus[20]在搜索樹的每個結(jié)點加入更多的推理，如超二元歸結(jié)和等式約簡，使得求解效率有了很大提升.Darwiche[21]利用知識編譯的方法來求解#SAT問題，將CNF(conjunctive normal form)公式轉(zhuǎn)化成可分解的、確定的d-DNNF(deterministic,decomposable negation normal form)公式來求解模型個數(shù).以上的算法都是完備性算法，即可以得到精確的模型個數(shù).在#SAT問題求解算法中還存在著一類近似求解的非完備性算法.近似算法主要是基于采樣的思想，如ApproxCount算法[22].該方法從原公式選取若干變量組成子空間，并求出該空間精確模型個數(shù)，然后通過采樣得出總模型個數(shù)與子空間模型個數(shù)的近似比例，根據(jù)此比例和子空間的精確模型個數(shù)求出原公式總模型個數(shù)近似解.雖然近似算法在大規(guī)模問題中有著較好效率，但在許多情況下，需要知道問題的精確模型個數(shù)，必須通過完備算法進行求解.甚至，在ApproxCount算法近似求解的過程中，也需要通過精確算法求出子空間的模型個數(shù).因此，對#SAT問題的完備性算法研究有著重要意義.

以上求解#SAT問題的完備性方法基本上都是以歸結(jié)原理為基礎(chǔ)推理方法的.歸結(jié)原理的基本思想是通過推出空子句的方法來判定給定子句集的不可滿足性.然而，與歸結(jié)方法相反，擴展規(guī)則方法通過推出所有極大項組成的集合判定給定子句集的不可滿足性[23].基于擴展規(guī)則的定理證明方法已經(jīng)得到了許多相關(guān)研究人員的重視,如將擴展規(guī)則改進應(yīng)用到模態(tài)邏輯的自動定理證明中[24]；結(jié)合擴展規(guī)則的知識編譯方法[25]；對基于擴展規(guī)則方法進行改進提出NER,SER,IBOHMH_IER等系列算法[26-28].殷明浩等人[29]提出基于擴展規(guī)則求解#SAT問題的CER(counting models using extension rules)方法.與其他的#SAT求解方法需找出哪些賦值是給定子句集的模型不同，該方法需找出不是子句集模型的賦值，可以看作是基于歸結(jié)的求解#SAT問題方法的一種補方法.CER方法的基本思想是計算給定子句集所能擴展出的所有極大項個數(shù)，進而得出模型個數(shù).這種求解模型計數(shù)的方法受到原子句集中互補對個數(shù)的影響，當(dāng)互補對個數(shù)較多時該方法一般要優(yōu)于基于歸結(jié)的方法，反之當(dāng)互補對個數(shù)較少時要差于基于歸結(jié)的方法.

本文在充分吸收國內(nèi)外研究成果的基礎(chǔ)上，分析基于擴展規(guī)則的求解#SAT問題CER方法的優(yōu)勢與不足，對其進行改進，提出一種基于極大互補度的模型計數(shù)新方法，結(jié)合帶有終止結(jié)點的集合枚舉樹(set enumeration tree, SE-Tree)形式化地表達求解過程，逐步計算給定子句集所能擴展的極大項個數(shù)，避免了大部分“無用”結(jié)點的生成，從而提高求解效率.

1擴展規(guī)則

本節(jié)將主要介紹擴展規(guī)則及其相關(guān)概念和定理.首先對在本文中使用的一些符號做出如下規(guī)定：xi(i=1,2,…,m)表示布爾變量；X={x1,x2,…,xm}表示變量集合；用li表示文字，分為正文字和負文字，xi表示變量xi的正文字，xi表示變量xi的負文字；Ci(i=1,2,…,n)表示子句，由文字的析取構(gòu)成，可將其看成是文字的集合；Φ，Φ′表示CNF公式，由子句的合取構(gòu)成，可將其看成是子句的集合.

擴展規(guī)則是與歸結(jié)原理“互補”的推理規(guī)則，其定義如下：

定義1[23].對于一個給定的子句C和一個布爾變量集合X，子句C中出現(xiàn)的變量包含于變量集合X中，則有子句集合D={C∨x,C∨x|x∈X并且x的正負文字都不出現(xiàn)在子句C中}，將C到D中元素的推導(dǎo)過程叫作擴展規(guī)則，D中的元素叫作子句C應(yīng)用擴展規(guī)則的結(jié)果.

例1. 給定子句C=x1∨x2∨x3與變量集合X={x1,x2,x3,x4}，則D={x1∨x2∨x3∨x4,x1∨x2∨x3∨x4}就是子句C應(yīng)用擴展規(guī)則后的結(jié)果.

定理1[23].子句C與其應(yīng)用擴展規(guī)則后的結(jié)果D是等價的.

由擴展規(guī)則及定理1可知，一個子句可以被擴展成一個與其等價的子句集.那么，可以對給定子句集中的所有子句應(yīng)用擴展規(guī)則，從而得到一個與原子句集等價的新子句集.

定義2[29].一個非重言式子句是變量集合X上的極大項當(dāng)且僅當(dāng)它包含集合X中的所有變量的正文字或其負文字.

若對一個子句不斷應(yīng)用擴展規(guī)則，最終將得到一個僅由極大項構(gòu)成的子句集.由極大項性質(zhì)可知，對于一個變量集合上的每個極大項來說，在全部賦值空間中有且僅有一個賦值使得其為假，并且一個賦值能且只能使一個極大項為假.這就使得極大項與賦值之間有一個一一對應(yīng)的關(guān)系.

2CER方法

假設(shè)給定一個只包含極大項的子句集合Φ，且極大項C包含在子句集Φ中，由于極大項與唯一的一個賦值對應(yīng)，且使其為假，規(guī)定使極大項C為假的賦值為I，那么賦值I也一定使子句集為假.即子句集Φ中包含多少個極大項，就會有多少個賦值使其為假，反之，其不包含的極大項數(shù)目就是模型個數(shù).由此給出如下定理：

定理2[29].給定一個子句集Φ，其中所有變量集合是X，且Φ中所有子句都是X上的極大項，那么子句集Φ的模型個數(shù)為2|X|-|Φ|，其中|X|表示集合X中變量個數(shù)，|Φ|表示子句集Φ中子句個數(shù).

特殊地，當(dāng)只包含極大項的子句集Φ不可滿足時，模型個數(shù)2|X|-|Φ|=0，即Φ中包含所有的2|X|個極大項.

由擴展規(guī)則可知，一個子句集可以擴展成只包含極大項的集合，如此，再利用定理2即可計算出子句集的模型個數(shù).然而，直接用擴展規(guī)則將子句集擴展成只包含極大項的形式是不明智的，實際上，只需要知道子句集能擴展出的極大項個數(shù)即可計算出子句集的模型個數(shù)，然而，子句集中所有子句擴展出的極大項集合的并集就是子句集能擴展出的極大項集合，即S=|P1∪P2∪…∪Pn|，其中S表示子句集Φ={C1,C2,…,Cn}可擴展出的極大項個數(shù)，Pi表示子句Ci可擴展出的極大項集合，其中i=1,2,…,n.

定理3[23].2個子句擴展出的極大項集合不含交集當(dāng)且僅當(dāng)這2個子句含有互補文字.

結(jié)合包含排斥原理[30]可以得到式(1)來計算子句集所能擴展出的極大項個數(shù)，詳情可參照文獻[23].

(-1)n-1|P1∩P2∩…∩Pn|,

(1)

其中,

S表示子句集Φ={C1,C2,…,Cn}可擴展出的極大項個數(shù)，X為變量集合.Pi表示子句Ci可擴展出的極大項集合，i=1,2,…,n.在CER方法中，首先通過式(1)計算出給定子句集可擴展出的極大項個數(shù)S，再由定理2即可得到子句集的模型個數(shù)2|X|-S.

從式(1)容易看出，當(dāng)含有互補文字的子句對較多時，式(1)中的值為0的項就較多，顯然這些項不用計算，因此算法的效率就較高.為了權(quán)衡子句集中這樣的含有互補文字的子句對的多少，引入互補因子的概念如下：

定義3[23].給定一個子句集Φ={C1,C2,…,Cn}，Φ的互補因子(complementary factor)是含有互補文字的子句對個數(shù)與所有子句對個數(shù)之比，即T(n(n-1)2)，其中T表示含互補文字的子句對個數(shù).

CER方法受互補因子的影響，當(dāng)互補因子較高時算法效率較高，當(dāng)互補因子降低時算法效率也會隨之降低.但是，CER方法中簡單地利用式(1)按照分層計算的方式，并沒有很好地利用子句間含有互補文字的情況來簡化計算過程.基于此，本文對其進行改進，提出了基于互補度的求解方法.

3結(jié)合互補度的求解方法

在給出基于互補度的求解方法之前，下面先給出互補度定義及其相關(guān)概念.

3.1互補度概念

定義4. 給定子句集Φ，C∈Φ，則稱子句集Φ中與子句C含有互補文字的子句個數(shù)為子句C的互補度，記為Com_D(C,Φ).

例2. 給定子句集Φ={x1∨x2∨x3,x1∨x3,x1∨x2},子句集Φ中子句x1∨x2∨x3的度為Com_D(x1∨x2∨x3,Φ)=2，同樣地,Com_D(x1∨x3,Φ)=1，Com_D(x1∨x2,Φ)=1.

命題1. 給定子句集Φ，若Φ的一個子集Φ′中子句所擴展出的極大項集合交集為空，則任何Φ′的超集中子句擴展出的極大項集合的交集也為空.

命題2. 給定子句集Φ，若Φ的一個子集Φ′的互補度Com_D(Φ′,Φ)=0，則Φ′中必不含有互補文字.

顯然，對含有互補文字的子句子集及其超集對應(yīng)的式(1)中計算項是沒有必要求值的.那么，若可以提前找到含互補文字的最小子句集(即不是任何含有互補文字的子句集的超集)并忽略掉它的超集，則可避免對這些超集判斷是否含互補文字的計算.基于此，提出一種結(jié)合SE-Tree的基于互補度的#SAT求解方法.

3.2CDCER(complementary-degree-based CER)

方法

SE-Tree是由Rymon[31]提出的一種用于列舉一個集合的冪集中元素的樹型數(shù)據(jù)結(jié)構(gòu)：一個完全的SE-Tree按照一定的順序(如數(shù)字、字母順序等)可以列舉出一個集合的冪集中所有的元素集合.如一個包含4個子句的子句集Φ={C1,C2,C3,C4}，它的完全集合枚舉樹如圖1所示:

Fig. 1　The SE-Tree of {C1,C2,C3,C4}.圖1　子句集{C1,C2,C3,C4}的完全集合枚舉樹

CER方法中，求解子句集Φ={C1,C2,…,Cn}的模型個數(shù)即為計算式(2)的值：

(2)

式(2)中每一項都與子句集Φ的一個子集相對應(yīng)，如|Pi∩Pj∩…∩Pk|是子句集{Ci,Cj,…,Ck}中子句擴展出的極大項集合交集的大小.特殊地，2|X|與空子集相對應(yīng).式(2)中每一項都與子句集Φ的SE-Tree中結(jié)點對應(yīng).

CDCER方法的基本思想如下：使用SE-Tree按照集合長度由小到大的順序逐步生成給定子句集的子集，計算每個結(jié)點的子結(jié)點互補度，按照互補度由大到小的順序生成子結(jié)點.判斷結(jié)點子句集中是否含有互補文字，如果有則對枚舉樹剪枝；否則統(tǒng)計結(jié)點中文字個數(shù)W，計算2|X|-W，將結(jié)果進行累加(或累減)，并將這樣生成的樹記為CDSE-Tree(complementary-degree-based SE-Tree).

例3. 給定子句集Φ={C1,C2,C3,C4}，其中含有互補文字的子句對有(C1,C4),(C2,C4),(C2,C3),(C3,C4)，即Com_D(C1,Φ)=1，Com_D(C2,Φ)=2，Com_D(C3,Φ)=2，Com_D(C4,Φ)=3.未結(jié)合互補度進行剪枝生成的SE-Tree如圖2(a)所示，SE-Tree生成13個結(jié)點，其中2個結(jié)點被剪枝；按照互補度由大到小順序生成的CDSE-Tree如圖2(b)所示，CDSE-Tree生成10個結(jié)點，其中3個結(jié)點被剪枝；相比沒有加入互補度的SE-Tree，CDSE-Tree中剪掉了更多冗余結(jié)點.

Fig. 2　Comparison of SE-Tree and CDSE-Tree of {C1,C2,C3,C4}.圖2　子句集{C1,C2,C3,C4}的SE-Tree與CDSE-Tree比較

基于互補度的CDCER方法通過CDSE-Tree描述計算過程，可以避免更多值為0的冗余的計算項生成，減少對相應(yīng)子句集判斷是否含有互補文字的計算，從而提高了算法的求解效率.具體算法如下：

算法1. CDCER(Φ,X).

輸入：子句集Φ、變量集合X；

輸出：子句集Φ的模型個數(shù).

①num_model=0;

②Node←?;

③ For (當(dāng)前互補度最大的結(jié)點Node)

④ Begin

⑤ If (Com_D(Node,Φ)=-1)

⑥ Break;

⑦ EndIf

⑧ If(Com_D(Node,Φ)>0并且Node中有互補文字)

⑨Com_D(Node,Φ)=-1;

⑩ Continue;

算法1開始時，當(dāng)前結(jié)點為根結(jié)點，即空集.若當(dāng)前結(jié)點含有互補文字，則直接將其互補度置為-1并剪枝，繼續(xù)找互補度最大的結(jié)點.否則，計算結(jié)點中子句能擴展出的極大項集合交集的大小，結(jié)點在偶數(shù)層(其中有偶數(shù)個子句)則將結(jié)果累加，在奇數(shù)層則累減.然后，將結(jié)點互補度置為-1，并擴展其子結(jié)點.若當(dāng)前結(jié)點中互補度最大為-1，則表示CDSE-Tree中所有“有效”結(jié)點已經(jīng)擴展完.由命題2可知，若當(dāng)前結(jié)點中互補度最大為0，如根結(jié)點，則結(jié)點中必沒有互補文字，可直接對其計算無需判斷是否含有互補文字.

下面從理論上對算法1做相應(yīng)分析：

1) 修剪規(guī)則的正確性.在CDCER方法中，對每一個已經(jīng)產(chǎn)生的結(jié)點子句集(除根結(jié)點)都需要判定結(jié)點中是否包含互補文字，即結(jié)點中是否包含一對含有互補文字的子句.若包含，則由定理3可知，結(jié)點中子句擴展出的極大項集合的交集為空集，在式(2)中此結(jié)點相對應(yīng)的計算項值為0，那么不對此計算項進行求解也不會影響求解結(jié)果.在CDCER方法中對此類結(jié)點進行剪枝.若結(jié)點不包含互補文字，則結(jié)點中子句擴展出的極大項集合的交集為非空集合，需要對其進行相應(yīng)求值計算.由命題1可知，若子句集中含有互補文字，則其任意超集中子句擴展出的極大項集合的交集必為空集.然而在CDSE-Tree中，一個結(jié)點的所有子孫結(jié)點都是該結(jié)點的超集，那么若當(dāng)前結(jié)點中含有互補文字，結(jié)點計算結(jié)果為0，則其子孫結(jié)點也必是包含互補文字的冗余結(jié)點，不需要對它們進行求解，對這樣的結(jié)點剪枝將不會影響求解結(jié)果，保證了修剪規(guī)則的正確性.

2) 完備性.一個完全的SE-Tree能夠按照某種預(yù)定的順序枚舉出一個集合的所有子集，CDCER方法結(jié)合SE-Tree按照集合長度由小到大和互補度由大到小的順序逐步生成給定子句集的子集.若不存在剪枝的情況，那么最后生成的完全CDSE-Tree將枚舉出給定子句集的所有子集.由包含排斥原理的知識可知，式(2)中所有計算項與給定子句集的所有子集是一一對應(yīng)的關(guān)系.然而CDCER方法中的剪枝規(guī)則只是修剪掉了CDSE-Tree中的冗余結(jié)點，即在式(2)中相應(yīng)地去掉值為0的計算項，并不會對求解結(jié)果的正確性產(chǎn)生影響.所以CDCER方法必將求解出全部的模型個數(shù).

以上部分給出了本文提出的基于互補度的#SAT求解方法CDCER方法，并用SE-Tree描述算法求解過程；CDCER方法減少了判斷子句間是否含有互補文字的計算，從而提高了算法的效率.

4實驗結(jié)果分析

本節(jié)給出CDCER方法在隨機問題上的實驗測試結(jié)果，并將其與CER方法進行比較.實驗平臺如下: Windows XP操作系統(tǒng),CPU AMD AthlonTM64 X2 Dual Core Processor 3600+ 1.9 GHz,2.00 GB RAM.

之所以選擇隨機問題是為了方便控制生成用例的類型，如互補因子.實驗用例由隨機生成器產(chǎn)生,其輸入?yún)?shù)有變量個數(shù)m、子句個數(shù)n以及變量在各子句中的出現(xiàn)概率p,每個子句都按一定概率p從m個變量中選取變量,因變量的正負文字相對于子句集來說是對稱的,所以這里只控制變量為正的概率p′,p′范圍是(0.1,0.5).本文的實驗數(shù)據(jù)采用變量個數(shù)為30、子句個數(shù)為100的隨機樣例進行實驗測試.通過限定變量在子句中出現(xiàn)概率并結(jié)合其正文字出現(xiàn)概率來限定子句集中子句的平均子句長度以及互補因子的大小,實驗測試互補因子范圍為0.1～0.9,實驗結(jié)果是10次實驗的平均結(jié)果.CER與CDCER方法對于隨機問題的實驗結(jié)果如表1所示.

表1給出了2種方法對于各測試用例的求解時間及兩者時間差(CER方法的求解時間減去CDCER方法的求解時間)、求解過程中需要擴展的結(jié)點數(shù)(需生成的子句集合數(shù))及其差值(CER方法需擴展的結(jié)點數(shù)量減去CDCER方法的結(jié)點數(shù))，時間單位為s.從表1的結(jié)果可以看出，隨著互補因子的增大，2種方法的求解時間都相對減少，且CDCER方法的求解效率普遍要優(yōu)于CER方法.這是因為一般情況下CDCER方法與CER方法中所需擴展的結(jié)點數(shù)的差值較大，而CDCER方法恰恰節(jié)省了對這些CER方法中多擴展出的結(jié)點判斷是否含有互補文字的時間，所以效率一般要優(yōu)于CER方法.

Table 1　The Comparison of Running Time Cost in CER and CDCER

Note: Each instance contains 30 variables and 100 clauses.

Fig. 3　Comparison of number of nodes extended in CER and CDCER.圖3　CER和CDCER方法運行過程中擴展結(jié)點數(shù)對比圖

此外，隨著互補因子的增大，2種方法需要擴展的結(jié)點數(shù)量都相對減少，并且兩者的差值也隨之減小.而相比CER方法，CDCER方法求解時間降低的多少與結(jié)點數(shù)量差值大小有著直接關(guān)系，隨著差值減小，2種方法的時間差也隨之減少.在互補因子很高的特殊情況下，如表1中測試用例R9，CER方法中需要擴展的結(jié)點數(shù)很少，CDCER方法與CER方法需擴展的結(jié)點數(shù)差值較小.此時，CDCER方法對子句互補度的計算抵消了由結(jié)點數(shù)減少帶來的效率提升，故其效率低于CER方法.但在這種特殊情況下CER方法求解時間已經(jīng)很少，算法效率的提升空間已經(jīng)很小，而CDCER方法的求解效率也較高.下面給出2種方法求解過程中擴展結(jié)點數(shù)的對比，如圖3所示：

圖3中散點表示測試用例，是隨機生成的變量數(shù)為30、子句個數(shù)為100的50個隨機測試用例.橫豎坐標分別表示CDCER和CER兩種方法運行過程中擴展的結(jié)點數(shù).從圖3可以看出，對于所有測試用例CDCER方法求解過程中生成的結(jié)點都遠少于CER方法.對于大部分測試用例CER方法求解過程中擴展的結(jié)點數(shù)是CDCER方法中結(jié)點數(shù)的3～4倍(圖3中大部分散點落于3倍線，甚至4倍線之上)，甚至更高.相對于CER方法，CDCER方法運行過程中擴展的結(jié)點數(shù)減少的越多，其效率提升也就越高.

5結(jié)束語

許多學(xué)者對#SAT問題的求解方法進行了研究.在CER方法中，利用擴展規(guī)則方法求出給定子句集所能擴展出的極大項個數(shù)，從而得到不能擴展出的極大項個數(shù)，得出求解結(jié)果.當(dāng)互補因子較高時，基于擴展規(guī)則的方法一般要優(yōu)于基于歸結(jié)的方法；反之，當(dāng)互補因子較低時，基于擴展規(guī)則的方法要差于基于歸結(jié)的方法.針對此問題本文基于CER方法提出了求解#SAT的CDCER方法，在互補因子較低時較大程度地提高了求解效率.該方法結(jié)合SE-Tree形式化描述求解過程，易于理解且編程簡單，實現(xiàn)時并不用構(gòu)造樹.在枚舉樹生成結(jié)點時，按照結(jié)點的互補度由大到小的順序生成結(jié)點，盡可能早地生成含有互補文字的結(jié)點，有效地減少了枚舉樹中擴展出的冗余結(jié)點個數(shù)，避免了對大部分冗余結(jié)點是否含有互補文字的判斷.還給出了CDCER方法的正確性和完備性證明，實驗結(jié)果表明該方法效率較高.

致謝全體作者對本文所有匿名審稿人的辛勤工作和提出的寶貴意見表示真摯感謝！

參考文獻

[1]Rintanen J. Planning as satisfiability: Heuristics[J]. Artificial Intelligence, 2012, 193: 45-86

[2]Grastien A, Anbulagan A. Diagnosis of discrete event systems using satisfiability algorithms: A theoretical and empirical study[J]. IEEE Trans on Automatic Control, 2013, 58(12): 3070-3083

[3]Biere A, Cimatti A, Clarke E M, et al. Symbolic model checking using SAT procedures instead of BDDs[C]Proc of the 36th Annual ACMIEEE Design Automation Conf. New York: ACM, 1999: 317-320

[4]Monasson R, Zecchina R, Kirkpatrick S, et al. Determining computational complexity from characteristic “phase transitions”[J]. Nature, 1999, 400(6740): 133-137

[5]Mezard M, Parisi G, Zecchina R. Analytic and algorithmic solution of random satisfiability problems[J]. Science, 2002, 297(5582): 812-815

[6]Luo Chuan, Cai Shaowei, Wu Wei, et al. Double configuration checking in stochastic local search for satisfiability[C]Proc of the 28th AAAI Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2014: 2703-2709

[7]Cai Shaowei, Su Kaile. Comprehensive score: Towards efficient local search for SAT with long clauses[C]Proc of the 23rd Int Joint Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2013: 489-495

[8]Davis M, Putnam H. A computing procedure for quantification theory[J]. Journal of the ACM (JACM), 1960, 7(3): 201-215

[9]Cai Shaowei, Su Kaile. Local search for boolean satisfiability with configuration checking and subscore[J]. Artificial Intelligence, 2013, 204: 75-98

[10]Luo Chuan, Cai Shaowei, Su Kaile, et al. Clause states based configuration checking in local search for satisfiability[J]. IEEE Trans on Cybernetics, 2015, 45(5): 1014-1027

[11]Chavira M, Darwiche A. On probabilistic inference by weighted model counting[J]. Artificial Intelligence, 2008, 172(6): 772-799

[12]Sang T, Beame P, Kautz H A. Performing Bayesian inference by weighted model counting[C]Proc of the 20th National Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2005: 475-481[13]Majercik S M, Littman M L. Contingent planning under uncertainty via stochastic satisfiability[J]. Artificial Intelligence, 2003, 147(1): 119-162[14]Bacchus F, Dalmao S, Pitassi T. Algorithms and complexity results for #SAT and Bayesian inference[C]Proc of the 44th Symp on Foundations of Computer Science. Los Alamitos, CA: IEEE Computer Society, 2003: 340-351[15]Zhou Junping, Yin Minghao, Zhou Chunguang. New worst-case upper bound for #2-SAT and #3-SAT with the number of clauses as the parameter[C]Proc of the 24th AAAI Conf on Artificial Intelligence (AAAI 2010). Menlo Park, CA: AAAI, 2010: 217-222[16]Birnbaum E, Lozinskii E L. The good old Davis-Putnam procedure helps counting models[J]. Journal of Artificial Intelligence Research, 1999, 10(1): 457-477[17]Bayardo Jr R J, Pehoushek J D. Counting models using connected components[C]Proc of the 17th National Conf on Artificial Intelligence (AAAI 2000). Menlo Park, CA: AAAI, 2000: 157-162[18]Bacchus F, Dalmao S, Pitassi T. DPLL with caching: A new algorithm for #SAT and Bayesian inference[J]. Electronic Colloquium on Computational Complexity, 2003, 10: 1-21[19]Sang T, Bacchus F, Beame P, et al. Combining component caching and clause learning for effective model counting[C]Proc of the SAT 2004. Berlin: Springer, 2004: 20-28[20]Davies J, Bacchus F. Using more reasoning to improve #SAT solving[C]Proc of the 22nd National Conf on Artificial Intelligence. Menlo Park, CA: AAAI, 2007: 185-190[21]Darwiche A. New advances in compiling CNF into decomposable negation normal form[C]Proc of the 16th European Conf on Artificial Intelligence. Amsterdam: IOS, 2004: 328-332[22]Wei W, Selman B. A new approach to model counting[C]Proc of the SAT 2005. Berlin: Springer, 2005: 324-339[23]Lin Hai, Sun Jigui, Zhang Yimin. Theorem proving based on extension rule[J]. Journal of Automated Reasoning, 2003, 31(1): 11-21[24]Wu Xia, Sun Jigui, Lin Hai, et al. Modal extension rule[J]. Progress in Natural Science, 2005, 15(6): 550-558[25]Lin Hai, Sun Jigui. Knowledge compilation using extension rule[J]. Journal of Automated Reasoning, 2004, 32(2): 93-102[26]Sun Jigui, Li Ying, Zhu Xingjun, et al. A novel theorem proving algorithm based on extension rule[J]. Journal of Computer Research and Development, 2009, 46(1): 9-14 (in Chinese)(孫吉貴, 李瑩, 朱興軍, 等. 一種新的基于擴展規(guī)則的定理證明算法[J]. 計算機研究與發(fā)展, 2009, 46(1): 9-14)[27]Zhang Liming, Ouyang Dantong, Bai Hongtao. Theorem proving algorithm based on semi-extension rule[J]. Journal of Computer Research and Development, 2010, 47(9): 1522-1529 (in Chinese)(張立明, 歐陽丹彤, 白洪濤. 基于半擴展規(guī)則的定理證明方法[J]. 計算機研究與發(fā)展, 2010, 47(9): 1522-1529)[28]Li Ying, Sun Jigui, Wu Xia, et al. Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J]. Journal of Software, 2009, 20(6): 1521-1527 (in Chinese)(李瑩, 孫吉貴, 吳瑕, 等. 基于IMOM和IBOHM啟發(fā)式策略的擴展規(guī)則算法[J]. 軟件學(xué)報, 2009, 20(6): 1521-1527)[29]Yin Minghao, Lin Hai, Sun Jigui. Solving #SAT using extension rules[J]. Journal of Software, 2009, 20(7): 1714-1725 (in Chinese)(殷明浩, 林海, 孫吉貴. 一種基于擴展規(guī)則的#SAT求解系統(tǒng)[J]. 軟件學(xué)報, 2009, 20(7): 1714-1725)[30]Sun Jigui, Yang Fengjie, Ouyang Dantong, et al. Discrete Mathematics [M]. Beijing: Higher Education Press, 2002 (in Chinese)(孫吉貴, 楊鳳杰, 歐陽丹彤, 等. 離散數(shù)學(xué)[M]. 北京: 高等教育出版社, 2002)[31]Rymon R. Search through systematic set enumeration[C]Proc of the 3rd Int Conf on Principles of Knowledge Representation and Reasoning. San Francisco: Morgan Kaufmann, 1992: 539-550

Ouyang Dantong, born in 1968. Professor and PhD supervisor of Jilin University. Senior member of China Computer Federation. Her main research interests include model-based diagnosis, model checking and automated reasoning.

Jia Fengyu, born in 1991. Master candidate. His main research interests include model-based diagnosis, SAT problem and automated reasoning (jiafy_email@163.com).

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

Zhang Liming, born in 1980. PhD, post-doctor in Jilin University. His main research interests include model-based diagnosis, model checking and automated reasoning.

收稿日期：2015-01-12；修回日期：2015-06-02

基金項目：國家自然科學(xué)基金項目(61402196,61272208,61133011,61003101,61170092)；中國博士后科學(xué)基金項目(2013M541302)；吉林省科技發(fā)展計劃基金項目(20140520067JH)

通信作者：張立明(limingzhang@jlu.edu.cn)

中圖法分類號TP18

An Algorithm Based on Extension Rule For Solving #SAT Using Complementary Degree

Ouyang Dantong, Jia Fengyu, Liu Siguang, and Zhang Liming

(CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012) (KeyLaboratoryofSymbolicComputationandKnowledgeEngineering(JilinUniversity),MinistryofEducation,Changchun130012)

AbstractThe #SAT problem also called model counting is one of the important and challenging problems in artificial intelligence. It is used widely in the field of artificial intelligence. After doing the in-depth study of model counting algorithm CER that is based on Extension Rule, we propose a method using complementary degree for #SAT problem in this paper. We formalize the computing procedure of solving #SAT problem by introducing SE-Tree which produces all the subsets of clause set that need to be computed. As the closed nodes are added into the SE-Tree, the most subsets that contain complementary literal(s) can never be produced, and the true resolutions cannot be missed by pruning either. Then the concept of complementary degree is presented in this paper, and the nodes of SE-Tree are extended in accordance with the descending order of complementary degree. With this extended order, the subsets that contain complementary literal(s) and have smaller size can not only be generated early, but also can reduce the number of generated nodes that are redundant. Moreover the calculation for deciding the complementarity of subsets is reduced. Results show that the corresponding algorithm runs faster than CER algorithm and further improves the solving efficiency of problems which complementary factor is lower.

Key wordsextension rule; model counting; CER (counting models using extension rules) algorithm; complementary degree; SE-Tree (set enumeration tree)

This work was supported by the National Natural Science Foundation of China (61402196,61272208,61133011,61003101,61170092), the China Postdoctoral Science Foundation (2013M541302), and the Jilin Province Science and Technology Development Plan (20140520067JH).