谷文祥，姜蘊(yùn)暉，周俊萍，殷明浩

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

人工智能研究領(lǐng)域存在著很多計算困難的問題，如 SAT(satisfiability)問題、QBF(quantified boolean formula)問題、智能規(guī)劃問題、模型診斷問題等.若P≠NP成立，人們將無法為這些問題找到多項式時間的求解算法.這時從理論上分析這些問題在最壞情況下的時間復(fù)雜性上界尤為重要，因為此時對該上界的一個微小的改進(jìn)，例如從O(ck)改進(jìn)為O((c－ε)k)，就會使得問題求解的算法在效率上獲得指數(shù)級別的提高.以SAT問題為例，作為第一個被證明是NP完全的問題，改進(jìn)其在最壞情況下的時間上界受到了研究人員的廣泛關(guān)注.MaxSAT(maximum satisfiability)問題是SAT問題的擴(kuò)展，它指的是給定一個命題邏輯公式，找到一組使真值賦值同時滿足最多的子句.與SAT問題一樣，MaxSAT問題在計算機(jī)科學(xué)領(lǐng)域有著十分重要的地位，因為它是求解人工智能和組合優(yōu)化問題的基礎(chǔ)［1-2］.當(dāng)公式中子句的長度至多為2時稱之為Max-2SAT(maximum two-satisfiability)問題，它是一個NP完全的問題［3］.近年來，眾多學(xué)者對Max-2SAT問題進(jìn)行了研究［4-7］，已經(jīng)將其最壞情況下的上界縮小到O(2m/6.312)［8］.與 MaxSAT 問 題 相 對 的 是 MinSAT(minimum satisfiability)問題，它指的是給定一個命題邏輯公式，找到一組使真值賦值同時滿足最少的子句.雖然人們對MaxSAT問題已經(jīng)做了非常多的研究，但對MinSAT問題的研究卻并不深入.目前，對MinSAT問題的求解主要采用近似方法［9-10］.此外，LI等在文獻(xiàn)［11］中將MinSAT問題轉(zhuǎn)換為Max-SAT問題，給出了一個MinSAT求解器.事實上，在求解某些組合優(yōu)化問題時，將其轉(zhuǎn)化為MinSAT問題比轉(zhuǎn)化為MaxSAT問題有著更快的速度，所以研究MinSAT問題也有著十分重要的理論意義和實際應(yīng)用價值.正如人們對MaxSAT問題的研究主要集中在Max-2SAT問題上，筆者同樣著眼于MinSAT問題中子句長度不超過2的情況，即對Min-2SAT問題進(jìn)行研究，提出了一種求解Min-2SAT問題的算法，并證明了算法在O(1.134 3m)時間內(nèi)可解.

1 基礎(chǔ)知識

1.1 基本概念

為了討論方便，首先介紹本文需要的相關(guān)概念.

定義1 真值賦值.給定一個布爾變量集合V={x1，x2，…，xn}，定義在V上的真值賦值是一個函數(shù)μ:V→{true，false}.每個真值賦值可以用一個n元布爾向量表示.對V中任意一個布爾變量xi，若它在真值賦值μ下取真，則μ(xi)=1，否則μ(xi)=0.

定義2 文字.對任意一個布爾變量x，稱符號x和?x是其文字，其中x是正文字，?x是負(fù)文字.

定義3 純文字.給定一個公式F和F中任意一個布爾變量x，若x只以正文字或負(fù)文字的形式出現(xiàn)在公式F中，則稱x為純文字.

定義4 子句.子句是若干文字的析取，用集合C 表示，C=l1∨l2∨…∨lk，其中 l1，l2，…，lk是文字.子句C中文字的個數(shù)稱為子句的長度，記作|C|.

k-子句是指子句長度為k的子句.永真子句T指的是對子句的變量任意賦值時子句都是可滿足的.

定義5 CNF范式.CNF范式是若干子句的合取，用 F 表示，F(xiàn)=C1∧C2∧…∧Ci，其中 C1，C2，…，Ci是子句.CNF范式F也稱為公式，當(dāng)且僅當(dāng)每一個子句都可滿足時，公式F在賦值μ下可滿足.

公式F同時可滿足的最少的子句數(shù)記為PesVal(F).稱文字l出現(xiàn)在子句中如果子句包含l，稱變量x出現(xiàn)在子句中如果子句包含x或?x.本文中，用#(F，l)表示文字l出現(xiàn)在公式F中的次數(shù)，用#k(F，l)表示文字l在公式F中的k-子句中出現(xiàn)的次數(shù).

用F［l］表示將F中所有包含l的子句替換為T，消去所有?l和所有 F中的空子句.用F［l1=l2］表示將所有的l1用l2替代，并將所有的?l1用?l2替代.

定義6 Min-2SAT問題.給定一個命題邏輯公式F，找到一組使真值賦值滿足最少的子句，如果子句的長度至多為2，則稱其為Min-2SAT問題.

定義7 變量的度.變量x的度是指包含x的2-子句的個數(shù)，也就是說，如果變量 x的度為 k，則#2(F，x)+#2(F，? x)=k.

定義8 變量的鄰居.變量x的鄰居是指所有和x一起出現(xiàn)在同一個2-子句的變量.

用V(F)表示F中所有變量的集合，對于變量集合V0?V(F)，用N(F，V0)來表示變量集合V0的所有鄰居.

用G(F)表示一個無向圖，V(F)是所有頂點(diǎn)的集合，如果F中2個變量出現(xiàn)在同一個2-子句中，則在這2個頂點(diǎn)之間添加1條邊.

1.2 復(fù)雜性分析方法

本節(jié)介紹分支算法的復(fù)雜性分析方法，首先給出分支樹的概念［12］.

分支樹是由i(i＞0)個結(jié)點(diǎn)組成的有限集合Q，其中一個特定的結(jié)點(diǎn)為根結(jié)點(diǎn)，標(biāo)記為公式F，除根結(jié)點(diǎn)以外的其他結(jié)點(diǎn)被劃分為j(j≥0)個互不相交的有限集合 Q1，Q2，…，Qj，分別標(biāo)記為公式 F1，F(xiàn)2，…，F(xiàn)j.其中每一個集合又都是分支樹，稱為根結(jié)點(diǎn)的子分支樹，分別表示對公式F中的某些變量進(jìn)行賦值后得到的公式，即公式F的子公式.葉子結(jié)點(diǎn)標(biāo)記的公式為空公式或者其中存在一個空子句.

分支樹中的每一個結(jié)點(diǎn)都有1個分支向量.設(shè)分支樹中某一個結(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(F0)=m(F0)是公式F0中子句的數(shù)目，f(F0)=n(F0)是公式F0中變量的數(shù)目.

每個結(jié)點(diǎn)的分支向量的值被稱為結(jié)點(diǎn)的分支數(shù)，可用式(1)計算.

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

由分支樹的定義可以看出，分支樹的構(gòu)造過程相當(dāng)于基于DPLL(Davis-Putnam-Logemann-Loveland)算法的執(zhí)行過程.算法逐一對公式F中的變量進(jìn)行賦值，直到確定任意一個賦值滿足或不滿足公式F為止.假設(shè)基于DPLL的算法在分支樹T中任意一個結(jié)點(diǎn)執(zhí)行的操作都是多項式的，那么從子句數(shù)目的角度考慮，算法的執(zhí)行時間t為

若從變量數(shù)目的角度考慮，算法的執(zhí)行時間t為

用F表示2-CNF公式，用Ni(F)表示在公式F的2-子句中出現(xiàn)i次的變量的個數(shù).很容易得到

式中:K2(F)表示 F中2-子句的數(shù)目.根據(jù)文獻(xiàn)［13］可以對其稍作修改，得到新的復(fù)雜性測度為

2 化簡規(guī)則

在給出求解Min-2SAT問題的算法之前，首先給出一個化簡算法如下.

化簡算法Simplify(F).

輸入:一個2-CNF范式F.

輸出:一個化簡后的2-CNF范式F.

1)如果F=F0∪{C，D}，并且對于一個文字 l有 C{l}=D{? l}，則返回 Simplipy(F0∪{C{l}，T}).

2)如果F中存在一個文字l滿足#(F，?l)=0，則返回 Simplipy(F［? l］).

3)如果F中存在一個文字l滿足#1(F，l)≥#(F，? l)，則返回 Simplipy(F［? l］).

4)如果F中存在2個變量x1和x2，并且x1至多出現(xiàn)在一個不含x2的2-字句中，令α和β分別為F［x2］和F［?x2］中通過化簡規(guī)則對x1所賦的布爾值(true或者false)，則根據(jù)α和β的值將公式F化簡的方法為:

a)如果 α =false，β =false，則返回 Simplipy(F［? x1］).

b)如果 α =false，β=true，則返回 Simplipy(F［x1=? x2］).

c)如果 α=true，β=false，則返回 Simplipy(F［x1=x2］).

d)如果 α =true，β =true，則返回 Simplipy(F［x1］).

對于給定的范式，重復(fù)使用化簡算法Simplify(F)對其進(jìn)行化簡，直到范式不能再應(yīng)用算法中任何一條化簡規(guī)則為止.這樣在求解Min-2SAT問題時可以減少算法需要考慮的情況，以減弱算法的復(fù)雜性.

根據(jù)化簡規(guī)則，可以得到下面的引理.

引理1 令F是一個2-CNF范式，F(xiàn)'=Simplify(F)，則F'中不包含度至多為2的變量.

證明 若變量的度為1，則可通過化簡算法Simplify(F)中化簡規(guī)則2)對其化簡;若變量的度為2，則可通過化簡規(guī)則4)進(jìn)行化簡.因此公式化簡后只包含度至少為3的變量.

引理2 令F是化簡后的公式，a、x是鄰居，a的度為3，則在 F［x］和 F［? x］中，至少有一個化簡規(guī)則會對a賦值.

證明 考慮變量a所有可能出現(xiàn)的情況.

1)當(dāng)(a∨x)∧(a∨x1)∧(? a∨x2)時，若 x=0，則由化簡規(guī)則3)可知a=1.

2)當(dāng)(a∨x)∧(? a∨x1)∧(? a∨x2)時，若x=1，則由化簡規(guī)則2)可知a=0.

3)當(dāng)(a∨x)∧(a∨x1)∧(a∨x2)∧? a 時，若x=0，則由化簡規(guī)則1)可知消除了a和?a，再由化簡規(guī)則2)可知a=1.

4)當(dāng)(a∨x)∧(a∨x1)∧(a∨x2)∧? a∧? a時，若x=1，則由化簡規(guī)則3)可知a=0.

5)當(dāng)(a∨x)∧(a∨x1)∧(? a∨x2)∧? a 時，若x=1，則由化簡規(guī)則3)可知a=0.

6)當(dāng)(a∨x)∧(? a∨x1)∧(? a∨x2)∧a 時，若x=0，則由化簡規(guī)則3)可知a=1.

由于公式F已化簡，所以不存在其他情況，引理得證.

3 算法MinSATAlg

本文給出一個求解Min-2SAT問題的算法Min-SATAlg，它是一個典型的分支算法.具體算法描述如下.

輸入:一個2-CNF范式F.

輸出:PesVal(F).

1)F=Simplify(F).

2)如果F只包含T字句，則返回L(F).

3)如果F=F1∪F2，并且F1和F2沒有相同的變量，則返回MinSATAlg(F1)+MinSATAlg(F2).

4)選擇變量 x 使 τ(r(F)－ r(Simplify(F［x］))，r(F)－r(Simplify(F［? x］)))最小，并返回min(MinSATAlg(F［x］)，MinSATAlg(F［? x］)).

在算法MinSATAlg中，首先，應(yīng)用化簡規(guī)則對公式進(jìn)行化簡;第2步是指如果公式中只包含永真子句T，則返回公式中子句的數(shù)目;第3步考慮公式中包含組件的情況，即將公式分支成2個更簡單的公式并對其遞歸調(diào)用;最后根據(jù)每次遞歸調(diào)用返回的結(jié)果得到最后的結(jié)果.定理1中給出了算法的時間復(fù)雜度.

定理2 給定一個2-CNF范式，算法 Min-SATAlg在O(1.134 3m)時間內(nèi)返回公式中同時可以滿足的最少的子句數(shù).

證明

1)當(dāng)公式F中包含一個度大于6的變量時.由化簡規(guī)則可知，F(xiàn)中的所有變量至少出現(xiàn)在2個沒有x出現(xiàn)的2-子句中.度至少為3的變量使r至少減少1/2，這是因為Ni的2個系數(shù)的差至少為1/2.這樣，當(dāng)對x賦值后，r至少減少w(w/2(x被消去)+w/2(x的鄰居的度減少)).因此，對x進(jìn)行分支的復(fù)雜度至少為O(τ(6，6)m)=O(1.122 5m).

2)當(dāng)公式F中變量的度都不超過5時.令x是一個度為5的變量，用kij表示在公式F中出現(xiàn)j次且和x一起出現(xiàn)i次的變量個數(shù)，其中1≤i≤j≤5.由于F已化簡，所以當(dāng)j≤2或j－i≤1時kij=0.由于x出現(xiàn)在5個2-子句中，所以有

k13+k14+k15+2k24+2k25+3k35=5.

對于共出現(xiàn)j次并且與x一起出現(xiàn)i次的變量，在對x賦值后其出現(xiàn)在2-子句中的次數(shù)為j－i.令F'為對F中的變量x賦值后得到的公式，則有

由此可見，對 x進(jìn)行分支的復(fù)雜度至少為O(τ(5.5，5.5)m)=O(1.134 3m).

3)當(dāng)公式F中變量的度都不超過4時.與第2種情況類似可得到

因此，對x進(jìn)行分支的復(fù)雜度至少為O(τ(5.5，5.5)m)=O(1.134 3m).

4)當(dāng)公式F中所有變量的度均為3時.在這種情況下很容易看出r(F)=N(F)，所以只需要證明以變量數(shù)目為參數(shù)時的復(fù)雜度為O(τ(6，6)n)=O(1.122 5n).由于變量的度均為3，所以變量的個數(shù)必為偶數(shù)，F(xiàn)的每一次分支都為(2k，2l)，其中k和l都是整數(shù).

a)如果公式F中包含3個變量且其中任意2個變量都出現(xiàn)在同一個2-子句中，則在圖G(F)中形成1個三角形.令a、b、c為形成三角形的3個變量，可以看出N({a，b，c})包含至少2個變量，至少1個鄰居只和{a，b，c}中的1個一起出現(xiàn)，將其標(biāo)記為d并和c一起出現(xiàn)，如圖1(a)所示.對d進(jìn)行分支的復(fù)雜度為 O(τ(6，6)n)=O(1.122 5n).這是因為對d賦值后，c只和a、b一起出現(xiàn)，或出現(xiàn)在單元子句中，化簡規(guī)則或者對c直接賦值，或者用包含a、b的子句替代含c的子句.對于前一種情況，a、b也會通過化簡規(guī)則被消去，對于后一種情況通過化簡規(guī)則4)會消去a、b中的一個.所以對d賦值后還會至少再消去4個變量，因此對d進(jìn)行分支的復(fù)雜度為O(τ(6，6)n)=O(1.122 5n).

b)考慮圖G(F)中不包含三角形的情況.假設(shè)F 包含一個變量 x，其鄰居為 a、b、c，這樣在 F［x］和F［? x］中化簡規(guī)則會對 a、b、c中至少一個賦值.很容易看出對x進(jìn)行分支的復(fù)雜度為O(τ(6，6)n)=O(1.122 5n).

c)下面需要考慮的是對F中的一個變量進(jìn)行分支時，化簡規(guī)則會在一個分支中對其全部鄰居賦值的情況.考慮一個變量 x，N({x})={a，b，c}.如果|N({a，b，c})|≥5，則 對 x 分 支 的 復(fù) 雜 度 為O(τ(4，10)n)?O(1.112 0n).如果|N({a，b，c})|＜5，這就意味著或者存在一個變量y≠x并且N(y)={a，b，c}(如圖1(b)所示)，或者存在2 個變量y，z≠x并且|N(y)∪{a，b，c}|=2，|N(z)∪{a，b，c}|=2(如圖1(c)所示).前一種情況對b分支的復(fù)雜度為O(τ(6，6)n)=O(1.122 5n)，后一種情況對x賦值的復(fù)雜度為O(τ(4，10)n)?O(1.112 0n).

圖1 情況4)的不同例子Fig.1 Different cases in 4)

由此可見，以變量數(shù)目為參數(shù)時的復(fù)雜度為O(τ(6，6)n)=O(1.122 5n).從而得到一個化簡后的公式F只包含度為3的變量時，則對其中一個變量進(jìn)行分支的時間復(fù)雜度為 O(τ(6，6)m)=O(1.122 5m).

綜上所述，給定一個2-CNF范式，算法 Min-SATAlg在O(1.134 3m)時間內(nèi)返回公式中同時可以滿足的最少的子句數(shù)，即定理2得證.

4 結(jié)束語

MaxSAT問題是求解人工智能和組合優(yōu)化問題的基礎(chǔ)，而在求解某些組合優(yōu)化問題時，將其轉(zhuǎn)化為MinSAT問題比MaxSAT問題有著更快的速度，因此求解MinSAT問題并分析其復(fù)雜度有著很高的實際價值.本文研究了MinSAT問題中每個子句長度不大于2的情況，即Min-2SAT問題，提出了一個求解Min-2SAT問題的算法并證明了算法的時間復(fù)雜度為O(1.134 3m)，其中m為公式中子句的數(shù)目.筆者運(yùn)用了一種新的復(fù)雜性測度來測量算法的運(yùn)行時間.另外還證明了對于每個變量至多出現(xiàn)在3個2-子句中的情況，其最壞情況下的時間復(fù)雜度為O(1.122 5n)，其中n為變量的數(shù)目.

在今后的工作中，可以進(jìn)一步修正復(fù)雜性測度或通過加入沖突子句等方法，來改善算法并減少算法的時間復(fù)雜度.

［1］HANSEN P，JAUMARD B.Algorithms for the maximum satisfiability problem［J］.Computing，1990，44(4):279-303.

［2］WALLACE R J.Enhancing maximum satisfiability algorithms with pure literal strategies［C］//Proceedings of the 11th Biennial Conference of the Canadian Society for Computational Studies of Intelligence on Advances in Artificial Intelligence.London，UK:Springer-Verlag，1996:388-401.

［3］NIEDERMEIER R，ROSSMANITH P.New upper bounds for MaxSat［C］//Proceedings of the 26th International Colloquium on Automata，Languages and Programming.London，UK:Springer-Verlag，1999:575-584.

［4］GRAMM J，HIRSCH E A，NIEDERMEIER R，et al.Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT［J］.Discrete Applied Mathematics，2003，130(2):139-155.

［5］KNEIS J，ROSSMANITH P.A new satisfiability algorithm with applications to Max-Cut:Technical Report AIB2005-08［R］.Aachen，Germany:Department of Computer Science，RWTH Aachen University，2005.

［6］KULIKOV A S，KUTZKOV K.New bounds for MAX-SAT by clause learning［C］//2nd International Symposium on Computer Science in Russia.Ekaterinburg，Russia，2007:194-204.

［7］BINKELE-RAIBLE D，F(xiàn)ERNAU H.A new upper bound for Max-2-SAT:a graph-theoretic approach［J］.Journal of Discrete Algorithms，2010，8(4):388-401.

［8］GASPERS S，SORKIN G B.A universally fastest algorithm for Max 2-Sat，Max 2-CSP，and everything in between［J］.Journal of Computer and System Sciences，2012，78(1):305-335.

［9］AVIDOR A，ZWICK U.Approximating MIN 2-SAT and MIN 3-SAT［J］.Theory of Computing Systems，2005，38(3):329-345.

［10］MARATHE M V，RAVI S S.On approximation algorithms for the minimum satisfiability problem［J］.Information Processing Letters，1996，58(1):23-29.

［11］LI Chumin，MANYA F，QUAN Zhe，et al.Exact MinSAT solving［C］//Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing.Berlin/Heidelberg， Germany:Springer-Verlag， 2010:363-368.

［12］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 the Twenty-Fourth AAAI Conference on Artificial Intelligence.Atlanta，USA，2010.

［13］KOJEVNIKOV A，KULIKOV A S.A new approach to proving upper bounds for MAX-2-SAT［C］//Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms.New York，USA:ACM，2006:11-17.