谷文祥，傅琳璐，周俊萍，姜蘊暉

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

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

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

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

1 基本概念

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

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

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

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

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

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

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

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

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

2 算法NAE

2.1 化簡規(guī)則

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

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

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

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

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-子句，則進行如下化簡:

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個或以上true或false文字的3-子句，則進行如下化簡:

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個true或false文字和singleton的3-子句，則進行如下化簡:

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

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

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

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

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

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

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í)行時間均為多項式時間.一旦某個規(guī)則的條件滿足，該規(guī)則就可被執(zhí)行，且所有規(guī)則按照順序依次執(zhí)行，即后面的規(guī)則只有在前面的規(guī)則都不適用時才會被執(zhí)行.待處理的公式F重復地被以上8條規(guī)則化簡，直到所有規(guī)則的條件都不滿足為止.

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

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

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

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

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

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

2.2 NAE 算法框架

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

算法的輸入是一個待處理的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能正確地判斷一個3-CNF公式是否為NAE-可滿足.

證明 下面的證明過程將對算法的每一行進行分析.

算法首先對公式F進行化簡(第1步)，當所有化簡規(guī)則都不可用時，進行判斷:因為在化簡過程中將NAE-可滿足的子句直接從公式中消去，所以若化簡后的公式F為空，則說明公式為NAE-可滿足，返回true(第2步);因為在化簡過程中將NAE-不可滿足的子句賦為空子句，所以若化簡后公式F包含空子句，則說明公式為NAE-不可滿足，返回false(第3步).

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

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

3 算法NAE時間復雜性分析

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

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

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

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

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

因為分支樹的構(gòu)造過程相當于基于分支回溯算法的執(zhí)行過程，它們逐一地對公式F中的變量進行賦值，直到確定公式的可滿足性為止.所以可用分支樹的方法對基于分支回溯的算法進行時間復雜性的分析.假設算法在分支樹T中任意一個結(jié)點執(zhí)行的操作都是多項式時間，那么算法的執(zhí)行時間t為

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

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

證明 下面將對算法NAE的每一行進行時間復雜度分析.

第1～3步:多項式時間內(nèi)時間復雜變?yōu)镺(1).

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

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

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

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

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

4 結(jié)束語

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

［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ù)學物理方法［J］.中國科學: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］.計算機研究與發(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.