可滿足問題中的模型計(jì)數(shù)

谷文祥，朱磊，黃平，殷明浩

(東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院，吉林長春 130117)

可滿足問題中的模型計(jì)數(shù)

谷文祥，朱磊，黃平，殷明浩

(東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院，吉林長春 130117)

模型計(jì)數(shù)問題是指計(jì)算給定問題的解的個(gè)數(shù)，這是一類比決策更困難的問題，也是人工智能領(lǐng)域研究的一個(gè)熱點(diǎn)問題.對模型計(jì)數(shù)問題的研究不僅可以提高算法的求解效率，更能促進(jìn)對問題困難本質(zhì)的了解.以可滿足問題(命題可滿足(SAT)和約束可滿足問題(CSP))為例，從精確算法和近似求解兩方面綜述了模型計(jì)數(shù)問題的研究現(xiàn)狀，重點(diǎn)介紹了相關(guān)概念以及各個(gè)算法之間的優(yōu)缺點(diǎn)，并提出了有待解決的開放性問題，對模型計(jì)數(shù)問題的研究予以了總結(jié)和展望.

人工智能;約束可滿足問題;命題可滿足問題;模型計(jì)數(shù)

命題可滿足問題(propositional satisfiability problem，SAT)的求解是近年來人工智能領(lǐng)域研究的熱點(diǎn)問題，這類問題的計(jì)算復(fù)雜度是屬于NP完全的［1］，也即意味著如果P≠NP成立，即無法在多項(xiàng)式時(shí)間內(nèi)解決SAT問題.而模型計(jì)數(shù)問題是比這類決策問題更難解決的問題，它的計(jì)算復(fù)雜度是屬于#P完全的.一些原本是多項(xiàng)式時(shí)間的決策問題的模型計(jì)數(shù)也是屬于#P完全的，例如2SAT［2］.模型計(jì)數(shù)問題是指計(jì)算給定問題的解的個(gè)數(shù)，即使得公式值為真的不同的變量的賦值數(shù).高效地解決模型計(jì)數(shù)問題對人工智能的很多領(lǐng)域都有著深遠(yuǎn)的影響，許多的概率推理如貝葉斯網(wǎng)絡(luò)推理［3］等都可以轉(zhuǎn)換為模型計(jì)數(shù)問題［2］.另一個(gè)應(yīng)用是組合問題，計(jì)算解的個(gè)數(shù)能夠更深入地了解問題的本質(zhì).對于組合這樣的問題，即使找到一個(gè)解都是困難的，搜索整個(gè)解空間的模型計(jì)數(shù)問題的時(shí)間復(fù)雜度更是巨大的.這也就使得目前模型計(jì)數(shù)算法能解決問題的規(guī)模與決策性算法相比相差了好幾個(gè)數(shù)量級(jí).對于模型計(jì)數(shù)問題，目前確定性算法能夠解決的問題的變量數(shù)約為幾百個(gè)，近似算法能解決的問題的變量數(shù)約為1 000個(gè).

約束可滿足問題(constraint satisfaction problem，CSP)是SAT問題的一種泛化，當(dāng)CSP問題中變量的取值為布爾值時(shí)，CSP問題就退化為普通的SAT問題.CSP問題的多值使得其在實(shí)際生活中有著更加廣泛的應(yīng)用，如圖著色問題就是一種特殊的CSP問題，而規(guī)劃問題也可以轉(zhuǎn)換為動(dòng)態(tài)CSP問題求解.CSP問題的模型計(jì)數(shù)(#CSP)方法大部分都是由求解SAT問題的模型計(jì)數(shù)(#SAT)方法擴(kuò)展而來的，因此#CSP問題的求解也可分為2類:精確算法和近似求解.精確算法主要是以DPLL算法和局部搜索為基礎(chǔ)，與決策問題只要找到一個(gè)可滿足解不同，模型計(jì)數(shù)問題需要搜索整個(gè)解空間，因此算法的時(shí)間復(fù)雜度是巨大的.近似求解一般采用采樣的方法來避免搜索整個(gè)解空間，利用局部解的數(shù)目來估計(jì)整個(gè)空間解的個(gè)數(shù).這樣使得算法的時(shí)間復(fù)雜度有了很大的改善，但是所得到解的數(shù)目卻不再是精確的.本文將從以上2個(gè)方面分別介紹#SAT和#CSP問題求解算法的發(fā)展、相關(guān)概念以及算法的優(yōu)缺點(diǎn)，并對模型計(jì)數(shù)問題的求解方向進(jìn)行展望.

1 相關(guān)概念

本文討論的模型計(jì)數(shù)問題都是基于SAT問題和CSP問題的.在介紹具體的算法之前，首先介紹一些與模型計(jì)數(shù)有關(guān)的定義.

定義1(命題可滿足問題，SAT)給定一個(gè)命題邏輯公式F，其變量集為V=var(F)，是否存在對其變量集V的一個(gè)真值賦值，使命題公式F成立(可滿足)，如果成立則返回這些變量真值賦值.

定義2(命題可滿足問題的模型計(jì)數(shù)，#SAT)給定一個(gè)命題邏輯公式F，其變量集為V=var(F)，計(jì)算使得公式值為真的變量集V的賦值的個(gè)數(shù)，并返回這個(gè)值.

定義3(約束可滿足問題，CSP)CSP問題可以描述為一個(gè)三元組P(X，D，C)，其中X是有限變量集合{X1，X2，…，Xn}，D為與X中變量對應(yīng)的域值集合{D1，D2，…，Dn}，C是有限約束的集合，用于限制變量的取值.一個(gè)CSP問題就是找到一個(gè)滿足約束C的變量集X的取值.

定義4(約束可滿足問題的模型計(jì)數(shù)，#CSP)給定一個(gè)CSP問題P，計(jì)算所有使得P中約束滿足的變量集的取值數(shù)目，并返回這個(gè)值.

由上面的定義可知，決策性問題可以看作模型計(jì)數(shù)問題的一種特殊情況.決策性問題只需找到一個(gè)可滿足的解，而模型計(jì)數(shù)問題則要求找到問題的所有解.

在實(shí)際問題求解的過程中，一般將問題轉(zhuǎn)換為圖的結(jié)構(gòu).

定義5(約束圖，GF) 給定一個(gè)命題邏輯公式F，F(xiàn)的約束圖GF的定義如下:

1)GF中的頂點(diǎn)為F中的變量;

2)若F中的2個(gè)變量出現(xiàn)在同一個(gè)子句中，則在這2個(gè)變量所對應(yīng)的頂點(diǎn)連上邊.

約束圖中的頂點(diǎn)表示原問題中的變量，而邊表示變量之間的約束，問題的約束越多，則圖的結(jié)構(gòu)越緊密.

2 SAT中的模型計(jì)數(shù)

SAT問題是CSP問題的特殊實(shí)例，即SAT問題是域大小為2的CSP問題，相較于一般的CSP問題，SAT問題的模型計(jì)數(shù)比較簡單，下面首先介紹有關(guān)SAT問題的模型計(jì)數(shù)方法.

2.1 精確算法

目前求解模型計(jì)數(shù)的方法有2種，即精確算法和近似求解.本文先介紹#SAT中主要的精確算法，然后給出典型的近似求解方法.

2.1.1 CDP算法

Valiant在1979年證明了模型計(jì)數(shù)問題是屬于#P完全的［2］，即這是一類比NP問題更困難的問題.Dubois在1991年給出了一種求解SAT問題模型個(gè)數(shù)的方法，并且證明了時(shí)間復(fù)雜度為O()，其中n為變量數(shù)，m為子句數(shù)，ak是多項(xiàng)式y(tǒng)kyk－1－ … －1 的正根，k為子句的長度［4］.Zhang在1996年也給出了基于類似思想的算法，時(shí)間復(fù)雜度也近似相等［5］.雖然他們的算法都能夠得到問題的解的數(shù)目，但是當(dāng)問題規(guī)模增大時(shí)，算法的時(shí)間復(fù)雜度幾乎是呈指數(shù)級(jí)增長，當(dāng)k趨于無窮的時(shí)候，ak=2.Birnbaum和Lozinskii在1999年提出了基于SAT求解器DPP的CDP［6］，該方法不論是算法的復(fù)雜度還是時(shí)間復(fù)雜度上較前面的2個(gè)方法都有很大的改善.CDP(F，n)算法的基本框架如圖1.

式中:l為單元文字，x為分支變量.

算法的輸入?yún)?shù)為公式F和變量數(shù)n.首先判斷公式是否為空，如果是，則表示公式已經(jīng)被滿足，所以返回解的個(gè)數(shù)為2n;反之公式若包含了空子句，則肯定不滿足，返回0;若公式中有單元子句，則先對單元子句進(jìn)行處理以簡化公式，否則隨機(jī)選擇一個(gè)變量進(jìn)行分支，分支后公式求得模型的總個(gè)數(shù)為原公式的模型數(shù).

SAT求解器DPP找到一個(gè)可滿足解就結(jié)束搜索，而CDP則需要搜索整個(gè)解空間，直到找到所有可滿足的解，算法才結(jié)束.算法的時(shí)間復(fù)雜度為O(mdn)，其中，m為子句數(shù)，n為變量數(shù)，

p為一個(gè)文字出現(xiàn)在一個(gè)子句中的概率.由于純文字規(guī)則在模型計(jì)數(shù)中不能使用，因此分支變量的選擇直接影響了算法的時(shí)間復(fù)雜度.作者提出了2種選擇分支變量的方法，一是使得m2+m3的值盡可能小，m2、m3分別為F2、F3中的子句數(shù)，另外一種是使max(m2，m3)盡量小.通過實(shí)驗(yàn)得出，分支變量的選擇使用第1種方法得到的效果明顯比第2種方法好，但當(dāng)這樣的變量有多個(gè)時(shí)，可以用第2種方法確定下一個(gè)分支變量的擺選擇.

圖1 CDP算法框架Fig.1 Framework of CDP

2.1.2 Relsat算法

在CDP算法中，如果當(dāng)前的賦值使得公式的值為真，那么剩下變量的賦值則不會(huì)影響公式的真值，若當(dāng)前已賦值的變量數(shù)為t，則模型的個(gè)數(shù)為2n－t.雖然這樣可以加快算法的速度，但是算法的主要時(shí)間還是花費(fèi)在分支計(jì)算上，如果能同時(shí)計(jì)算多個(gè)分支的模型個(gè)數(shù)，則算法的速度便可以得到很大的提高.由于CNF公式可以用約束圖來表示，而各個(gè)獨(dú)立的約束圖可以看成是相互獨(dú)立的組件，多個(gè)組件可以同步計(jì)算其模型的個(gè)數(shù)，因此可以將組件的思想應(yīng)用于模型計(jì)數(shù)中，即算法 Relsat［7］.

2.1.3 Cachet算法

在Relsat算法中，主要是通過分別計(jì)算各個(gè)組件的模型數(shù)來得到公式的模型個(gè)數(shù)，如果在計(jì)算的過程中，出現(xiàn)了前面已經(jīng)計(jì)算過的組件，利用Relsat求解算法則需重新計(jì)算一次，如果能在第1次計(jì)算時(shí)記錄這個(gè)結(jié)果，在后續(xù)的搜索過程中得到同樣的組件時(shí)，便可以直接使用緩存里面存儲(chǔ)的結(jié)果.這和SAT求解器中的子句學(xué)習(xí)類似，利用空間換時(shí)間的方法.在Cachet算法中，同時(shí)使用了這2種方法:組件緩存和子句學(xué)習(xí)［8］.

Cachet算法主要是基于SAT求解器zchaff，直接應(yīng)用組件緩存和子句學(xué)習(xí)使得算法求解出來的模型可能是實(shí)際問題模型的一個(gè)下界.為了避免這種情況，作者提出了用Routine remove siblings的方法來避免兩者之間不必要的交叉.

Thurley在Cachet算法上利用不同的存儲(chǔ)方式提高了算法的空間利用率.如算法存儲(chǔ)的組件的子句至少有2個(gè)沒有被賦值的變量，不顯示存儲(chǔ)原公式中的二元子句，并且存儲(chǔ)的是組件中變量的索引以及屬于組件的原始子句的索引.另外，在搜索時(shí)還加入了前向的搜索機(jī)制［9］.Davies和 Bacchus在搜索中的每個(gè)節(jié)點(diǎn)加入了更多的推理，如超二元?dú)w結(jié)和等式約簡，也使得算法的效率有了很大的提高［10］.筆者還提出了利用歸結(jié)的逆(擴(kuò)展規(guī)則)來求解問題的模型數(shù)［11］.

2.1.4 cnf2ddnnf算法

前面提到的算法都是用不同的方法來直接求解給定的問題，而Darwiche在2004年改進(jìn)了以前的知識(shí)編譯算法，在SAT求解器zchaff的基礎(chǔ)上提出了cnf2ddnnf算法［12］.算法的主要思想是將 CNF公式轉(zhuǎn)換為確定的、可分解的否定范式的形式(ddnnf).在轉(zhuǎn)換之前，首先要為原CNF公式F構(gòu)造1棵分解樹，這是一棵每個(gè)節(jié)點(diǎn)只有2個(gè)后代的二元樹，葉子節(jié)點(diǎn)是F中的子句，每個(gè)節(jié)點(diǎn)都保存了一個(gè)稱為separator變量集，里面存儲(chǔ)的是左子樹和右子樹相同的變量.算法的主要思想是為separator變量集中的變量賦值，使得左右子樹變量的交集為空，然后遞歸地構(gòu)造分解樹并將其轉(zhuǎn)換為ddnnf的形式.

2.2 近似求解

模型計(jì)數(shù)的時(shí)間復(fù)雜度是屬于#P完全的，這是比NP完全問題(如SAT問題的可滿足性)更困難的一類問題.目前確定性算法能求解的問題的變量數(shù)約為幾百個(gè)，對于更大規(guī)模的問題，這樣的求解器是無能為力的.另一方面，在某些領(lǐng)域，并不一定要求得到問題精確的模型數(shù)，而只需要一個(gè)大概的估計(jì).近似求解便能很好地滿足這樣的問題，近似求解算法不僅在時(shí)間復(fù)雜度上比確定性算法要低很多，而且能解決更大規(guī)模的問題.

2.2.1 ApproxCount算法

近似求解算法主要是基于采樣的思想，在ApproxCount算法［13］中，用 SampleSAT［14］來進(jìn)行采樣.由于在采樣的過程中使用隨機(jī)行走算法，出現(xiàn)頻率最高的解與出現(xiàn)頻率最低的解相差了幾個(gè)數(shù)量級(jí);因此在SampleSAT算法中加入了MCMC(Markov chain Monte Carlo)來平衡隨機(jī)行走，使得采樣盡量均勻.

首先從公式F的解空間中進(jìn)行K次采樣(一個(gè)采樣是公式的一個(gè)可滿足的解)，K的值由算法的精確度決定.由于采樣是均勻的，所以有

式中:#(x1=t1)是在K次采樣中，x1取t1值的賦值數(shù)，設(shè)t1=true，M(F)為公式F的模型數(shù).定義變量x1的乘數(shù)因子:

由式(1)和(2)，通過遞歸計(jì)算，可得公式F的模型數(shù)為

式中:Fx1=t1為F∧x1單元?dú)w結(jié)后的子公式，其他類似.

根據(jù)相變的原理，當(dāng)C/V(子句數(shù)/變量數(shù))小于某個(gè)值時(shí)，模型數(shù)很多，因此理論上搜索的時(shí)間也多，但是ApproxCount算法的搜索時(shí)間與C/V基本無關(guān).

近似求解時(shí)會(huì)出現(xiàn)由于小誤差的積累而導(dǎo)致大的誤差，但是這種情況在ApproxCount算法中沒有出現(xiàn)，因?yàn)橛?0%的時(shí)間步過高估計(jì)了乘數(shù)因子，而另外的50%過低估計(jì)了乘數(shù)因子，從而使得整個(gè)過程的求解偏差并不大.該算法是遞增式進(jìn)行的，每次設(shè)置一個(gè)變量的值，并且在每一步計(jì)算乘數(shù)因子.ApproxCount時(shí)間復(fù)雜度是關(guān)于問題規(guī)模的多項(xiàng)式時(shí)間的.

2.2.2 SampleCount算法

ApproxCount算法雖然能快速地估計(jì)問題的模型數(shù)，但是算法要求采樣是均勻的，而進(jìn)行均勻采樣的復(fù)雜度是NP的，且算法對得到的結(jié)果沒有保證.Gomes等在IJCAI07會(huì)議上提出的SampleCount算法避免了這樣的問題［15］.

SampleCount算法主要是先為一些變量設(shè)定初值，直到化解后的子公式能夠使用exact count算法進(jìn)行求解，該算法與采樣的質(zhì)量(即是否為均勻采樣)沒有任何關(guān)系.主要是用 SampleSAT［14］作為啟發(fā)式來指導(dǎo)設(shè)定初值的變量的選擇，一般選擇平衡變量，如果沒有，則使用等價(jià)變量化解公式.該算法得到的公式的模型數(shù)為M(F)=2s－αM(G)，s為設(shè)定初值的變量數(shù)，α是松弛因子，M(G)為 exact count計(jì)算出的子公式確定的模型數(shù).SampleCount算法不僅能保證得到的下界的正確率，而且即使采樣是不均勻的也不會(huì)影響結(jié)果.算法精確度為1－2αt，t為迭代次數(shù)，α 是松弛因子，且 α ＞0.

2.2.3 MBound算法

MBound的主要思想是在原始的公式中加入XOR子句，對加入后的公式直接用SAT求解器進(jìn)行求解［16］.由于在最好的情況下，加入XOR子句可以消減一半的解空間，即當(dāng)加入s個(gè)XOR子句后，公式仍是可滿足的，因此原公式至少有2s個(gè)模型.因?yàn)閄OR約束可以有效地提供一個(gè)將解基本平分的hash函數(shù)，所以算法的求解與解在解空間中的分布沒有關(guān)系.算法迭代t次，每次迭代中都加入s個(gè)XOR子句.若每次迭代的結(jié)果公式都是可滿足的，則算法的下界為2s－α，其中α是松弛因子，且α＞0.上界2s+α也是類似得到的.如果在算法中將SAT求解器改為模型計(jì)數(shù)的求解器，算法的求解精度能進(jìn)一步提高.

3 CSP中的模型計(jì)數(shù)

約束可滿足問題是SAT問題的一種泛化，當(dāng)CSP問題中變量的取值為布爾值時(shí)，CSP問題就變?yōu)榱似胀ǖ腟AT問題.CSP問題的多值使得其在實(shí)際生活中有著更加廣泛的應(yīng)用，如圖著色問題和規(guī)劃問題.目前求解CSP的模型計(jì)數(shù)問題的算法只能求解變量數(shù)在100以內(nèi)的問題，且要花費(fèi)大量時(shí)間.由此，設(shè)計(jì)一個(gè)好的求解CSP模型的算法就成為了一個(gè)急需解決的問題.

3.1 精確求解

目前關(guān)于#CSP精確求解的研究成果并不多，以下是主要的求解方法.

3.1.1 CSP2SAT算法

Angelsmark等在2002年給出了一種求解#CSP的方法，這種方法的主要思想是將原問題轉(zhuǎn)換為相對簡單的問題(2SAT)，通過求解轉(zhuǎn)換后的問題的模型數(shù)來得到原問題的模型數(shù)［17］.

給定變量數(shù)為n，值域?yàn)閐的二元CSP實(shí)例P.將P轉(zhuǎn)換為多個(gè)2SAT實(shí)例I0，I1，…，Im，使得P的模型數(shù)與轉(zhuǎn)換后的I0，I1，…，Im模型總數(shù)相同，其中m的大小與n、d的值均有關(guān)，每個(gè)實(shí)例Ik(k=0，1，…，m)中的變量對應(yīng)P中變量的值，即Ik中的變量xe表示P中變量x取值為e.對于給定的變量x∈var(P)，e∈Dom(x)，則xe∈var(Ik)取值為真當(dāng)且僅當(dāng)變量x的賦值為e.實(shí)例Ik主要由兩部分組成:1)與原問題中的約束對應(yīng)的子句，即若P中有約束x≠y，則對所有的e，有﹁(xe∨ye).2)剩下的子句將由原問題中變量的域分對構(gòu)成.如x∈var(P)，e1，e2∈Dom(x)，則加入子句(∨xe2)和(﹁xe1∨)，對于其他e∈Dom(x)且e≠e1，e≠e2，則添加﹁xe，由此來保證x只能取e1或者e2中的一個(gè).若d為偶數(shù)，則有(d/2)n個(gè)實(shí)例，并且覆蓋了原問題P;若d為奇數(shù)，作者給出了一種比較復(fù)雜的域的分法.整個(gè)算法的時(shí)間復(fù)雜度為:當(dāng)d為奇數(shù)時(shí)，分2種情況考慮，當(dāng)d=4k+1，時(shí)間復(fù)雜度為O(O(#2SAT)×((d2+d+2)/4)n/2);當(dāng)d=4k+3，時(shí)間復(fù)雜度為O(O(#2SAT)((d2+d)/4)n/2)，其中O(#2SAT)是目前#2SAT問題最好的求解器所用的時(shí)間復(fù)雜度.3.1.2 CSP2wSAT算法

算法的主要思想是將CSP問題轉(zhuǎn)換為weighted－2SAT問題，但要根據(jù)不同的d值，采用不同的方式.當(dāng)d≤5時(shí)，問題直接轉(zhuǎn)換，然后利用求解#weighted－2SAT模型個(gè)數(shù)的方法來求解原問題的模型個(gè)數(shù);當(dāng)d＞5時(shí)，將d分為小于5且不相交的集合，不同的集合代表不同的問題實(shí)例，然后分別將這些問題實(shí)例轉(zhuǎn)換為weighted－2SAT問題，以這些實(shí)例的復(fù)雜度基底的和作為原問題復(fù)雜度的基底，由此得到了原問題的時(shí)間復(fù)雜度［18］.

該算法的時(shí)間復(fù)雜度為:

式中:a是#weighted－2SAT算法時(shí)間復(fù)雜度的上界基數(shù)，即O(#weighted－2SAT)=O(an).

3.1.3 BTD算法

Favier 等 利用 BTD(backtracking with tree－decomposition)的搜索方法來求解CSP問題的模型數(shù).樹分解的本質(zhì)是對ci∩cj(cj是ci的兒子)的賦值能夠把初始問題分成2個(gè)能獨(dú)立求解的問題.樹搜索中假定簇ci中變量的賦值總是先于ci兒子中變量的賦值，這樣的變量排序可以利用樹分解的性質(zhì).對于樹中的簇ci，逐一對變量賦值，若出現(xiàn)沖突，則進(jìn)行回退，直到ci中所有的變量都已經(jīng)賦值.然后通過BTD算法計(jì)算ci的第1個(gè)兒子cj引導(dǎo)的子問題在賦值ci∩cj下的模型數(shù)，將ci在當(dāng)前賦值下的模型的乘積返回，ci中所有賦值的模型數(shù)的和作為ci的模型數(shù).最后得到c1的模型數(shù)即為要求解的問題的模型數(shù)［19］.該算法的時(shí)間復(fù)雜度是O(mndw+1)，其中，w為樹寬.

3.2 近似求解

3.2.1 CSP+XOR算法

2006年，Gomes等將XOR應(yīng)用于求解SAT問題的模型計(jì)數(shù)中，使得算法不僅能給出問題模型的上下界，還能對給定的結(jié)果進(jìn)行評(píng)估［16］.2007年，他們擴(kuò)展了這一思想，將XOR應(yīng)用到求解CSP問題模型數(shù)［20］.

作者提出了2種實(shí)現(xiàn)方法.一是將CSP問題轉(zhuǎn)換成SAT問題，然后直接加入二值的XOR，求解的過程和MBound算法相同.算法得到的模型個(gè)數(shù)的上下界和值的準(zhǔn)確度也和MBound算法相同.另外一種是不需要轉(zhuǎn)換，直接加入更一般的XOR約束到CSP問題中，算法得到的模型數(shù)的下界為ds－α，準(zhǔn)確度為1－dαt，其中，s是問題中加入的XOR約束的數(shù)目，t是算法迭代的次數(shù)，α就是一個(gè)松弛因子.

3.2.2 ApproxBTD算法

前面介紹的BTD算法只能解決樹寬比較小的問題，當(dāng)問題的樹寬比較大，且為稀疏圖時(shí)，BTD算法會(huì)因?yàn)槌瑫r(shí)而不能給出問題的模型數(shù).而Approx－BTD算法能夠快速地給出更大規(guī)模問題的模型數(shù)近似值.

該算法主要思想是將圖拆分成沒有公共邊的子圖，且每個(gè)子圖都是chordal的.對于每一個(gè)這樣的子圖，調(diào)用BTD求解，然后利用這些子圖的模型數(shù)來估計(jì)原問題的模型個(gè)數(shù)［19］.

3.2.3 AE－count算法

許可等證明了用RB模型生成的隨機(jī)CSP問題存在確定的相變點(diǎn)［21］，因此筆者也提出了一種近似求解 RB模型生成隨機(jī) CSP實(shí)例的算法——AE－count［22］.該算法主要利用了一階矩和二階矩在證明相變點(diǎn)位置時(shí)的特殊作用，證明了算法AE－count的時(shí)間復(fù)雜度是線性的，并且隨著問題規(guī)模的增大，算法的精確度越高.定理1是該算法的主要的思想.

定理1［22］給定用RB模型生成的CSP實(shí)例I、k、α 和r滿足不等式ke－α/k≥1(k≥1/(1 －p))和α ＞1/k，則當(dāng)n→∞且滿足p＜1－e－α/r(或r＜ －α/ln(1－p))時(shí)，

4 未解決的問題

模型計(jì)數(shù)問題是目前人工智能領(lǐng)域的研究熱點(diǎn)之一，但還存在如下一些開放性的問題.

1)在SAT問題中，模型計(jì)數(shù)的確定性算法能解決的問題的變量數(shù)約為幾百個(gè)，這與決策問題能解決的問題規(guī)模相差了好幾個(gè)數(shù)量級(jí).能否設(shè)計(jì)出計(jì)算大規(guī)模問題的確定性算法便成為一個(gè)亟需解決的難題.

2)相較于SAT問題，CSP問題結(jié)構(gòu)更加復(fù)雜，所以求解時(shí)更加得困難.針對CSP問題本身的結(jié)構(gòu)設(shè)計(jì)算法，以提高算法的求解效率，則是另一個(gè)需要進(jìn)一步研究的問題.

5 結(jié)束語

本文給出了SAT和CSP問題目前主要的模型計(jì)數(shù)方法，并對算法的優(yōu)缺點(diǎn)進(jìn)行了評(píng)價(jià).模型計(jì)數(shù)的精確算法只能解決小規(guī)模的問題，并且算法的時(shí)間復(fù)雜度隨著問題規(guī)模增大呈指數(shù)級(jí)增長.將更多的規(guī)則應(yīng)用到算法中，以減小解空間，從而快速地求出解數(shù)是該類算法的一個(gè)發(fā)展方向.近似求解能解決較大規(guī)模的問題，但是算法的復(fù)雜度隨著算法的精度的提高和規(guī)模的增大而增大，AE－count算法不僅簡單，而且當(dāng)變量的值趨于無窮時(shí)，算法的精度為100%，可以作為精確算法.將AE－count應(yīng)用于一般的#SAT和#CSP是下一步的工作重點(diǎn)，最后希望本文的工作能對相關(guān)人員的研究提供幫助.

［1］COOK S A.The complexity of theorem－proving procedures［C］//Proceedings of the Third Annual ACM Symposium on Theory of Computing.New York，USA:ACM，1971:151－158.

［2］VALIANT L G.The complexity of computing the permanent［J］.Theoretical Computer Science，1979，8(2):189－201.

［3］DARWICHE A.The quest for efficient probabilistic inference［R］.Edinburgh，UK:IJCAI，2005.

［4］DUBOIS O.Counting the number of solutions for instances of satisfiability［J］.Theoretical Computer Science，1991，81(1):49－64.

［5］ZHANG Wenhui.Number of models and satisfiability of sets of clauses［J］.Theoretical Computer Science，1996，155(1):277－288.

［6］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.

［7］BAYARDO R J Jr，PEHOUSHEK J D.Counting models using connected components［C］//Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence.Austin，USA，2000:157－162.

［8］SANG T，BACCHUS F，BEAME P，et al.Combining component caching and clause learning for effective model counting［C/OL］. ［2011－07－20］.http://cs.rochester.edu/ ～ kautz/papers/modelcount－sat04.pdf.

［9］THURLEY M.SharpSAT:counting models with advanced component caching and implicit BCP［M］//BIERE A，GOMES C P.Theory and Applications of Satisfiability Testing.Seattle，USA:Springer，2006:424－429.

［10］DAVIES J，BACCHUS F.Using more reasoning to improve#SAT solving［C］//Proceedings of the 22nd National Conference on Artificial Intelligence.Vancouver，Canada，2007:185－190.

［11］YIN Minghao，LIN Hai，SUN Jigui.Counting models using extension rules［C］//Proceedings of the 22nd National Conference on Artificial Intelligence.Vancouver，Canada，2007:1916－1917.

［12］DARWICHE A.New advances in compiling CNF into decomposable negation normal form［C］//Proceedings of the 16th Eureopean Conference on Artificial Intelligence.Valencia，Spain，2004:328－332.

［13］WEI W，SELMAN B.A new approach to model counting［M］//FAHIEM B，WALSH T.Theory and Applications of Satisfiability Testing.St.Andrews， UK: Springer，2005:324－339.

［14］WEI W，ERENRICH J，SELMAN B.Towards efficient sampling:exploiting random walk strategies［C］//Proceedings of the 19th National Conference on Artificial Intelligence，Sixteenth Conference on Innovative Applications of Artificial Intelligence.San Jose，USA，2004:670－676.

［15］GOMES C P，HOFFMANN J，SABHARWAL A，et al.From sampling to model counting［C］//Proceedings of the 20th International Joint Conference on Artificial Intelligence.San Francisco，USA:Morgan Kaufmann Publishers Inc，2007:2293－2299.

［16］GOMES C P，SABHARWAL A，SELMAN B.Model counting:a new strategy for obtaining good bounds［C］//Proceedings of the Twenty－First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference. Boston，USA，2006:54－61.

［17］ANGELSMARK O，JONSSON P，LINUSSON S，et al.Determining the number of solutions to binary CSP instances［C］//Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming.Ithaca，USA，2002:327－340.

［18］ANGELSMARK O，JONSSON P.Improved algorithms for counting solutions in constraint satisfaction problems［C］//Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming.Kinsale，Ireland，2003:81－95.

［19］FAVIER A，GIVRY S D，JEGOU P.Exploiting problem structure for solution counting［C］//Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming.Lisbon，Portugal，2009:335－343.

［20］GOMES C P，Van HOEVE W J，SABHARWAL A，et al.Counting CSP solutions using generalized XOR constraints［C］//Proceedings of the 22nd National Conference on Artificial Intelligence.Vancouver，Canada，2007:204－209.

［21］XU Ke，LI Wei.Exact phase transitions in random constraint satisfaction problems［J］.Journal of Artificial Intelligence Research，2000，12:93－103.

［22］HUANG Ping，YIN Minghao，XU Ke.Exact phase transitions and approximate algorithm of#CSP［C/OL］.［2011－07－20］.http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3508/4142.

谷文祥，男，1947年生，教授，博士生導(dǎo)師，主要研究方向?yàn)橹悄芤?guī)劃與規(guī)劃識(shí)別、形式語言與自動(dòng)機(jī)、模糊數(shù)學(xué)及其應(yīng)用.參與或承擔(dān)多項(xiàng)國家自然科學(xué)基金項(xiàng)目、教育部重點(diǎn)項(xiàng)目、省科委項(xiàng)目，發(fā)表學(xué)術(shù)論文100余篇.

朱磊，男，1987年生，碩士研究生，主要研究方向?yàn)橹悄芤?guī)劃、智能信息處理.

黃平，女，1986年生，碩士研究生，主要研究方向?yàn)橹悄芤?guī)劃與規(guī)劃識(shí)別.

The model counting of a satisfiability problem

GU Wenxiang，ZHU Lei，HUANG Ping，YIN Minghao
(School of Computer Science and Information Technology，Northeast Normal University，Changchun 130117，China)

A model counting problem refers to computing the number of solutions for a given problem which is harder than the decision－making problem.Model counting problems are also a hot topic in the field of artificial intelligence.Research on model counting problems can not only improve the efficiency of an algorithm，but also enhance the understanding of the nature of hard problems.Taking a satisfiability problem in propositional logic，known as an SAT，and a constraint satisfaction problem(CSP)as an example，a model counting problem was reviewed from two aspects:an exact algorithm and approximate algorithm.For each aspect，the development and related concepts along with the advantages and disadvantages were emphasized.Moreover，this paper proposed some unsolved questions of the model counting and gave a summary and outlook of the research on model counting.

artificial intelligence;constraint satisfaction problem;propositional satisfiability problem;model counting

TP18

A

1673－4785(2012)01－0033－07

10.3969/j.issn.1673－4785.201107008

http://www.cnki.net/kcms/detail/23.1538.TP.20120217.1520.001.html

2011－07－25. 網(wǎng)絡(luò)出版時(shí)間:2012－02－17.

國家自然科學(xué)基金資助項(xiàng)目(61070084，60573067，60803102).

黃平.E－mail:huangp218@nenu.edu.cn.