基于尋找可滿足2-SAT子問題的SAT算法

摘 要:可滿足問題(SAT)是一個NP-Hard問題。提出了一種求解SAT的新算法(FFSAT)。該算法將SAT問題轉換為尋找一個可滿足的2-SAT子問題。SAT問題雖然是NP完全問題，但是當所有子句長度不大于2時，SAT問題可以在線性時間求解。使用2-SAT算法-BinSat求解2-SAT子問題，當它不滿足時，根據賦值選擇新的2-SAT子問題。實驗結果表明，采用本算法的結果優于UnitWalk。

關鍵詞:SAT問題; 2-SAT子問題; 2-SAT算法

中圖分類號:TP301.6

文獻標志碼:A

文章編號:1001-3695(2010)02-0462-03

doi:10.3969/j.issn.1001-3695.2010.02.015

New SAT solver based on finding satisfiable 2-SAT sub problem

FU Yang-chun， ZHOU Yu-ren

(School of Computer Science Engineering， South China University of Technology， Guangzhou 510006， China)

Abstract:Satisfiability (SAT) problem is one of the NP-Hard problems. This paper introduced a new SAT solver called FSSAT. This SAT solver solved the problem by searching a satisfiable 2-SAT sub problem. SAT was NP-complete， but it can be solved in linear time when the given formula contains only binary clauses (2-SAT).BinSat(2-SAT solver) was used to solve the 2-SAT sub problem and improved the 2-SAT sub problem according to the truth assignment. The experimental results show that the solver outperforms UnitWalk.

Key words:SAT problem; 2-SAT sub problem; 2-SAT solver

0 引言

命題邏輯合取范式(CNF)的可滿足性問題(SAT)是當代理論計算機科學的核心問題。SAT問題是典型的NP完全問題[1]，其快速求解方法不僅具有重要的理論意義，還有著直接應用;它的研究成果廣泛應用于電子設計自動化、人工智能等領域 ，可解決自動測試向量生成、時序分析、邏輯驗證、等價性檢查、智能規劃等問題。

目前SAT問題的算法有完全算法和不完全算法兩大類[2]。前者主要是以Davis-Putnam[3]算法為原型的一類DP算法，后者主要基于局部搜索算法。完全算法雖然能保證判定SAT問題的可滿足性，但是在最壞情況下將達到指數級的時間復雜度，不適合求解大規模的SAT問題。局部搜索算法雖然不能判定一個SAT問題不滿足，但在SAT問題可滿足時可快速得到它的一個解，因此近年來獲得了廣泛的研究，其成果豐富，如Selman等人的GSAT[4]和WALKSAT[5]、Edward的UnitWalk[6]等。

雖然SAT問題是NP完全問題，當子句長度大于等于3時尋找其解需要花費指數級的時間，但在每個子句的長度小于等于2(2-SAT)的情況下是可以在線性時間判定其可滿足性的。基于單元歸結的BinSat[7]算法是目前解決2-SAT問題的最好算法。Zhang等人[8]將其應用到DPLL算法中，有效地減少了搜索空間。UnitWalk也通過使用2-SAT算法減少了變量翻轉的次數?？蓾M足的2-SAT子問題的解也是原SAT問題的一個解?；谶@個思想，本文提出一種新的基于尋找可滿足2-SAT子問題的局部搜索算法，并與WALKSAT、UnitWalk進行實驗對比。實驗結果表明該算法優于UnitWalk算法。

1 SAT問題描述和轉換

1.1 SAT問題描述

下面給出SAT問題的一般性描述和本文用到的符號。

定義1 變元集合

用符號X表示命題變元的集合，若X由n個變元x1，x2，x3，…，xn組成，那么X={x1，x2，x3，…，xn}，用n=|X|表示變元集合的大小。

定義2 真值指派

X的一個真值指派A是映射X→{0，1}n，變元xi在A下為真，可以表示為A(xi)=1，否則A(xi)=0。因此在X上存在2n個不同的真值指派。

定義3 文字

對任意變元xi，符號xi和xi是其文字，稱xi是正文字，xi是反文字。用L 表示文字集。文字xi在真值指派A下取真值當且僅當A(xi)=1;文字xi真值指派A下取真值當且僅當A(xi)=0。

定義4 子句

X上的子句是X上的一些文字的析取，用c表示，c=∨ki=1li。子句在指派A下取真值(或稱在指派A下是可滿足的)，當且僅當子句包含的文字中至少有一個在指派A下取真值。k=|c|表示子句c中的文字數，稱為子句長度。一個長度為k的子句是一個k-子句。

定義5 子句集

子句集C是由X上的子句組成的集合，C={c1，c2，…，cm}。m=|C|表示子句集中子句的個數。子句集C在指派A下是可滿足的，當且僅當C中所有的子句c在指派A下都是取真值的。

定義6 合取范式(conjectured normal formula，CNF)

X上的合取范式F是X上的一些子句的合取，F=∧mj=1cj。合取范式F在指派A下取真值(或者稱在指派A下是可滿足的)，當且僅當F中包含的所有子句c在指派A下都是取真值的。

定義7 SAT問題

給定一個命題變元的集合X={x1，x2，x3，…，xn}和一個X上的合取范式F=∧mj=1cj，問是否存在一個關于X的真值指派A，使得F是可滿足的。

定義8 子句的文字集

子句c中包含的文字構成的集合記為V(c)，即V(c)={l1，l2，…，lk}，若c=l1∨l2∨…∨lk。

定義9 2-SAT子問題

給定SAT問題T，其命題變元的集合為X={x1，x2，x3，…，xn}，子句集為C={c1，c2，…，cm}，稱T′是其2-SAT子問題。如果其命題變元的集合是X，子句集為C′={c′1，c′2，…，c′m}，且V(c′j)V(cj)∧|c′j|=2，j∈{1，2，3，…，m}。

1.2 SAT問題的轉換

根據2-SAT子問題T′的定義可以得出，如果T′是可滿足的，那么它的解也是原SAT問題T的一個解。于是求解SAT問題可以轉換為:尋找一個2-SAT子問題T′，然后使用BinSat判斷其可滿足性，若T′是可滿足的，那么它的解為原問題的一個解;若T′是不滿足的，使用本文后面提到的調整策略，替換部分文字形成改進的T′。重復以上過程，直到尋找到可滿足的2-SAT子問題T′為止。

2 FSSAT算法概述

FSSAT包含了兩個主要的步驟，即使用2-SAT算法求解2-SAT子問題和選擇2-SAT子問題。下面將詳細介紹這兩個過程。

2.1 線性時間的2-SAT算法

經典的基于猜測和推導的2-SAT算法在1976年由Even等人[9]提出，它是一個時間復雜度為O(|X||C|)的算法。Alvaro[7]對這個算法進行了改進，提出了一個新的2-SAT算法——BinSat，其求解時間僅為O(|C|)。算法描述如下:

procedure PropUnit(T)

while(x and xy∈T)

T:=(T-{xy})∪{y};

return T

end

procedure Temp PropUnit(x)

if tempval(x)=1

then T:=PropUnit(T∪{x}) return;

tempval(x):=true;

tempval(x):=1;

foreach yx∈T do:

if tempval(y)≠true then Temp PropUnit(y);

procedure BinSat(T)

foreach variable p of T do:

tempval(p):=tempval(p):=NIL;

permval(p):=permval(p):=NIL;

T:=PropUnit(T);

while(x permval(x)=tempval(x)=NIL)do:

Temp PropUnit(x);

if □∈T

then return Unsatisfiable;

else return Satisfiable;

BinSat是一種基于單元歸結(或稱為布爾約束推導)的算法。單元歸結作為一種優化策略，能夠根據賦值對子句進行化簡。例如，對于子句x1∨x2∨x3，如果將變元x2賦值為1，那么子句將化簡為x1∨x3，而對于含有文字x2的子句則已滿足，可以從問題中刪去，使原問題子句數相應減少。隨著變元不斷被賦值，子句中未賦值變元的減少，會出現單元子句，即子句中除了一個文字外，其余所有文字都賦為0。例如，當x1=0，x2=1時，子句x1∨x2∨x3就成為單元子句x3。顯然，子句x3要滿足，文字x3必須賦值(隱含賦值)為1，這稱為單元子句規則。單元歸結就是不斷應用單元子句規則，直到問題中不再出現單元子句。在進行單元歸結中會使某個子句不滿足，即該子句所有文字都被賦值為0，這時稱為出現沖突。

BinSat中變元的賦值有兩種方式，即臨時賦值和永久賦值，分別保存在數組tempval和permval中。BinSat包含了兩個子過程Prop Unit和TempPropUnit。PropUnit和TempPropUnit都是進行單元歸結，不同之處是TempPropUnit只作臨時賦值，而Pr opUnit只作永久賦值。首先，選擇一個未賦值的文字，在TempPropUnit中對該文字進行臨時賦值，然后使用單元歸結推導該賦值。推導該賦值帶來隱含賦值以及該隱含賦值引起的其他隱含賦值，這些隱含賦值都保存在數組tempval中。如果在推導過程中產生沖突，例如，當出現要把文字xi賦值為1時，而tempval[xi]=1，這時可以推斷出要使2-SAT問題滿足xi必須賦值為1，因此調用過程PropUnit(T∪{xi})，使得permval[xi]=1。若在Pr opUnit進行單元歸結時也發生沖突，就可以得出原問題不滿足。

當2-SAT問題不滿足時，BinSat會在發生沖突時立即返回結果，這樣可能存在尚未賦值的變元，得不到足夠的信息。因此，本文對BinSat進行了修改，即使發生沖突算法也不停止。雖然這時所得到的真值指派A不是一個可滿足的解，但是對后面選擇一個可滿足的2-SAT子問題是有用的。

BinSat返回后，真值指派A可以這樣得到:對于任意變元xi∈X，若permval[xi]≠NIL，則xi賦值為permval[xi];若permval[xi]=NIL，則xi賦值為tempval[xi]。

2.2 選擇2-SAT子問題

當BinSat返回不滿足時，需要重新選擇2-SAT子問題。本文的選擇策略是根據得到的真值指派A，替換掉2-SAT子問題中不為真的文字，使2-SAT子問題的子句滿足數增加。

首先定義映射S:C′→{0，1，2}m為2-SAT問題在真值指派A下子句中文字取真的個數，即S(c′)=A(l′1)+A(l′2)，c′=l′1∨l′2。本文只需考慮2-SAT問題中兩種類型子句:子句在當前真值指派A下不滿足(S(c′)=0)和只有一個文字取真值(S(c′)=1)。

對任意c′i∈C′，ci∈C(i=1，2，3，…，m)(C′為2-SAT子問題子句集，C為原SAT問題子句集)，有:

a)若S(c′i)=0，對于任意l∈V(ci)-V(c′i)，若存在A(l)=1，隨機選擇文字l′∈V(c′i)替換為l，即V(c′i)=V(c′i)-{l′}∪{l}。

b)若S(c′i)=1，對于任意l∈V(ci)-V(c′i)，若存在A(l)=1，把子句c′i中不為真的文字l′替換為l，即V(c′i)=V(c′i)-{l′}∪{l}，l′∈V(c′i)∧A(l′)=0;若不存在A(l)=1，隨機選擇一個文字l∈V(ci)-V(c′i)，以一定概率P(本文使用P=n/m)替換子句c′i中不為真的文字l′。

通過以上兩種替換策略，得到新的2-SAT子問題T′，使得不滿足的子句有更大的概率變得滿足。

2.3 算法基本流程

下面給出FSSAT基本流程:

a)初始化參數，設置最大循環次數MAXTRIES。

b)令循環次數t=0，隨機選擇每個子句中的兩個文字生成初始2-SAT子問題T′。

c)調用BinSat(T′)求解2-SAT子問題T′，若BinSat(T′)返回滿足，循環結束跳轉到e);否則更新真值指派A。

d)令t=t+1，若t≤MAXTRIES，根據2.2節的選擇策略選擇新的2-SAT子問題T′，跳轉到c);否則循環結束，未能找到可滿足的解。

e)結束，輸出結果。

3 實驗結果

WALKSAT和UnitWalk是當前國際具有代表性的局部搜索算法。與它們進行對比測試，可以有效反映本文算法的性能。本文測試算法成功運行時間。本文算法采用C語言實現，WALKSAT和UnitWalk均從網絡下載源碼在本機編譯運行。本文測試平臺為微機Pentium M 1.7 GHz， 768 MB 內存，操作系統為Ubuntu 8.04。

本文測試所用的SAT問題均是隨機生成的3-SAT問題，這些實例均來之SATLIB[10]網站。根據Mitchell等人[11]的研究，隨機生成的難求解3-SAT測試樣本，當子句數數目與變元數目之比是4.3時，SAT問題的約束即不會過少，也不會過多，它們屬于可滿足和不滿足的概率是相等的，因而這些問題是比較難解的。因此采用這些3-SAT測試樣本可以有效評價算法的優劣性。本文選用的實例子句數數目與變元數目之比都是4.3，每個實例測試100次，取平均運行時間。

表1給出了三種算法的運行時間，其中n表示變元數，m表示子句數。從表1中可以看出，表現最好的還是WALKSAT，在所有問題的解決時間都是最少的。UnitWalk是2003年SAT競賽中隨機生成可滿足問題方面的獲勝者[6]，而本文算法明顯優于UnitWalk算法，在所選擇的測試問題都獲得了不同程度的提高，而與WALKSAT的差距不大，表明本文算法FSSAT求解SAT問題是有效可行的。

表1 FSSAT與UnitWalk、WALKSAT的比較結果

合取范式

nm

平均運行時間/s

FSSATUnitWalkWALKSAT

1004300.0050.0060.004

1506450.0040.0070.003

2008600.0170.0410.015

2501 0750.4200.8390.208

3001 2900.2530.5660.232

3501 5050.5811.0450.420

4001 7200.0400.0650.020

4501 9350.1570.3020.094

5002 1500.3860.8390.268

6002 5800.4150.5670.208

7003 0100.4501.2560.303

4 結束語

本文結合了2-SAT算法——BinSat，提出一種新的基于尋找可滿足2-SAT子問題的新SAT算法。通過實驗結果表明，本文算法FSSAT明顯優于著名的UnitWalk算法，解決問題花費的時間平均減少了50%，為解決SAT問題提供了一個新的有效途徑。如何選擇2-SAT子問題是影響算法收斂的關鍵，因此使用更好的啟發策略選擇2-SAT子問題將是未來本文算法的改進方向。

參考文獻:

[1]COOK S A. The complexity of theorem proving procedures[C]//Proc of the 3rd Annual ACM Symposium on the Theory of Computing. New York:ACM Press， 1971:151-158.

[2]GOMES C P， KAUTZ H， SABHARWAL A， et al. Satisfiability sol-vers[M]//Handbook of Knowledge Representation Amsterdam:2007:89-134.

[3]DAVIS M， PUTNAM H. A computing procedure for quantification theory[J]. Communications of the Association for Computing Machinery， 1960， 7(3):201-215.

[4]SELMAN B， LEVESQUE H J， MITCHELL D G. A new method for solving hard satisfiability problems[C]//Proc of the 12th National Conference on Artificial Intelligence. Cambridge:MIT Press， 1992:440-446.

[5]SELMAN B， KAUTZ H， COHEN B. Noise strategies for local search[C]//Proc of the 13th National Conference on Artificial Intelligence. Cambridge:MIT Press， 1994:337-343.

[6]HIRSCH E A， KOJEVNIKOV A. UnitWalk:a new SAT solver that uses local search guided by unit clause elimination[J]. Annals of Mathematics and Artificial Intelligence， 2005， 43(1/4):91-111.

[7]ALVARO D V. On 2-SAT and renamable horn[C]//Proc of the 17th National Conference on Artificial Intelligence. Cambridge:MIT Press， 2000:343-348.

[8]ZHENG Lei， STUCKEY P J. Improving SAT using 2-SAT[J]. Australasian Computer Science Communications， 2002，24(1):331-340.

[9]EVEN S， ITAI A， SHAMIR A. On the complexity of timetable and multi-commodity flow problems[J]. SIAM Journal of Computing， 1976， 5(4):691-703.

[10]HOOS H H， STTZLE T. SATLIB:an online resource for research on SAT[M]. Alabama:IOS Press， 2000:283-292.

[11]MITCHELL D， SELMAN B， LEVESQUE H J. Hard and easy distributions of SAT problems[C]//Proc of the 12th National Conference on Artificial Intelligence. Cambridge:MIT Press， 1992:459-465.