多文字可滿足SAT問(wèn)題的相變點(diǎn)上界*

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

(1.北方民族大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院，寧夏 銀川 750021； 2.北方民族大學(xué)圖像圖形智能處理國(guó)家民委重點(diǎn)實(shí)驗(yàn)室，寧夏 銀川 750021)

1 引言

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

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

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

MLSAT問(wèn)題是SAT問(wèn)題的衍生問(wèn)題，研究SAT問(wèn)題的相變點(diǎn)上界，對(duì)研究MLSAT問(wèn)題很有參考意義。在多項(xiàng)式時(shí)間內(nèi)，任意CNF公式都可歸約轉(zhuǎn)換到3-CNF公式[2,3]，因此，學(xué)術(shù)界普遍研究3-SAT問(wèn)題的相變點(diǎn)上界。1983年，F(xiàn)ranco等人[4]利用一階矩方法的簡(jiǎn)單應(yīng)用產(chǎn)生了5.191的上界。1992年，文獻(xiàn)[5]經(jīng)過(guò)實(shí)驗(yàn)驗(yàn)證存在相變點(diǎn)。在后續(xù)的研究中，文獻(xiàn)[6]是一個(gè)重要的進(jìn)步，Kamath等人基于占用問(wèn)題和獨(dú)立變量，將上界提升到了4.758。文獻(xiàn)[7]基于一階矩負(fù)素解，將上界提升到4.64。文獻(xiàn)[8]基于一階矩隨機(jī)變量序列，將上界提升到4.667。文獻(xiàn)[9]通過(guò)限制典型句法特征，又邁進(jìn)了一大步，將上界提升到4.506。在此基礎(chǔ)上，Dubois等人[10,11]對(duì)相變點(diǎn)上界進(jìn)行了綜述。文獻(xiàn)[12]將上界提升到了4.489 8，這是目前為止最好的上界。此外，基于統(tǒng)計(jì)物理的理論性但不嚴(yán)謹(jǐn)?shù)墓ぷ餮芯縖13,14]，閾值估計(jì)在4.27左右。

本文針對(duì)MLSAT問(wèn)題的相變點(diǎn)上界展開(kāi)研究，引入隨機(jī)CNF實(shí)例產(chǎn)生模型，利用一階矩和文獻(xiàn)[8]中的局部最大值技術(shù)，提升了該問(wèn)題的相變點(diǎn)上界。具體地講，利用簡(jiǎn)單的一階矩證明，當(dāng)k=3時(shí)，α*=1(具體請(qǐng)參考定理1)；利用單次翻轉(zhuǎn)，α*提升到了0.740 4(具體請(qǐng)參考定理2和定理3)；利用2次翻轉(zhuǎn)，α*提升到了0.719 3(具體請(qǐng)參考定理4)，本文的模型可推廣到k-CNF公式。最后，選擇變?cè)?guī)模為100和200的隨機(jī)CNF實(shí)例進(jìn)行實(shí)驗(yàn)，驗(yàn)證了k=3和k=4時(shí)的2種情形，實(shí)驗(yàn)結(jié)果均表明：理論結(jié)果與實(shí)驗(yàn)結(jié)果相吻合。為了方便描述，本文所有的“滿足”均默認(rèn)為MLSAT問(wèn)題。

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

2.1 MLSAT問(wèn)題實(shí)例生成模型

2.2 一階矩簡(jiǎn)單證明

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

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

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

□

下面再證明定理1：

(1)

□

3 主要結(jié)論

3.1 單次翻轉(zhuǎn)證明相變點(diǎn)上界

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

(2)

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

證明在3-MLSAT問(wèn)題中，給定3個(gè)不同的變量xi,xj和xk，其文字組合有8種。對(duì)于任意一個(gè)文字組合，可滿足的賦值指派有4種，設(shè)恰好滿足該子句2個(gè)文字的真值指派為A1，更改A1的變?cè)≈担暮蟮闹概刹粷M足該子句。從一個(gè)子句出發(fā)，可推導(dǎo)至m個(gè)子句，引理2得證。

□

(3)

其中,

(4)

引理3得證。

□

A∈Sn]

(5)

□

下面給出定理2的證明：

(6)

□

(7)

(8)

定理3得證。當(dāng)k=4時(shí)，α*=1.6085，符合第3節(jié)的實(shí)驗(yàn)結(jié)果。

□

3.2 2次翻轉(zhuǎn)證明相變點(diǎn)上界

引進(jìn)變量字典序的定義：變量賦值為False的字典序小于賦值為True的。定義字典序的作用是識(shí)別關(guān)于n個(gè)變量的賦值指派的類別。2次翻轉(zhuǎn)也從3-CNF公式入手。

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

(9)

引理6式(10)成立：

(10)

3.2.1 概率計(jì)算

先來(lái)介紹一下子句的生成模型:

Gp：模型中的每個(gè)子句都以獨(dú)立的概率p出現(xiàn)在公式中。

Gm：通過(guò)均勻且獨(dú)立地選擇m個(gè)子句且不放回抽樣來(lái)獲得隨機(jī)公式。

Gmm：通過(guò)均勻且獨(dú)立地選擇m個(gè)子句且放回抽樣來(lái)獲得隨機(jī)公式，本文中使用的即為Gmm模型(請(qǐng)注意，我們僅引用賦值指派A滿足的子句)。

(11)

(12)

引理7式(13)成立：

(13)

(14)

引理7得證。

□

Janson不等式

(15)

□

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

(16)

根據(jù)引理7，ε=o(1)。現(xiàn)在計(jì)算不等式中出現(xiàn)的Δ，設(shè)置u=e-3α/2，則式(14)變?yōu)槿缡?17)所示：

(17)

引理8令df0和df1為2個(gè)2次翻轉(zhuǎn)，它們共享從False變?yōu)門rue的變量。然后可以得到式(18)：

(18)

□

引理9令df0和df1為2個(gè)2次翻轉(zhuǎn)，它們共享從True變?yōu)镕alse的變量。然后可以得到式(19)：

(19)

□

現(xiàn)在，觀察到2次翻轉(zhuǎn)的有序?qū)Φ臄?shù)量最多為df(A)·n，且引理8中的概率小于引理9中的概率。代入Δ，得到式(20)：

(20)

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

(21)

在u的取值范圍內(nèi)，不等式的右側(cè)表達(dá)式最多為1?，F(xiàn)在，通過(guò)式(10)～式(12)和式(21)，得到式(22):

(22)

其中：

X=1-u+o(1)

(23)

(24)

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

3.2.2 數(shù)值估計(jì)

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

(25)

其中：

證明原理請(qǐng)參閱文獻(xiàn)[26]，然后對(duì)n進(jìn)行歸納[27,28]。

(26)

(27)

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

□

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

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

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

(28)

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

□

4 數(shù)值實(shí)驗(yàn)與分析

在實(shí)驗(yàn)中，利用第1節(jié)中的MLSAT問(wèn)題實(shí)例模型G(n,k,α)來(lái)生成隨機(jī)實(shí)例，取2組變?cè)?guī)模不同的數(shù)據(jù)，規(guī)模分別為n=100和n=200。根據(jù)定理1,當(dāng)k=3時(shí)，α*=1；當(dāng)k=4時(shí)，α*=1.8499；根據(jù)定理2和定理3，當(dāng)k=3時(shí),α*=0.7404；當(dāng)k=4時(shí),α*=1.6085。根據(jù)定理4，當(dāng)k=3時(shí),α*=0.7193。圖1和圖2分別表示k=3和k=4時(shí)的MLSAT問(wèn)題的相變現(xiàn)象，圖中的每個(gè)數(shù)據(jù)點(diǎn)均由100個(gè)隨機(jī)實(shí)例的統(tǒng)計(jì)結(jié)果產(chǎn)生，橫坐標(biāo)表示相變控制參數(shù)α，縱坐標(biāo)表示MLSAT問(wèn)題實(shí)例可滿足的統(tǒng)計(jì)概率。經(jīng)實(shí)驗(yàn)得到，3-MLSAT的相變點(diǎn)在0.6～0.8，4-MLSAT的相變點(diǎn)在1.4～1.8。本文理論結(jié)果與實(shí)驗(yàn)結(jié)果吻合。

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

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

5 結(jié)束語(yǔ)

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