莫孝玲，許道云

貴州大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，貴陽 550025

1 引言

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

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

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

本文旨在通過研究BF圖上的一些基礎(chǔ)性質(zhì)，分析公式的結(jié)構(gòu)信息[10]，并進(jìn)一步采用貪心搜索策略，在圖上進(jìn)行隨機(jī)游走以達(dá)到變量翻轉(zhuǎn)的目的，研究CNF公式可滿足解的概率性質(zhì)，為在圖上設(shè)計(jì)有效的啟發(fā)式算法求解CNF公式的可滿足問題提供理論依據(jù)。

2 基礎(chǔ)知識(shí)

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

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

2.1 帶變量翻轉(zhuǎn)控制參數(shù)的BF圖

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

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

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

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

2.2 BF圖實(shí)例構(gòu)造

通過一個(gè)具體的實(shí)例來說明對于一個(gè)3-CNF給定的公式F，如何構(gòu)造其對應(yīng)的BF圖。

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

由2.1節(jié)中BF圖的定義可知，1≤k≤4，該CNF公式F有4個(gè)變元，總共有24=16組賦值指派，則對應(yīng)的BF圖有24=16個(gè)點(diǎn)。表1列出了在16種賦值指派下，CNF公式F所滿足的子句個(gè)數(shù)。

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

取k=1，此時(shí)每個(gè)賦值結(jié)點(diǎn)有個(gè)鄰接結(jié)點(diǎn)。

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

根據(jù)以上分析，得出當(dāng)k=2時(shí)的有向BF圖的鄰接矩陣，見表2。

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

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

上述例子給出了一個(gè)含4個(gè)變元，6個(gè)子句的CNF公式在相應(yīng)翻轉(zhuǎn)控制參數(shù)下的構(gòu)造BF圖的詳細(xì)過程。由于點(diǎn)與點(diǎn)之間的復(fù)雜聯(lián)系，直接對圖進(jìn)行研究顯然是不可取的，通過對圖的鄰接矩陣進(jìn)行研究，以達(dá)到對圖進(jìn)行研究的目的，進(jìn)一步研究圖上的若干性質(zhì)。

Fig.1 BF graph atk=2圖1 k=2時(shí)的BF圖

3 帶翻轉(zhuǎn)控制參數(shù)的BF圖的基礎(chǔ)性質(zhì)

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

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

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

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

通過簡易分析可歸納BF圖上的基礎(chǔ)性質(zhì)有：

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

（3）?vi∈V(D)，diDn(vi)≤ Δin(D)=C1n+C2n+…+Cnk，當(dāng)結(jié)點(diǎn)vi是CNF公式的一個(gè)可滿足指派時(shí)，取等號(hào)。

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

（5）在k=n的BF圖中，若兩個(gè)指派所滿足的子句數(shù)相同，那么兩個(gè)賦值指派點(diǎn)的入度和出度分別對應(yīng)相等。當(dāng)時(shí)，有。

4 BF圖上可滿足解的概率性質(zhì)

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

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

4.1 可滿足解的概率性質(zhì)

定理2若一個(gè)CNF公式本身是可滿足的，在其任意k值下的BF圖上進(jìn)行t次隨機(jī)游走，當(dāng)t足夠大時(shí)，取得可滿足解的概率最終會(huì)收斂，且收斂于1。

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

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

若在BF圖上經(jīng)過t次隨機(jī)游走之后，則有：

將式（1）的兩端分別進(jìn)行相減并進(jìn)行化簡：

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

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

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

式（3）可等價(jià)表示成：

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

根據(jù)BF圖的定義可知，如果在圖上進(jìn)行無限次隨機(jī)游走之后，當(dāng)結(jié)點(diǎn)一旦跳出滿足相同子句的點(diǎn)之間的循環(huán)時(shí)，最終都會(huì)到達(dá)可滿足解的點(diǎn)或者在可滿足解的點(diǎn)之間進(jìn)行循環(huán)。最終落入到可滿足解的概率將無限趨近于1。

定理3隨著翻轉(zhuǎn)控制參數(shù)k的增大，在其BF圖上進(jìn)行一步隨機(jī)游走取得可滿足解的概率也相應(yīng)增大，當(dāng)k靠近n時(shí)，取得可滿足解的概率穩(wěn)定。

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

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

用M′表示BF圖上的概率轉(zhuǎn)移矩陣：

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

（1）對不可滿足賦值指派點(diǎn)隨機(jī)游走一步到達(dá)可滿足指派點(diǎn)進(jìn)行分析。

假設(shè)當(dāng)k=q時(shí)，不可滿足點(diǎn)vi一步隨機(jī)游走到可滿足點(diǎn)的概率為：

當(dāng)k=q-1時(shí)到可滿足點(diǎn)的概率為：

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

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

對約束關(guān)系進(jìn)行組合可分成如下四種情形：

下面分別對各種情況進(jìn)行討論：

（2）對可滿足賦值指派點(diǎn)隨機(jī)游走一步一定會(huì)到達(dá)可滿足指派點(diǎn)進(jìn)行分析。

假設(shè)當(dāng)k=q時(shí)，不可滿足點(diǎn)vj的行走到可滿足點(diǎn)的概率為：

當(dāng)k=q-1時(shí)到可滿足解的概率為：

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

式（14）中參數(shù)的取值滿足關(guān)系：Δ2=Δ2′或 Δ2=Δ2′+y2成立；同時(shí)，Mj=Mj′或Mj=Mj′+x2成立。

對約束關(guān)系進(jìn)行組合可分成如下四種情形：

分別對各種情況進(jìn)行討論：

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

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

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

此時(shí)，將等式（7）進(jìn)行化簡，則獲得可滿足解的概率為：

由第3章中的第（5）條基礎(chǔ)性質(zhì)可對式（17）進(jìn)行化簡得：

由式（18）可知，當(dāng)k=n時(shí)，獲得可滿足解的概率只與滿足各類子句數(shù)的賦值指派點(diǎn)的個(gè)數(shù)有關(guān)，與點(diǎn)與點(diǎn)之間的聯(lián)系無關(guān)。

4.2 實(shí)驗(yàn)仿真及分析

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

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

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

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

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

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

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

因此可得出結(jié)論：隨著翻轉(zhuǎn)控制參數(shù)k的增大，在其對應(yīng)的BF圖中獲得可滿足解的概率會(huì)逐漸增大。而且，當(dāng)k趨近于n，獲得可滿足解的概率最終穩(wěn)定。由此也佐證了定理3的正確性。

5 結(jié)束語

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

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