可滿足問題中的模型計數

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

(東北師范大學計算機科學與信息技術學院，吉林長春 130117)

可滿足問題中的模型計數

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

(東北師范大學計算機科學與信息技術學院，吉林長春 130117)

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

人工智能;約束可滿足問題;命題可滿足問題;模型計數

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

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

1 相關概念

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

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

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

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

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

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

在實際問題求解的過程中，一般將問題轉換為圖的結構.

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

1)GF中的頂點為F中的變量;

2)若F中的2個變量出現在同一個子句中，則在這2個變量所對應的頂點連上邊.

約束圖中的頂點表示原問題中的變量，而邊表示變量之間的約束，問題的約束越多，則圖的結構越緊密.

2 SAT中的模型計數

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

2.1 精確算法

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

2.1.1 CDP算法

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

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

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

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

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

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

2.1.2 Relsat算法

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

2.1.3 Cachet算法

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

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

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

2.1.4 cnf2ddnnf算法

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

2.2 近似求解

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

2.2.1 ApproxCount算法

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

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

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

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

式中:Fx1=t1為F∧x1單元歸結后的子公式，其他類似.

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

近似求解時會出現由于小誤差的積累而導致大的誤差，但是這種情況在ApproxCount算法中沒有出現，因為有50%的時間步過高估計了乘數因子，而另外的50%過低估計了乘數因子，從而使得整個過程的求解偏差并不大.該算法是遞增式進行的，每次設置一個變量的值，并且在每一步計算乘數因子.ApproxCount時間復雜度是關于問題規模的多項式時間的.

2.2.2 SampleCount算法

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

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

2.2.3 MBound算法

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

3 CSP中的模型計數

約束可滿足問題是SAT問題的一種泛化，當CSP問題中變量的取值為布爾值時，CSP問題就變為了普通的SAT問題.CSP問題的多值使得其在實際生活中有著更加廣泛的應用，如圖著色問題和規劃問題.目前求解CSP的模型計數問題的算法只能求解變量數在100以內的問題，且要花費大量時間.由此，設計一個好的求解CSP模型的算法就成為了一個急需解決的問題.

3.1 精確求解

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

3.1.1 CSP2SAT算法

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

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

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

該算法的時間復雜度為:

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

3.1.3 BTD算法

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

3.2 近似求解

3.2.1 CSP+XOR算法

2006年，Gomes等將XOR應用于求解SAT問題的模型計數中，使得算法不僅能給出問題模型的上下界，還能對給定的結果進行評估［16］.2007年，他們擴展了這一思想，將XOR應用到求解CSP問題模型數［20］.

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

3.2.2 ApproxBTD算法

前面介紹的BTD算法只能解決樹寬比較小的問題，當問題的樹寬比較大，且為稀疏圖時，BTD算法會因為超時而不能給出問題的模型數.而Approx－BTD算法能夠快速地給出更大規模問題的模型數近似值.

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

3.2.3 AE－count算法

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

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

4 未解決的問題

模型計數問題是目前人工智能領域的研究熱點之一，但還存在如下一些開放性的問題.

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

2)相較于SAT問題，CSP問題結構更加復雜，所以求解時更加得困難.針對CSP問題本身的結構設計算法，以提高算法的求解效率，則是另一個需要進一步研究的問題.

5 結束語

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

［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年生，教授，博士生導師，主要研究方向為智能規劃與規劃識別、形式語言與自動機、模糊數學及其應用.參與或承擔多項國家自然科學基金項目、教育部重點項目、省科委項目，發表學術論文100余篇.

朱磊，男，1987年生，碩士研究生，主要研究方向為智能規劃、智能信息處理.

黃平，女，1986年生，碩士研究生，主要研究方向為智能規劃與規劃識別.

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. 網絡出版時間:2012－02－17.

國家自然科學基金資助項目(61070084，60573067，60803102).

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