CNF公式賦值空間上可滿足解的概率性質*

莫孝玲，許道云

貴州大學 計算機科學與技術學院，貴陽 550025

1 引言

可滿足性問題（SAT問題）是指：給定一組布爾變量V，由V上變元或其否定生成的集合作為子句，一組子句集合構成一個公式F，判定是否存在一組真值賦值滿足F中所有子句。SAT問題是理論計算機科學和人工智能的核心問題，其理論及其應用研究是計算機與數理邏輯界眾多學者共同關注的一個重大問題。涉及協調性驗證的問題都可以轉化為SAT問題。因此，在實際應用中得到廣泛應用，如：人工智能、交通運輸、資源調度、工程技術等領域[1]。

SAT問題是著名的NP完全問題，在某些控制條件下的有效求解算法及隨機算法一直受到關注。1992年Selman等人提出了貪婪搜索算法GSAT（greedy local procedure for solving satisfiability problems）[2]，隨后在GSAT算法中加入隨機游走所產生的GSAT+walk[3]算法對求解SAT問題更加有效，然而在GSAT+walk的搜索過程中會出現很多平移[4]。平移指將一個變量翻轉后，滿足的子句個數不變。一段連續的平移則組成了一個平臺，即陷入局部最優解。隨著對SAT問題的不斷研究，基于圖論工具是重要的方法之一，圖結構的表達能力和性質在SAT問題研究得到應用。文獻[5-6]將合取范式（conjunctive normal form，CNF）公式轉化成因子圖，研究圖上的有關性質，探究CNF公式的可滿足性。由于子句、變元之間聯系的復雜性，使得SAT實例存在潛在的結構性特征。文獻[7]通過將SAT實例表示成圖模型，采用團體結構數據挖掘技術分析SAT實例中子句與子句之間，變元與變元之間潛在的結構信息。文獻[8]采用公式的結構信息和子句間的約束關系，提出了CNF公式幾種新型特征，并基于此設計了一種新型的SAT求解器的分類模型。文獻[9]將CNF公式子句中文字之間的關系形成一類子句圖，利用圖來提取和研究隱藏在CNF公式中的結構信息，并基于此對CNF公式提出了各種簡化技術，提高了SAT問題的求解效率。但是，通過該簡化技術僅僅作用于部分特殊子句，對大部分子句不起作用。因此，公式中所隱含的結構信息為探究可滿足性問題提供了新的方法，為求解SAT問題提供了新的思路。

目前尋找問題精確解的算法可分為回溯搜索法和局部最優搜索法。而局部最優搜索法的基本步驟為：隨機為布爾變量賦初值，重復隨機選擇變量翻轉以改善當前解的質量，直到無法改變當前解的質量為止。但該方法每次都只翻轉一個變量，要實現多個變量都翻轉時，需要進行多次翻轉。本文引入了一個帶翻轉次數界控制的參數k(1≤k≤n)，其中n為公式中出現的變元個數，以CNF公式的每個賦值作為一個結點，基于翻轉界控制下賦值滿足子句數的大小，引入一類有向圖——BF（bounded flips）圖。k的不同取值，控制了變量翻轉的個數，以此來考察在給定賦值下至多同時翻轉k個變量值的鄰近賦值如何影響公式的可滿足性，并在參數k控制下分析解的結構性質及概率性質。

本文旨在通過研究BF圖上的一些基礎性質，分析公式的結構信息[10]，并進一步采用貪心搜索策略，在圖上進行隨機游走以達到變量翻轉的目的，研究CNF公式可滿足解的概率性質，為在圖上設計有效的啟發式算法求解CNF公式的可滿足問題提供理論依據。

2 基礎知識

給定一組布爾變量V=(x1,x2,…,xn)，|V|=n，變元xi對應的文字是xi或者?xi，xi是正文字，?xi是負文字，文字用L表示。一個子句C是若干個文字（不同變元）的析取，所含文字的個數稱為子句的長度，記為|C|[11]。一個合取范式（CNF）公式F是若干個子句的合取F=(C1∧C2∧…∧Cm)，公式F可以視為一個子句的集合F={C1,C2,…,Cm}。如果一個子句含有一對互補文字，稱該子句為重言子句[12]。在一個公式中刪除重言子句后，不影響公式的可滿足性。SAT問題是指：是否存在一組對變元的真值賦值，滿足子句集{C1,C2,…,Cm}中每一個子句。

如果公式中每個子句的長度恰好為r，那么這個CNF公式稱為r-CNF公式。任一個CNF公式在多項式時間內都可以規約為一個3-CNF公式[13]。因此，本文的研究主要圍繞3-CNF公式展開研究。

2.1 帶變量翻轉控制參數的BF圖

F是一個含有n個變元(x1,x2,…,xn)，m個子句{C1,C2,…,Cm}的合取范式，對于合取范式公式F的一個指派τ=(a1,a2,…,an)∈{0,1}n，用表示指派τ中1出現的個數。并用#τ(F)表示合取范式公式F在指派τ下滿足的子句數。顯然，#τ(F)≤m，并且當#τ(F)=m時，指派τ是合取范式公式F的一個可滿足指派。對于合取范式公式F的任意兩個賦值指派τ=(a1,a2,…,an),τ′=(b1,b2,…,bn)∈{0,1}n定義τ⊕τ′=(a1⊕b1,a2⊕b2,…,an⊕bn)，則|τ⊕τ′|1記錄了τ與τ′兩個指派之間賦值發生改變的變量個數。

對于給定的一個含有n個變元和m個子句的CNF公式F。引入了一個帶翻轉次數界控制參數k(1≤k≤n)，由此定義一個與CNF公式F相關聯的有向圖D=(V,A)。點集合V={0,1}n，其中 |V|=2n，即每一組賦值指派對應有向圖D中的一個點。邊集合A={e1,e2,…,el}，對于任意的兩個結點τ,τ′∈V，邊定義為：

其中，λF:V→[m]為一個結點賦權函數，[m]={0,1,…,m}，λF(τ):=#τ(F)。由此可知，若兩個結點之間有邊，當且僅當兩個結點的賦值指派之間變量翻轉數不小于1且不超過k；而且，有向邊的方向是從賦值滿足子句數少的結點指向滿足子句數多或相等的結點。因此，有向圖中的邊指示了賦值的進化情況，并且每次改變指派中的賦值時，控制取值改變的變量數不超過k。如：k=1時，代表圖中鄰結點至少有一個變量取值被翻轉。

將上述定義的有向圖D=(V,A)稱為CNF公式F的BF圖。

2.2 BF圖實例構造

通過一個具體的實例來說明對于一個3-CNF給定的公式F，如何構造其對應的BF圖。

假定CNF公式F含有n=4個變元，m=6個子句，F由如下公式給出：

由2.1節中BF圖的定義可知，1≤k≤4，該CNF公式F有4個變元，總共有24=16組賦值指派，則對應的BF圖有24=16個點。表1列出了在16種賦值指派下，CNF公式F所滿足的子句個數。

Table 1 Number of clauses satisfied under each assignment表1 各賦值指派下所滿足的子句數

取k=1，此時每個賦值結點有個鄰接結點。

例如：對于0000賦值結點，一個變量發生改變的賦值鄰接結點共 4個，分別是 0001、0010、0100、1000。由表1可知，指派0000、0001、0010、0100、1000所滿足子句數分別是6、6、5、4、6。由BF圖中邊的定義可知，0000結點與1000結點和0001結點所滿足的子句數都相等，則結點0000與0001和1000之間都存在一條雙向邊（可看成為無向邊）。雖然0000點與0010點、0100點之間存在邊，但是BF圖中的邊是從滿足子句數少的點指向滿足子句數多的點。因此，存在一條由0010點指向0000點的有向邊，存在一條由0100點指向0000點的有向邊，即0000?0001，0000?1000，0000←0010，0000←0100。

根據以上分析，得出當k=2時的有向BF圖的鄰接矩陣，見表2。

Table 2 Adjacency matrix of BF graph atk=2表2 k=2，BF圖的鄰接矩陣

表2中0表示兩個點之間無邊相連，第i行第j列的值為1表示存在一條從結點i指向結點j的有向邊。根據CNF公式F的鄰接矩陣，可畫出BF圖。圖1為示例中k=2時的BF圖。雖然CNF公式只有4個變元，共計16個點，當k=1時，BF圖的總邊數為32，但是當k=2時，圖的總邊數高達80。因此隨著變量翻轉控制參數k的不斷增大，對應BF圖的規模也逐漸增加，BF圖中點與點之間的關系將會變得異常復雜。

上述例子給出了一個含4個變元，6個子句的CNF公式在相應翻轉控制參數下的構造BF圖的詳細過程。由于點與點之間的復雜聯系，直接對圖進行研究顯然是不可取的，通過對圖的鄰接矩陣進行研究，以達到對圖進行研究的目的，進一步研究圖上的若干性質。

Fig.1 BF graph atk=2圖1 k=2時的BF圖

3 帶翻轉控制參數的BF圖的基礎性質

設由包含n個變元，m個子句的CNF公式F所定義的有向BF圖D=(V(D),A(D))，|V(D)|=2n=N為結點數，點集合V(D)={v1,v2,…,vN}，|A(D)|為邊數，用dD(vi)表示結點vi的度，用分別表示結點vi的入度和出度，則有：

有向圖D的鄰接矩陣M(D)=(cij)N×N，cij∈{0,1}(i,j∈{1,2,…,N})表示M(D)中第i行j列的元素，cij=1表示有一條從結點vi指向結點vj的有向邊。

值得注意的是：由于BF圖是有向圖，因此有：

用K(D)=(eij)N×N表示D的距離矩陣[14]，eij∈[N]為K(D)中第i行j列的元素，表示從結點vi到結點vj的最短路徑距離，則有 ?i,j∈[N]，eii=0，eij≠eji。因此，有向圖D的直徑表示為：dm(D)=maxu,v∈V(D)K(u,v)。

通過簡易分析可歸納BF圖上的基礎性質有：

（2）隨著k的增大，BF圖的直徑越來越小，當k=n時，dm(D)=1。

（3）?vi∈V(D)，diDn(vi)≤ Δin(D)=C1n+C2n+…+Cnk，當結點vi是CNF公式的一個可滿足指派時，取等號。

（4）?vi∈V(D)，doDut(vi)≤ Δout(D)=C1n+C2n+…+Ckn，滿足子句數最少的賦值指派點有最大出度。

（5）在k=n的BF圖中，若兩個指派所滿足的子句數相同，那么兩個賦值指派點的入度和出度分別對應相等。當時，有。

4 BF圖上可滿足解的概率性質

用sat(F)表示使含n個變元m個子句的CNF公式F可滿足的賦值指派個數。在公式F定義的BF圖中均有2n個結點，在圖上隨機選擇一個點，選中能使F可滿足的結點的概率為。下面，本文進一步研究在圖上獲得可滿足解的概率性質。

定理1[15]非負n階矩陣A=(aij)n×n為概率矩陣，當且僅當A有特征值1，且對應的特征向量α=[1,1,…,1]T。此定理將用于后面的性質證明。

4.1 可滿足解的概率性質

定理2若一個CNF公式本身是可滿足的，在其任意k值下的BF圖上進行t次隨機游走，當t足夠大時，取得可滿足解的概率最終會收斂，且收斂于1。

證明記[n]={1,2,…,n}，則π=(π(1),π(2),…,π(n))稱為[n]上的一個概率行向量，對應[n]上的一個概率分布。

記P=(pij)n×n是一個n階概率矩陣，其中，矩陣中的每一行Pi=(pi1,pi2,…,pin)都是[n]上的一個分布。根據圖中有向邊的方向，可在圖中進行隨機游走到達目的結點。由此，可定義BF圖中點與點之間的概率轉移矩陣為：A=(aij)2n×2n。顯而易見，A是一個2n階概率矩陣，表示為：

若在BF圖上經過t次隨機游走之后，則有：

將式（1）的兩端分別進行相減并進行化簡：

對等式（2）左右兩端分別右乘一個向量，等式仍然成立，因此有：

由定理1和概率矩陣A的定義可得出：

將式（4）左右兩端分別左乘一個向量，等式仍成立，因此有：

式（3）可等價表示成：

由于式（6）中α=[1,1,…,1]T為非零向量，因此式（6）成立的充要條件是(Bt+1-Bt)為全零矩陣，即Bt+1=Bt。因此，在確定的初始分布下，在BF圖上進行t次隨機游走，當t足夠大時，取得可滿足解的概率最終會收斂。

根據BF圖的定義可知，如果在圖上進行無限次隨機游走之后，當結點一旦跳出滿足相同子句的點之間的循環時，最終都會到達可滿足解的點或者在可滿足解的點之間進行循環。最終落入到可滿足解的概率將無限趨近于1。

定理3隨著翻轉控制參數k的增大，在其BF圖上進行一步隨機游走取得可滿足解的概率也相應增大，當k靠近n時，取得可滿足解的概率穩定。

證明用M表示BF圖的鄰接矩陣：

其中，?i,j∈{1,2,…,2n},cij∈{0,1}。

用M′表示BF圖上的概率轉移矩陣：

只在圖上隨機游走一步便可到達可滿足解的點的起點分為兩種情況：（1）起點是使公式不可滿足的賦值指派結點；（2）起點是使得公式可滿足的賦值指派結點。下面就這兩種情況分別進行討論：取在兩個相鄰k值下的BF圖上獲得可滿足解的概率進行分析。

（1）對不可滿足賦值指派點隨機游走一步到達可滿足指派點進行分析。

假設當k=q時，不可滿足點vi一步隨機游走到可滿足點的概率為：

當k=q-1時到可滿足點的概率為：

將等式（8）、等式（9）兩端分別相減可得：

等式（10）中參數的約束關系滿足：Δ1=Δ1′或Δ1=Δ1′+y1成立；同時，Mi=Mi′或Mi=Mi′+x1成立。

對約束關系進行組合可分成如下四種情形：

下面分別對各種情況進行討論：

（2）對可滿足賦值指派點隨機游走一步一定會到達可滿足指派點進行分析。

假設當k=q時，不可滿足點vj的行走到可滿足點的概率為：

當k=q-1時到可滿足解的概率為：

由式（12）、式（13）可得：

式（14）中參數的取值滿足關系：Δ2=Δ2′或 Δ2=Δ2′+y2成立；同時，Mj=Mj′或Mj=Mj′+x2成立。

對約束關系進行組合可分成如下四種情形：

分別對各種情況進行討論：

由于含T(T≠0)個可滿足賦值指派結點的bf圖中有2n-T個不可滿足指派結點，因此綜上所討論，由式（11）和式（15）可得出在兩個相鄰k值下，在bf圖上隨機選擇一個點并進行一步隨機游走后得到可滿足解的概率變化滿足如下約束關系：

對式（16）進行分析發現，當q的取值逐漸靠近n時，x1、x2、y1、y2的值逐漸減小至0，Mi、Mi′的值逐漸增大到 2n-1，Mj、Mj′的值逐漸增加到T。因此有，即。當q逐漸靠近n時，在k=q和k=q-1下獲得可滿足解的概率是相等的。由上述討論得到：當變量翻轉控制參數k逐漸趨近于n時，在BF圖上進行一步隨機游走之后到達可滿足解的概率最終收斂。

假設一個含n個變元，m個子句的CNF公式是可滿足的，公式有s(s≤m)種不同的滿足子句數類別，分別為1,2,…,s-1,s。滿足的子句數分別對應為m,m-1,m-2,…,m-s,m-s+1。賦值指派點個數對應為T,T1,T2,…,TS-2,TS-1,其中由此，當k=n時各類別結點出度分別對應為。

此時，將等式（7）進行化簡，則獲得可滿足解的概率為：

由第3章中的第（5）條基礎性質可對式（17）進行化簡得：

由式（18）可知，當k=n時，獲得可滿足解的概率只與滿足各類子句數的賦值指派點的個數有關，與點與點之間的聯系無關。

4.2 實驗仿真及分析

采用Matlab進行實驗仿真，利用3-sat的實例產生模型生成多組含8個變元12個子句的CNF公式進行研究。當k的取值固定時，在BF圖上進行多次隨機游走，分析取得可滿足解概率的變化情況。在本實驗中取k=1。從圖2可以看出，無論CNF公式本身的初始可滿足概率是何值，在BF圖上進行隨機游走，當t（隨機游走次數）足夠大時，獲得可滿足解的概率最終會收斂且無限趨近于1。概率的收斂速度與獲得可滿足解的初始概率有關，若使得公式本身可滿足的賦值指派較多，概率收斂的速度將會很快。否則，收斂速度很慢。此實驗證明了定理2的正確性。

Fig.2 Random walk steps and probability of satisfied solution on BF graph withk=1圖2 k=1時BF圖隨機游走步數與可滿足解的概率

隨著k取值的增大，圖中邊的規模增加，BF圖的直徑越來越小[17]，連通性也越來越強。由于圖中各個結點的度數逐漸增加，結點出度也將相應增大，那么隨機選擇一條邊的概率將會減小，但是到達可滿足點的路徑將會增加。那么，在圖上隨機游走一步之后，取得可滿足解的概率會如何，接下來僅考慮可滿足的CNF公式（當公式是不可滿足時，可滿足解的概率為零），研究不同k值下的BF圖對求CNF公式的可滿足解概率的影響。

針對該問題，生成了12組變元規模為8，子句數為12的CNF公式，在28=256種賦值指派中，使得每組CNF公式可滿足的指派數不全相同，還生成了多組變元規模分別為7、9、10的CNF公式進行驗證實驗。

圖3給出了在含8個變元的CNF公式下，k的取值對獲得可滿足解的概率的影響。從圖3可以看出，k=0表示在BF圖中任意取一個賦值指派點恰好為CNF公式的可滿足指派點的概率。隨著k的逐漸增大，在CNF公式對應的BF圖中取得可滿足解的概率逐漸增加，當k無限靠近n時，概率最終穩定。

Fig.3 Probability of satisfied solutions under differentkvalues,formula onn=8,m=12圖3 n=8，m=12時公式在不同k值下的可滿足解概率

緊接著，用變元規模分別為7、9、10的CNF公式進行驗證。圖4刻畫了當變元數分別為7、8、9、10的CNF公式在不同k值下的BF圖上隨機游走一步之后，取得可滿足解的速率變化曲線。圖4表明，無論變元規模有多大，當k=1時，取得可滿足解的概率變化速率最大，隨著k的取值逐漸趨近于n（變元數），變化速率也逐漸趨于0。因此進一步證明，隨著k的增大，在其BF圖上取得CNF公式可滿足解的概率最終收斂。

因此可得出結論：隨著翻轉控制參數k的增大，在其對應的BF圖中獲得可滿足解的概率會逐漸增大。而且，當k趨近于n，獲得可滿足解的概率最終穩定。由此也佐證了定理3的正確性。

5 結束語

為研究含有n個變元m個子句的CNF公式的結構信息，本文引入一個帶翻轉次數界控制的參數k(1≤k≤n)，定義以賦值為結點的翻轉界控制圖——BF圖，分析并總結了BF圖上的基礎性質。在BF圖上進行隨機游走，并利用概率矩陣和圖論的相關知識分析和探究了在BF圖上獲得可滿足解的概率的性質，并通過實驗驗證了性質的正確性。研究發現，無論k取何值，在BF圖上進行隨機游走之后，獲得可滿足解的概率都將會大幅度提升。當k靠近n時，概率收斂。本文的性質有助于設計合理的啟發式算法，為求解可滿足性問題提供理論依據。但是，隨著公式中變元的增多，BF圖的規模逐漸增大，在圖上獲取可滿足解的時間隨著k的增大將會呈指數增加。進一步的工作是：綜合考慮所消耗的時間和獲取可滿足解的概率，探究k的合適取值。由于目前局部搜索算法和隨機游走策略在求解可滿足性問題中所表現出的高性能，下一步可通過CNF賦值空間構造的BF圖和CNF公式的結構信息設計求解可滿足性問題的隨機游走算法。

Fig.4 Change rate of satisfied solution probability underkvalues under different variables圖4 不同變元數時k值下的可滿足解概率變化速率