最壞情況下Min-2SAT問題的上界

谷文祥，姜蘊暉，周俊萍，殷明浩

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

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

1 基礎知識

1.1 基本概念

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

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

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

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

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

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

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

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

用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-子句的個數，也就是說，如果變量 x的度為 k，則#2(F，x)+#2(F，? x)=k.

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

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

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

1.2 復雜性分析方法

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

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

分支樹中的每一個結點都有1個分支向量.設分支樹中某一個結點是F0，它的子結點分別是F1，F2，…，Fk.則結點 F0的分支向量為 τ =(r1，r2，…，rk)，其中 ri=f(F0)－f(Fi)，f(F0)=m(F0)是公式F0中子句的數目，f(F0)=n(F0)是公式F0中變量的數目.

每個結點的分支向量的值被稱為結點的分支數，可用式(1)計算.

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

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

若從變量數目的角度考慮，算法的執行時間t為

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

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

2 化簡規則

在給出求解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至多出現在一個不含x2的2-字句中，令α和β分別為F［x2］和F［?x2］中通過化簡規則對x1所賦的布爾值(true或者false)，則根據α和β的值將公式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］).

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

根據化簡規則，可以得到下面的引理.

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

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

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

證明 考慮變量a所有可能出現的情況.

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

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

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

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

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

6)當(a∨x)∧(? a∨x1)∧(? a∨x2)∧a 時，若x=0，則由化簡規則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中，首先，應用化簡規則對公式進行化簡;第2步是指如果公式中只包含永真子句T，則返回公式中子句的數目;第3步考慮公式中包含組件的情況，即將公式分支成2個更簡單的公式并對其遞歸調用;最后根據每次遞歸調用返回的結果得到最后的結果.定理1中給出了算法的時間復雜度.

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

證明

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

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

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

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

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

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

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

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

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

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

c)下面需要考慮的是對F中的一個變量進行分支時，化簡規則會在一個分支中對其全部鄰居賦值的情況.考慮一個變量 x，N({x})={a，b，c}.如果|N({a，b，c})|≥5，則 對 x 分 支 的 復 雜 度 為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分支的復雜度為O(τ(6，6)n)=O(1.122 5n)，后一種情況對x賦值的復雜度為O(τ(4，10)n)?O(1.112 0n).

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

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

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

4 結束語

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

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

［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，FERNAU 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.