多文字可滿足SAT問題的相變點上界*

蘆 磊,王曉峰,2,梁 晨,張九龍

(1.北方民族大學計算機科學與工程學院，寧夏 銀川 750021； 2.北方民族大學圖像圖形智能處理國家民委重點實驗室，寧夏 銀川 750021)

1 引言

可滿足性SAT(SATisfiability)問題是一種特殊的約束滿足問題 CSP(Constraint Satisfaction Problem)，也是最基本的CSP問題。給定一個合取范式CNF(Conjunctive Normal Form)公式F，SAT問題指是否存在一組布爾變元賦值，使得F中每個子句至少有1個文字為真。在SAT問題中，子句長度為k的SAT問題被稱為k-SAT問題。k≥3的k-SAT問題是世界上第一個被證明的NP-完全問題[1]。

本文研究的多文字可滿足SAT問題MLSAT(Multi Literal SATisfiability problem)是指：是否存在一組變元指派，使得SAT實例的每個子句至少有2個文字為真。顯然，MLSAT問題仍然是NP難問題。MLSAT問題是SAT問題的特殊情況，如果一個賦值指派是MLSAT問題的解，則其必然也是SAT問題的解。在現實生活中，MLSAT問題也很常見，如機器調度問題往往需要多臺機器同時運行，又比如在競賽中，往往需要3局2勝才能取得勝利。各種NP難問題往往不會恰好編碼為嚴格的SAT問題，因此，研究多個文字為真的SAT問題很有意義。

設F是MLSAT問題中n個布爾變量x1,…,xn的隨機3-CNF公式，m為F的子句個數，約束密度α=m/n。本文研究的問題是計算最小實數α*，當n趨于無窮大時，如果α嚴格大于α*，3-MLSAT問題可滿足的概率收斂到0。在這種情況下，3-MLSAT問題高概率不可滿足。實驗數據表明，α*的值在0.65左右。實驗還表明，如果α嚴格小于α*， 3-MLSAT問題高概率是漸近可滿足的。因此，從實驗上講，α*既是可滿足性相變點上界，又是命題公式由可滿足變化到不可滿足的閾值。本文模型從3-CNF公式出發，可推廣到k-CNF公式。通過對相變上界的研究，不僅有助于進一步認識這類問題的難解本質，還有助于設計出更為高效的算法。

MLSAT問題是SAT問題的衍生問題，研究SAT問題的相變點上界，對研究MLSAT問題很有參考意義。在多項式時間內，任意CNF公式都可歸約轉換到3-CNF公式[2,3]，因此，學術界普遍研究3-SAT問題的相變點上界。1983年，Franco等人[4]利用一階矩方法的簡單應用產生了5.191的上界。1992年，文獻[5]經過實驗驗證存在相變點。在后續的研究中，文獻[6]是一個重要的進步，Kamath等人基于占用問題和獨立變量，將上界提升到了4.758。文獻[7]基于一階矩負素解，將上界提升到4.64。文獻[8]基于一階矩隨機變量序列，將上界提升到4.667。文獻[9]通過限制典型句法特征，又邁進了一大步，將上界提升到4.506。在此基礎上，Dubois等人[10,11]對相變點上界進行了綜述。文獻[12]將上界提升到了4.489 8，這是目前為止最好的上界。此外，基于統計物理的理論性但不嚴謹的工作研究[13,14]，閾值估計在4.27左右。

本文針對MLSAT問題的相變點上界展開研究，引入隨機CNF實例產生模型，利用一階矩和文獻[8]中的局部最大值技術，提升了該問題的相變點上界。具體地講，利用簡單的一階矩證明，當k=3時，α*=1(具體請參考定理1)；利用單次翻轉，α*提升到了0.740 4(具體請參考定理2和定理3)；利用2次翻轉，α*提升到了0.719 3(具體請參考定理4)，本文的模型可推廣到k-CNF公式。最后，選擇變元規模為100和200的隨機CNF實例進行實驗，驗證了k=3和k=4時的2種情形，實驗結果均表明：理論結果與實驗結果相吻合。為了方便描述，本文所有的“滿足”均默認為MLSAT問題。

2 基礎知識

2.1 MLSAT問題實例生成模型

2.2 一階矩簡單證明

定理13-MLSAT問題的不滿足閾值α*=1,4-MLSAT問題的不滿足閾值α*=1.8499，k-MLSAT問題的不滿足閾值為α*=-ln 2/ln(1-(k+1)/2k)。

在證明定理1之前，需要先證明引理1。

引理1在MLSAT問題中，對于任意指派Z={z1,z2,…,zn}∈{0,1}n，指派Z可滿足的公式數量是相同的。

□

下面再證明定理1：

(1)

□

3 主要結論

3.1 單次翻轉證明相變點上界

(1/2)α(2-e-3α/2)=1

(2)

在證明定理2之前，需要先證明下面幾個引理。

證明在3-MLSAT問題中，給定3個不同的變量xi,xj和xk，其文字組合有8種。對于任意一個文字組合，可滿足的賦值指派有4種，設恰好滿足該子句2個文字的真值指派為A1，更改A1的變元取值，更改后的指派不滿足該子句。從一個子句出發，可推導至m個子句，引理2得證。

□

(3)

其中,

(4)

引理3得證。

□

A∈Sn]

(5)

□

下面給出定理2的證明：

(6)

□

(7)

(8)

定理3得證。當k=4時，α*=1.6085，符合第3節的實驗結果。

□

3.2 2次翻轉證明相變點上界

引進變量字典序的定義：變量賦值為False的字典序小于賦值為True的。定義字典序的作用是識別關于n個變量的賦值指派的類別。2次翻轉也從3-CNF公式入手。

引理5在MLSAT中，式(9)中的馬爾可夫不等式成立:

(9)

引理6式(10)成立：

(10)

3.2.1 概率計算

先來介紹一下子句的生成模型:

Gp：模型中的每個子句都以獨立的概率p出現在公式中。

Gm：通過均勻且獨立地選擇m個子句且不放回抽樣來獲得隨機公式。

Gmm：通過均勻且獨立地選擇m個子句且放回抽樣來獲得隨機公式，本文中使用的即為Gmm模型(請注意，我們僅引用賦值指派A滿足的子句)。

(11)

(12)

引理7式(13)成立：

(13)

(14)

引理7得證。

□

Janson不等式

(15)

□

利用Janson不等式的上述變體得出如式(16)所示結論:

(16)

根據引理7，ε=o(1)。現在計算不等式中出現的Δ，設置u=e-3α/2，則式(14)變為如式(17)所示：

(17)

引理8令df0和df1為2個2次翻轉，它們共享從False變為True的變量。然后可以得到式(18)：

(18)

□

引理9令df0和df1為2個2次翻轉，它們共享從True變為False的變量。然后可以得到式(19)：

(19)

□

現在，觀察到2次翻轉的有序對的數量最多為df(A)·n，且引理8中的概率小于引理9中的概率。代入Δ，得到式(20)：

(20)

將式(17)和Δ代入式(16)，得到式(21)：

(21)

在u的取值范圍內，不等式的右側表達式最多為1?，F在，通過式(10)～式(12)和式(21)，得到式(22):

(22)

其中：

X=1-u+o(1)

(23)

(24)

在3.3.2節中，將給出不等式(22)總和的估計值。

3.2.2 數值估計

引理10如果0≤X2≤Y≤1，則式(25)成立:

(25)

其中：

證明原理請參閱文獻[26]，然后對n進行歸納[27,28]。

(26)

(27)

最后，令df_eq(α)是在公式ln(1/2)α(Z′/2)+dilog(1+X)-dilog(1+XeZ′/2)中替換X和Z′的值且去掉它們的漸近項時得到的表達式。引理10得證。

□

使用Yn/2=eZ′/2和Y=1+o(1)，則可以得到df_eq(α)的表達式如式(28)所示：

df_eq(α)=ln(1/2)α(Z′/2)+

dilog(Z′/2)-dilog(1+XeZ′/2)

(28)

方程df_eq(r)=0的唯一正數解即為α*。使用Matlab 獲得了值α*=0.7193，定理4得證。

□

4 數值實驗與分析

在實驗中，利用第1節中的MLSAT問題實例模型G(n,k,α)來生成隨機實例，取2組變元規模不同的數據，規模分別為n=100和n=200。根據定理1,當k=3時，α*=1；當k=4時，α*=1.8499；根據定理2和定理3，當k=3時,α*=0.7404；當k=4時,α*=1.6085。根據定理4，當k=3時,α*=0.7193。圖1和圖2分別表示k=3和k=4時的MLSAT問題的相變現象，圖中的每個數據點均由100個隨機實例的統計結果產生，橫坐標表示相變控制參數α，縱坐標表示MLSAT問題實例可滿足的統計概率。經實驗得到，3-MLSAT的相變點在0.6～0.8，4-MLSAT的相變點在1.4～1.8。本文理論結果與實驗結果吻合。

Figure 1 Phase transition phenomenon of MLSAT problem (k=3)圖1 MLSAT 問題的相變現象 (k=3)

Figure 2 Phase transition phenomenon of MLSAT problem (k=4)圖2 MLSAT 問題的相變現象 (k=4)

5 結束語

本文分析了隨機多文字可滿足SAT問題的可滿足性相變點上界。具體地講，設α*是關于k(k>3)的一個常數，F是一個隨機CNF實例，當相變控制參數α>α*時，則F是高概率不可滿足的。多文字可滿足SAT問題可以看作是SAT問題的一種特殊情況，對該問題相變現象的分析，有助于分析SAT問題及其同類型問題的相變。在研究中使用了一階矩和局部最大值方法，通過構造實例的解結構，給出了相關結論。下一步將利用更精確的方法研究相變上界，研究多文字可滿足SAT問題的相變下界等。