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

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

?

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

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

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

(ouyd@jlu.edu.cn)

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

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

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

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

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

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

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

1擴(kuò)展規(guī)則

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

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

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

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

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

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

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

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

2CER方法

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

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

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

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

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

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

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

(1)

其中,

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

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

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

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

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

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

3.1互補(bǔ)度概念

定義4. 給定子句集Φ，C∈Φ，則稱子句集Φ中與子句C含有互補(bǔ)文字的子句個(gè)數(shù)為子句C的互補(bǔ)度，記為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. 給定子句集Φ，若Φ的一個(gè)子集Φ′中子句所擴(kuò)展出的極大項(xiàng)集合交集為空，則任何Φ′的超集中子句擴(kuò)展出的極大項(xiàng)集合的交集也為空.

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

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

3.2CDCER(complementary-degree-based CER)

方法

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

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

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

(2)

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

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

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

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

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

算法1. CDCER(Φ,X).

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

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

①num_model=0;

②Node←?;

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

④ Begin

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

⑥ Break;

⑦ EndIf

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

⑨Com_D(Node,Φ)=-1;

⑩ Continue;

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

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

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

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

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

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

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

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

表1給出了2種方法對于各測試用例的求解時(shí)間及兩者時(shí)間差(CER方法的求解時(shí)間減去CDCER方法的求解時(shí)間)、求解過程中需要擴(kuò)展的結(jié)點(diǎn)數(shù)(需生成的子句集合數(shù))及其差值(CER方法需擴(kuò)展的結(jié)點(diǎn)數(shù)量減去CDCER方法的結(jié)點(diǎn)數(shù))，時(shí)間單位為s.從表1的結(jié)果可以看出，隨著互補(bǔ)因子的增大，2種方法的求解時(shí)間都相對減少，且CDCER方法的求解效率普遍要優(yōu)于CER方法.這是因?yàn)橐话闱闆r下CDCER方法與CER方法中所需擴(kuò)展的結(jié)點(diǎn)數(shù)的差值較大，而CDCER方法恰恰節(jié)省了對這些CER方法中多擴(kuò)展出的結(jié)點(diǎn)判斷是否含有互補(bǔ)文字的時(shí)間，所以效率一般要優(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方法運(yùn)行過程中擴(kuò)展結(jié)點(diǎn)數(shù)對比圖

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

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

5結(jié)束語

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

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

參考文獻(xiàn)

[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)(孫吉貴, 李瑩, 朱興軍, 等. 一種新的基于擴(kuò)展規(guī)則的定理證明算法[J]. 計(jì)算機(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)(張立明, 歐陽丹彤, 白洪濤. 基于半擴(kuò)展規(guī)則的定理證明方法[J]. 計(jì)算機(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ā)式策略的擴(kuò)展規(guī)則算法[J]. 軟件學(xué)報(bào), 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)(殷明浩, 林海, 孫吉貴. 一種基于擴(kuò)展規(guī)則的#SAT求解系統(tǒng)[J]. 軟件學(xué)報(bào), 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

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

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

中圖法分類號(hào)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).