基于分支回溯的NAE-3SAT問題求解算法

谷文祥，傅琳璐，周俊萍，姜蘊(yùn)暉

(1.東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院，吉林長春130117;2.長春建筑學(xué)院基礎(chǔ)教學(xué)部，吉林長春130607)

可滿足性問題(satisfiability，SAT)作為計(jì)算機(jī)理論與應(yīng)用的核心問題，在智能規(guī)劃、機(jī)器視覺、邏輯推理機(jī)以及電子設(shè)計(jì)自動(dòng)化等領(lǐng)域中有著重要的理論研究與實(shí)際應(yīng)用價(jià)值［1-4］.SAT問題的計(jì)算復(fù)雜性是NP完全的［5］，這意味著如果P≠NP成立，則無法在多項(xiàng)式時(shí)間內(nèi)解決SAT問題.這時(shí)從理論上分析該問題在最壞情況下的時(shí)間復(fù)雜性上界尤為重要，因?yàn)榇藭r(shí)對(duì)該問題上界的一個(gè)微小的改進(jìn)，例如從O(ck)改進(jìn)為O((c－ε)k)就會(huì)使得問題求解的算法在效率上獲得指數(shù)級(jí)別的提高.多年來，研究人員不斷改進(jìn)SAT問題及其約束子問題的求解算法在最壞情況下的時(shí)間復(fù)雜度上界［6-11］.以3SAT問題為例，最初Monien和Speckenmeyer在文獻(xiàn)［6］中給出了求解3SAT問題的上界為O(2m/3)，其中m是命題公式中的子句數(shù)目，目前獲得的最好上界為O(1.234m)［8］.SAT 問題理論上的不斷發(fā)展使得其系統(tǒng)的求解能力有了很大的提高.目前Zchaff、Survey Propagation等SAT求解系統(tǒng)已可以求解包含100 000個(gè)以上變量的SAT問題實(shí)例［12-14］.

NAESAT(not-all-equal satisfiability)問題作為SAT問題的一個(gè)重要擴(kuò)展，判斷是否存在一組真值賦值使得給定的命題公式為可滿足，并且使公式的每個(gè)子句中所有文字的取值不全為真.NAESAT和NAE-k-SAT(即公式中所有子句的長度都小于等于k，k≥3)都是 NP 完全問題［15-17］，其在集合分裂、最大割集等問題中都有著重要的應(yīng)用［16］.近來，從理論上研究NAESAT問題及其約束子問題在最壞情況下的時(shí)間復(fù)雜度上界受到了廣泛的關(guān)注.Monien等提出NAESAT問題可在O(1.587m)時(shí)間內(nèi)求解，其中m為公式中的子句數(shù)目［18］.Riege等將NAESAT問題算法在最壞情況下的時(shí)間復(fù)雜度上界改進(jìn)為 O(1.522 8m)［19］.2010 年，Shi等則運(yùn)用生物學(xué)方法提出了一種基于DNA的NAE-3SAT求解算法［20］.

事實(shí)上，算法的時(shí)間復(fù)雜度是根據(jù)問題實(shí)例的大小計(jì)算所得.而對(duì)于涉及命題公式的問題，問題實(shí)例的大小不僅依賴于公式中子句的數(shù)目，還依賴于變量的數(shù)目.以變量數(shù)目為參數(shù)研究NAESAT問題及其約束子問題在最壞情況下的時(shí)間復(fù)雜度上界，不僅可以從另一個(gè)角度衡量算法的好壞，而且在某種程度上更能準(zhǔn)確地反映出算法的性能.本文正是以此為著眼點(diǎn)，從變量數(shù)目的角度探討NAE-3SAT問題在最壞情況下的時(shí)間復(fù)雜度上界，提出了一個(gè)基于分支回溯(DPLL)的精確算法NAE.該算法給出了多種化簡規(guī)則，證明該算法在最壞情況下的時(shí)間復(fù)雜度上界為O(1.618n)，其中n為公式中的變量數(shù)目.

1 基本概念

文中符號(hào) x，y，z…表示布爾變量;符號(hào) l，l1，l2…表示文字.符號(hào) C，C1，C2…表示子句.符號(hào) F，F(xiàn)1，F(xiàn)2…表示CNF公式.

定義1 布爾變量.布爾變量(簡稱變量)取值為{true，false}.布爾變量x的度 φ(x)為變量x在公式中出現(xiàn)的次數(shù).把在公式中只出現(xiàn)一次的變量稱為singleton.

定義2 真值賦值.設(shè)變量集合X={x1，x2，…，xn}，定義在變量集合X上的真值賦值是一個(gè)函數(shù)μ:X→{true，false}.在變量集合X上存在2n組不同的真值賦值.文中把真值賦值簡稱為賦值.

定義3 文字.設(shè)x是一個(gè)變量，則稱x和?x為文字，其中稱x是正文字，?x是負(fù)文字.當(dāng)且僅當(dāng)變量x賦值為true，正文字x在賦值μ下取真值;當(dāng)且僅當(dāng)變量x賦值為false，文字?x在賦值μ下取真值;當(dāng)且僅當(dāng)F中恰好包含i個(gè)文字l，文字l稱為i-文字;當(dāng)且僅當(dāng)公式F中恰好包含i個(gè)文字l和j個(gè)文字?l，文字l稱為(i，j)-文字.公式中已經(jīng)被賦值為true(false)的文字稱為true(false)文字.

定義4 子句.子句由一組文字的析取而成，如C=l1∨l2∨ … ∨lk.當(dāng)且僅當(dāng)C中至少有一個(gè)文字取值為true，子句C在賦值μ下為可滿足.子句的長度是指子句中文字的個(gè)數(shù)，用符號(hào)|C|表示.把長度為k的子句稱為k-子句，長度為0的子句稱為空子句，用empty表示.空子句為不可滿足.

定義5 合取范式.合取范式(conjunctive normal form，CNF)由一組子句的合取而成，如F=C1∧C2∧ … ∧Ci.CNF范式也稱為公式F.當(dāng)且僅當(dāng)F中每一個(gè)子句都為可滿足，公式F在賦值μ下為可滿足，空公式為可滿足.

定義6 NAESAT問題.NAESAT問題對(duì)于一個(gè)給定的命題公式F，判斷是否存在一組賦值使得公式F為可滿足并且使公式F的每個(gè)子句中所有文字的取值不全為真，即要求公式F的每個(gè)子句中至少有一個(gè)文字為真，至少有一個(gè)文字為假.如果存在這樣的一組賦值，則稱公式F為NAE-可滿足的，否則稱公式F為NAE-不可滿足.使得公式F為NAE-可滿足的賦值稱為該公式的NAE-可滿足賦值.

如果給定的命題公式F中所有子句長度都小于等于3，則判斷是否存在一組賦值使得公式F為可滿足并且使公式F的每個(gè)子句中所有文字的取值不全為真的問題稱為NAE-3SAT問題.

另外需要說明的是，在文中符號(hào)F［x/false］表示將公式F中的x賦值為false，相應(yīng)地?x賦值為true后得到的子公式;符號(hào)F［x/?y］表示替換x=?y，即將公式F中的x用?y替換，?x用y替換后得到的子公式;符號(hào)F［z/y，t/?y］則表示替換z=y和t=?y，即同時(shí)將公式F中的z用y替換，t用?y替換，并相應(yīng)地將?z用?y替換，?t用y替換后得到的子公式.

2 算法NAE

2.1 化簡規(guī)則

在求解NAE-3SAT問題時(shí)，使用化簡規(guī)則對(duì)公式進(jìn)行約簡.應(yīng)用化簡規(guī)則的目的是減少公式中的變量數(shù)目，縮小搜索空間，提高算法的效率.

規(guī)則1:若公式F中存在1-子句，則進(jìn)行如下化簡:

規(guī)則2:若公式F中存在2個(gè)相同的子句，則進(jìn)行如下化簡:

規(guī)則3:若公式F中存在包含重復(fù)變量的子句，則進(jìn)行如下化簡:

1)(x∨x)∧F1→empty∧F1;

2)(x∨? x)∧F1→F1;

3)(x∨x∨x)∧F1→empty∧F1;

4)(x∨x∨? x)∧F1→F1;

5)(x∨? x∨y)∧F1→F1;

6)(x∨x∨y)∧F1→F1［y/? x］;

7)(true∨x∨x)∧F1→F1［x/false］;

8)(false∨x∨x)∧F1→F1［x/true］;

9)(true∨x∨? x)∧F1→F1;

10)(false∨x∨? x)∧F1→F1.

規(guī)則4:若公式F中存在2-子句，則進(jìn)行如下化簡:

1)(false∨false)∧F1→empty∧F1;

2)(true∨true)∧F1→empty∧F1;

3)(false∨true)∧F1→F1;

4)(false∨x)∧F1→F1［x/true］;

5)(true∨x)∧F1→F1［x/false］;

6)(x∨y)∧F1→F1［y/? x］.

規(guī)則5:若公式F中存在包含2個(gè)或以上true或false文字的3-子句，則進(jìn)行如下化簡:

1)(false∨false∨false)∧F1→empty∧F1;

2)(true∨true∨true)∧F1→empty∧F1;

3)(false∨true∨false)∧F1→F1;

4)(false∨true∨true)∧F1→F1;

5)(true∨true∨x)∧F1→F1［x/false］;

6)(false∨false∨x)∧F1→F1［x/true］;

7)(false∨true∨x)∧F1→F1.

規(guī)則6:若公式F中存在包含1個(gè)true或false文字和singleton的3-子句，則進(jìn)行如下化簡:

1)(true∨x∨y)∧F1→F1;

2)(false∨x∨y)∧F1→F1.

其中x或y為singleton或者x、y是singleton.

規(guī)則7:若公式F中存在包含2個(gè)或以上的singleton的3-子句，則進(jìn)行如下化簡:

其中 x、y、z或者 x、y是 singleton.

規(guī)則8:若公式F中存在2個(gè)子句，它們包含的變量都相同，則進(jìn)行如下化簡:

1)(x∨y∨z)∧(x∨y∨ ?z)∧F1→F1［y/? x］;

2)(x∨y∨z)∧(x∨?y∨?z)∧F1→F1［y/? z］;

3)(x∨y∨z)∧(? x∨? y∨? z)∧F1→(x∨y∨z)∧F1.

化簡規(guī)則的執(zhí)行時(shí)間均為多項(xiàng)式時(shí)間.一旦某個(gè)規(guī)則的條件滿足，該規(guī)則就可被執(zhí)行，且所有規(guī)則按照順序依次執(zhí)行，即后面的規(guī)則只有在前面的規(guī)則都不適用時(shí)才會(huì)被執(zhí)行.待處理的公式F重復(fù)地被以上8條規(guī)則化簡，直到所有規(guī)則的條件都不滿足為止.

定理1 以上8條化簡規(guī)則都是正確的，不會(huì)影響算法對(duì)公式F的NAE-可滿足性的判斷.

證明 由NAE-3SAT問題的定義可得規(guī)則1～5是正確的.在化簡過程中，把NAE-可滿足的子句直接從公式中消去，把NAE-不可滿足的子句賦為空子句，即empty.

規(guī)則6化簡包含一個(gè)true或false文字和singleton的子句，因?yàn)閷?duì)singleton的賦值不影響公式中其他變量的取值，可直接把singleton賦值為false(規(guī)則6中1))或true(規(guī)則6中2))使子句為NAE-可滿足.因此可直接把該子句從公式中消去.規(guī)則7與規(guī)則6類似.

在規(guī)則8的1)中，假設(shè)公式F包含2個(gè)子句為(x∨y∨z)和(x∨y∨? z)，如果 y=x=true 或 y=x=false，則2個(gè)子句中肯定有一個(gè)是NAE-不可滿足，所以必須使y=?x;規(guī)則8中2)與規(guī)則8中1)類似;規(guī)則8中3)，2個(gè)子句的文字皆為互補(bǔ)，由NAE-3SAT問題的定義可得若存在一組賦值使得其中一個(gè)子句為NAE-可滿足，則該賦值肯定也能使另一個(gè)子句為NAE-可滿足，所以可消去其中一個(gè)子句.因此規(guī)則8是正確的.

綜上所述，8條化簡規(guī)則都是正確的，化簡過程不影響公式的可滿足性，即若化簡后的公式F'∈NAE-3SAT，則可判定原公式F∈NAE-3SAT.

化簡后公式中將不存在1-子句、2-子句、包含重復(fù)變量的子句、包含2個(gè)或以上true或false文字的3-子句、包含1個(gè)true或false文字和singleton的3-子句、包含2個(gè)或以上的singleton的3-子句，且不會(huì)存在2個(gè)包含3個(gè)相同變量的3-子句.

2.2 NAE 算法框架

算法NAE的基本思想是給定任意的3-CNF公式F，首先利用2.1節(jié)中的化簡規(guī)則對(duì)公式進(jìn)行簡化;然后在化簡后的公式中選取某些變量進(jìn)行分支，分別判斷各個(gè)分支的NAE-可滿足性，進(jìn)而判斷出原公式的NAE-可滿足性;遞歸地執(zhí)行這個(gè)過程直到公式為空或者判定公式為NAE-不可滿足后停止.

算法的輸入是一個(gè)待處理的3-CNF公式F，輸出為true或者 false，true表示公式 F為 NAE-可滿足，false表示公式F為NAE-不可滿足.下面給出了算法的基本框架.

算法 NAE(F).

輸入:A formula F in 3-CNF.

輸出:If F is NAE-satisfiable，return true;

Else，return false.

1)Apply the rule 1～8 to F as long as one of them is applicable.

2)If F is empty，return true.

3)If F contains an empty clause，return false.

4)If F contains a clause with one true or false literal，C1=true∨x∨y or C1=false∨x∨y，then return(NAE(F［x/y］)∨NAE(F［x/? y］)).

5)If F contains two clauses C1=(x∨y∨z)，C2=(x∨y∨t)，then return(NAE(F［x/y］)∨NAE(F［x/? y］)).

6)If F contains two clauses C1=(x∨y∨z)and C2=(x∨? y∨t)，then return(NAE(F［x/y］)∨NAE(F［x/? y］)).

7)If F contains two clauses C1=(x∨y∨z)and C2=(? x∨? y∨t)，return(NAE(F［x/y］)∨NAE(F［x/? y］)).

8)Else choose a clause C1=(x∨y∨z)，return(NAE(F［x/y］)∨NAE(F［x/? y］)).

9)End.

定理2 算法NAE能正確地判斷一個(gè)3-CNF公式是否為NAE-可滿足.

證明 下面的證明過程將對(duì)算法的每一行進(jìn)行分析.

算法首先對(duì)公式F進(jìn)行化簡(第1步)，當(dāng)所有化簡規(guī)則都不可用時(shí)，進(jìn)行判斷:因?yàn)樵诨嗊^程中將NAE-可滿足的子句直接從公式中消去，所以若化簡后的公式F為空，則說明公式為NAE-可滿足，返回true(第2步);因?yàn)樵诨嗊^程中將NAE-不可滿足的子句賦為空子句，所以若化簡后公式F包含空子句，則說明公式為NAE-不可滿足，返回false(第3步).

若化簡后的公式F既不為空也不包含空子句，則算法進(jìn)入分支過程(第4～9步).分支過程根據(jù)化簡后的公式分幾種情況進(jìn)行:第4行:考慮公式中存在true或false文字的情況.由定理1可知包含該文字的子句一定為 C1=(true∨x∨y)或 C1=(false∨x∨y)，其中 x、y 為非 singleton.不失一般性，假設(shè)子句C1=(true∨x∨y)并對(duì)C1進(jìn)行分支，分別判斷2 個(gè)子公式 F［x/y］和F［x/? y］的 NAE-可滿足性，只要其中一個(gè)為NAE-可滿足，則可說明原公式為NAE-可滿足;第5～7步:考慮公式中存在2個(gè)子句包含2個(gè)相同變量的3種情況.對(duì)每一種情況，都進(jìn)行分支，分別判斷2個(gè)子公式F［x/y］和F［x/?y］的NAE-可滿足性;第8步:若以上情況都不存在，則公式中的任意2個(gè)子句間至多包含一個(gè)相同變量，算法任意選擇公式中的一個(gè)子句進(jìn)行分支，分別判斷 2 個(gè)子公式 F［x/y］和 F［x/? y］的 NAE-可滿足性.

綜上所述，算法NAE是正確并且完備的，能正確判斷一個(gè)給定的3-CNF公式是否為NAE-可滿足.

3 算法NAE時(shí)間復(fù)雜性分析

在本節(jié)中，用分支樹的方法來分析算法NAE的時(shí)間復(fù)雜性，并證明了其在最壞情況下的時(shí)間復(fù)雜度上界為O(1.618n)，其中n為公式中的變量數(shù)目.首先給出分支樹的概念.

分支樹是一個(gè)由i(i＞0)個(gè)結(jié)點(diǎn)組成的集合T，是一棵層級(jí)結(jié)構(gòu)樹［21-22］.分支樹的每個(gè)結(jié)點(diǎn)標(biāo)記一個(gè)CNF公式，其中一個(gè)特定的結(jié)點(diǎn)為根結(jié)點(diǎn)，標(biāo)記為公式F，除根結(jié)點(diǎn)外的其他結(jié)點(diǎn)被劃分為j(j≥0)個(gè)互不相交的有限集合T1，T2，…，Tj，每一個(gè)集合又都是分支樹，稱為根的子分支樹，分別標(biāo)記為公式F1，F(xiàn)2，…，F(xiàn)j.公式 F1，F(xiàn)2，…，F(xiàn)j是對(duì)公式F 中的某些變量進(jìn)行賦值后得到的公式，為公式F的子公式.分支樹的葉子結(jié)點(diǎn)標(biāo)記的是空公式或者包含空子句的公式.

分支樹中的每一個(gè)結(jié)點(diǎn)都有一個(gè)分支向量.設(shè)分支樹中某一個(gè)結(jié)點(diǎn)是F0，它的子結(jié)點(diǎn)分別是F1，F(xiàn)2，…，F(xiàn)k，則結(jié)點(diǎn) F0的分支向量為 τ(r1，r2，…，rk)，其中 ri=f(F0)－f(Fi)，f(Fi)(0≤i≤k)是公式Fi中變量的數(shù)目.每個(gè)結(jié)點(diǎn)所對(duì)應(yīng)的分支向量的值稱為該結(jié)點(diǎn)的分支數(shù)，可用式(1)計(jì)算:

所有結(jié)點(diǎn)分支數(shù)中最大的被定義為分支樹的分支數(shù)，用符號(hào)τmax表示.

定理3［7］設(shè)分支樹T的根結(jié)點(diǎn)標(biāo)記為公式F，則分支樹T中葉子的個(gè)數(shù)不超過(τmax)n，n是公式F中變量的數(shù)目.

因?yàn)榉种涞臉?gòu)造過程相當(dāng)于基于分支回溯算法的執(zhí)行過程，它們逐一地對(duì)公式F中的變量進(jìn)行賦值，直到確定公式的可滿足性為止.所以可用分支樹的方法對(duì)基于分支回溯的算法進(jìn)行時(shí)間復(fù)雜性的分析.假設(shè)算法在分支樹T中任意一個(gè)結(jié)點(diǎn)執(zhí)行的操作都是多項(xiàng)式時(shí)間，那么算法的執(zhí)行時(shí)間t為

式中:符號(hào)#{Tnode}表示分支樹T中結(jié)點(diǎn)的個(gè)數(shù)，符號(hào)#{Tleaves}表示分支樹T中葉子結(jié)點(diǎn)的數(shù)目，符號(hào)ploy(Fi)表示每個(gè)結(jié)點(diǎn)操作所用的時(shí)間是多項(xiàng)式時(shí)間.在本文中，忽略多項(xiàng)式時(shí)間.

定理4 算法NAE在最壞情況下的時(shí)間復(fù)雜度上界為O(1.618n)，其中n為公式中變量的數(shù)目.

證明 下面將對(duì)算法NAE的每一行進(jìn)行時(shí)間復(fù)雜度分析.

第1～3步:多項(xiàng)式時(shí)間內(nèi)時(shí)間復(fù)雜變?yōu)镺(1).

第4步:不失一般性，假設(shè)子句C1=true∨x∨y.在分支 F［x/y］中 C1=(true∨y∨y)，由化簡規(guī)則3中7)可得，y=false，因此消去x、y 2個(gè)變量.在分支F［x/? y］中 C1=(true∨? y∨y)，由化簡規(guī)則 3中9)可得子句C1可直接消去，因此消去x一個(gè)變量.執(zhí)行時(shí)間為O(τ(2，1)n)=O(1.618n).

第5步:在分支 F［x/y］中子句 C1=(y∨y∨z)，C2=(y∨y∨t)，由化簡規(guī)則 3 中 6)可得，z=t=? y，消去 x、z、t 3 個(gè)變量.分支 F［x/? y］中 C1=(? y∨y∨z)，C2=(? y∨y∨t)，由化簡規(guī)則 3 中5)可得子句C1、C2可直接消去，消去x一個(gè)變量.執(zhí)行時(shí)間為O(τ(3，1)n)=O(1.466n).

第6步:在分支F［x/y］中由化簡規(guī)則3中5)和6)可得，z=?y，消去 x、z 2個(gè)變量.同理在分支F［x/? y］中可消去 x、t 2 個(gè)變量.執(zhí)行時(shí)間為O(τ(2，2)n)=O(1.414n).

第7步:在分支F［x/y］中由化簡規(guī)則3中6)可得，z= ? y，t=y，消去 x、z、t 3 個(gè)變量.在分支F［x/? y］中由化簡規(guī)則3中5)可得子句 C1、C2可直接消去，消去 x一個(gè)變量.執(zhí)行時(shí)間為O(τ(3，1)n)=O(1.466n).

第8步:在分支F［x/y］中由化簡規(guī)則3中6)可得，z= ? y，消去 x、z 2 個(gè)變量.在分支 F［x/? y］中由化簡規(guī)則3中5)可得子句C1可直接消去，消去 x一個(gè)變量.執(zhí)行時(shí)間為 O(τ(2，1)n)=O(1.618n).

由以上分析可得，算法NAE最壞情況下的時(shí)間復(fù)雜度上界為O(1.618n).

4 結(jié)束語

本文從變量規(guī)模的角度探討了NAE-3SAT問題在最壞情況下的時(shí)間上界.針對(duì)NAE-3SAT問題新提出的8條化簡規(guī)則有效地提高了算法的時(shí)間效率.對(duì)于算法時(shí)間復(fù)雜性的分析，本文采用的是標(biāo)準(zhǔn)測度.近年來，眾多學(xué)者也在采用非標(biāo)準(zhǔn)測度來分析算法的時(shí)間復(fù)雜性，如measure and conquer方法.后續(xù)的工作將考慮利用非標(biāo)準(zhǔn)測度來分析算法的時(shí)間復(fù)雜性.

［1］COLMERAUER A.Opening the Prolog III universe［J］.Byte Magazine，1987，12(9):177-182.

［2］KLEER J.Exploiting locality in a TMS［C］//Proceedings of the 8th National Conference on Artificial Intelligence.Boston，USA，1990:264-275.

［3］GU J.Local search for satisfiability(SAT)problem［J］.IEEE Transactions on Systems， Man and Cybernetics，1993，23(4):1108-1129.

［4］李未，黃文奇.一種求解合取范式可滿足性問題的數(shù)學(xué)物理方法［J］.中國科學(xué):A輯，1994，24(11):1208-1217.LI Wei，HUANG Wenqi.A mathematic physical approach to the satisfiability problems［J］.Science in China:Series A，1994，24(11):1208-1217.

［5］COOK S A.The complexity of the theorem-proving procedures［C］//Proceedings of the Third Annual ACM Symposium on Theory of Computing.New York，USA，1971:151-158.

［6］MONIEN B，SPECKENMEYER E.Upper bounds for covering problems［R］.Universitat-Gesamtho Chschule-Paderborn:Reihe Theoretische Informatik，1980.

［7］HIRSCH E A.New worst-case upper bounds for SAT［J］.Journal of Automated Reasoning，2000，24(4):397-420.

［8］YAMAMOTO M.An improved O(1.234m)-time deterministic algorithm for SAT［J］.Lecture Notes in Computer Science，2005，3827:644-653.

［9］MONIEN B，SPECKENMEYER E.Solving satisfiability in less than 2n steps［J］.Discrete Applied Mathematics，1985，10(3):287-295.

［10］BRUEGGEMANN T，KERN W.An improved local search algorithm for 3-SAT［J］.Theoretical Computer Science，2004，329(1/2/3):303-313.

［11］DANTSIN E，GOERDT A，HIRSCH E A，et al.Adeterministic(2-2/(k+1))n algorithm for k-SAT based on local search［J］.Theoretical Computer Science，2002，289(1):69-83.

［12］ZHANG Lintao，MADIGN C F，MOSKEWICZ M H，et al.Efficient conflict driven learning in a Boolean satisfiability solver［C］//Proc of the ACM/IEEE ICCAD 2001.New York，USA，2001:279-285.

［13］ZECCHINA R，MEZARD M，PARISI G.Analytic and algorithmic solution of random satisfiability problems［J］.Science，2002，297(5582):812-815.

［14］ZECCHINA R，MONASSON R，KIRKPATRICK S，et al.Determining computational complexity from characteristic phase transitions［J］.Nature，1999，400(6740):133-137.

［15］THOMAS J S.The complexity of satisfiability problems［C］//Conference Record of the Tenth Annual ACM Symposium on Theory of Computing.New York，USA，1978:216-226.

［16］PORSCHEN S，RANDERATH B，SPECKENMEYER E.Linear time algorithms for some not-all-equal satisfiability problems［C］//Proceedings of the 6th International Conference on Theory and Application of Satisfiability Testing(SAT2003).Santa Margherita Ligure，Italy，2003:172-187.

［17］WALSH T.The interface between P and NP:COL，XOR，NAE，1-in-k，and Horn SAT［C］//Eighteenth National Conference on Artificial Intelligencet.Edmonton，Canada，2002:685-700.

［18］MONIEN B，SPECKENMEYER E，VORNBERGER O.Upper bounds for covering problems［J］.Methods of Operations Research，1981，43:419-431.

［19］RIEGE T，ROTHE J，SPAKOWSKI H.An improved exact algorithm for the domatic number problem［J］.Information Processing Letters，2006，101(3):101-106.

［20］SHI Nungyue，CHU Chihping.A DNA-based algorithm for the solution of not-all-equal 3-SAT problem［C］//ASE International Conference on Information Engineering.Taiyuan，China，2009:94-97.

［21］ZHOU Junping，YIN Minghao，ZHOU Chunguang.New worst-case upper bound for#2-SAT and#3-SAT with the number of clauses as the parameter［C］//Proceedings of 24rd AAAI Conference on Artificial Intelligence.Atlanta，USA，2010:217-222.

［22］周俊萍，殷明浩，周春光，等.最壞情況下#3-SAT問題最小上界［J］.計(jì)算機(jī)研究與發(fā)展，2011，48(11):2055-2063.ZHOU Junping，YIN Minghao，ZHOU Chunguang，et al.The worst case minimized upper bound in#3-SAT［J］.Journal of Computer Research and Development，2011，48(11):2055-2063.