基于任務分配與調度的GSAT算法求解3-SAT問題

付慧敏,徐 揚，何星星,寧欣然

(1.西南交通大學信息科學與技術學院，四川 成都 610031；2.西南交通大學系統可信性自動驗證國家地方聯合工程實驗室,四川 成都 610031)

1 引言

1971年Cook證明了SAT(SATisfiability)問題是NP完全問題，具有廣泛的實際應用。許多學者將一些組合問題例如人工智能、超大規模集成電路VLSI(Very Large Scale Intergration)設計、積木世界規劃、Job shop排工等轉化為SAT問題來求解[1]。經過國內外學者的努力，求解SAT問題的優化算法已經有很多，總體分成兩類：一是完備的方法，適應于應用類問題和組合問題，例如基于DPLL(Davis Putnam Logemann Loveland)的SATO(SAtisfiability Testing Optimized)[2]、BerkMin(Berkeley-Minsk)[3]、CDCL(Conflict-Driven Clause Learning)[4]等。其優點是對于任意SAT問題都能正確地判斷其可滿足或者不可滿足，缺點是隨著問題規模的不斷增大，其解空間的復雜度成指數增長，計算效率很低，不適應于大規模問題[5]。二是不完備的方法，適應于隨機生成問題。雖然對于任意SAT問題不能都正確地判斷其可滿足或者不可滿足，但是對于可滿足SAT問題其效率整體上超過完備的方法，因此受到很多學者的青睞，使得這種方法得以快速地發展。例如，MP(Message Passing)算法[6]、Local Search算法[7]、遺傳算法[8]、不完備算法之間的結合[9,10]、組織進化算法[11]、多智能體社會進化算法[5]、GSAT算法[12,13]、完備算法和不完備算法相結合的混合算法[14]等。

GSAT算法是一個很有效的局部搜索算法，其主要的技術是貪心搜索，即通過一系列的搜索得到問題的最優解，而每一次搜索都是當前狀態下某種策略的最好選擇。早期在求解SAT領域中，貪心搜索很容易陷入“早熟”，Selman等人[15]用WalkGSAT的局部搜索算法跳出局部最優，大量的實驗表明這個技術很適應于隨機生成的3SAT問題。1998年梁東敏等人[1]在WalkGSAT的基礎上，引進了子句權重的概念，實驗表明其性能優于WalkGSAT，尤其對于結構SAT問題。2002年林智勇等人[16]提出的Learning+Weighting+GSAT算法和2010年Bouhmala等人[17]提出的LA-GSATRW算法都是在GSAT算法的基礎上進行了改進，但是其優勢不是很明顯。2015年張玉安等人[8]將局部搜索的GSAT算法與具有全局搜索的改進遺傳算法相結合，明顯彌補了GSAT算法容易出現早熟的缺點，該算法的實驗結果表明其性能得到了明顯提高。雖然近幾年貪心搜索在SAT領域的研究學者并不多，但是在其他一些領域得到了快速的發展與應用，例如組合優化問題[18]、風機布局優化[19]、優化貪心算法[20,21]、自動車輛群內的信息傳播[22]等等，所以貪心算法具有一定的使用價值和研究意義。2004年劉靜等人[11]將組織進化的思想用到求解3-SAT問題上，而且根據SAT問題的特點重新定義了組織的概念，并根據組織和SAT問題的特點提出了新的算子；2014年潘曉英等人[5]的多智能體社會進化算法，將智能體對環境的感知能力的思想用到求解SAT問題上，而且根據SAT問題的特點重新定義了智能體的概念，并根據智能體的行為和SAT問題的特點提出了新的3種行為，對于3-SAT問題這兩種算法的性能都得到了顯著提高。

為了進一步提高GSAT算法的效率，即提高貪心算法的性能，本文根據組織進化算法、多智能體社會進化算法和李炳芬等人彌補GSAT算法具有局部搜索的缺點的思想，在Weighting+WalkGSAT的基礎上，將任務分配與調度的主要目的與3-SAT問題的特點相結合，并重新定義了任務分配與調度的概念，提出了基于任務分配與調度的GSAT算法求解3-SAT問題。在文獻[23,24]中，任務分別指的是數據并行交換和用戶提交的需求，本文算法的任務指的是3-SAT問題中的所有變量，與文獻[23,24]中的定義完全不同；而且分配與調度的概念與文獻[23,24]中的概念也完全不同，文獻[23]中的分配與調度是根據任務的特點和每個影響因素決定任務的順序，文獻[24]中的分配與調度是通過不同的分配策略和調度策略合理高效地處理用戶提交的任務，通過任務分配與調度的思想，他們都取得了很好的效果。不僅文獻[23,24]中的作者使用分配與調度，而且許多領域的國內外研究人員[25 - 28]都用到了這種思想，他們的目的都是為了高效地完成任務。本文的分配與調度是在搜索最優真值指派的過程中所用到的策略。在該算法中，與傳統的GSAT算法不同，根據任務的特點和分配與調度的思想設計了新的貪心策略。實驗結果表明，本文算法能更快地跳出局部最優，減少翻轉次數，提高成功率，具有一定的使用價值。

2 3-SAT問題及其表示

3-SAT問題是可滿足性問題，尋找一個給定的布爾值公式是否可滿足[29]。在本節中，首先定義一些相關概念，然后精確定義3-SAT問題。

定義1真值指派(Value-Assignment)[29]:用符號Xn表示n個布爾變量的集合，xi，i∈{1,2,…,n}表示布爾變量，則Xn={x1,x2,…,xn}。n個布爾變量的真值指派是一個函數v:{x1,x2,…,xn}→{0,1}，其中每個布爾變量x1,x2,…,xn都被指派為1或0，1表示真，0表示假。在本文的算法中1表示真，-1表示假。

定義2文字(Literal)[29]:每個文字是一個布爾變量或者一個布爾變量的否定，分別表示為xi或者xi(xi的非)，被分別稱為正文字和負文字，其中i∈{1,2,…,n}。

定義3子句(Clause):m個子句的集合表示為：Cm={c1,c2,…,cm}，每個子句ci由3個文字的析取(∨)組成[29,30]。若文字xi出現在Cm中且xi不出現在Cm中，則稱文字xi為純文字。

定義4合取范式(CNF):每個合取范式由若干子句的合取(∧)組成，形如F=c1∧c2∧…∧cm。

合取范式F在真值指派下為真當且僅當每個子句c1,c2,…,cm在真值指派下都為真[5]。

3-SAT問題就是?ck∈F,k∈{1,2,…,m}，是否存在一個真值指派使F為真，若存在這樣的真值指派，則稱3-SAT問題可解決[29]。

3 基于任務分配與調度的GSAT算法

3.1 求解3-SAT問題的任務定義

定義5任務i是布爾變量集合Xn中的一個變量xi，i∈{1,2,…,n}，任務的取值只有兩種，分別為真和假。

子句ck權重記為Weight(ck),k∈{1,2,…,m}，這里的權重與Weighting+WalkGSAT的權重定義相同。根據對任務的賦值，包含該任務的子句有兩種—取值為真的子句稱為可滿足子句，取值為假的子句稱為不可滿足子句；包含該任務的子句權重有兩種—取值為真的子句其權重稱為可滿足子句權重，取值為假的子句其權重稱為不可滿足子句權重；包含該任務的不可滿足子句權重有兩種，分別是翻轉該任務前稱為前不可滿足子句權重和翻轉該任務后稱為后不可滿足子句權重。本文的大任務指所有任務的集合，即包含問題的所有變量，與文獻[31]中的類似。任務貪心搜索是大任務的前不可滿足子句權重之和與后不可滿足子句權重之和的差達到最大，若這個差值的最大值(記為best_Diff)不小于0，則進行翻轉[16]。

在搜索最優真值指派的過程中，每個任務在當前真值指派下需要記錄一些信息，一個任務i的結構表達如下：

任務貪心搜索策略：記錄該任務翻轉的條件，即:

best_Diff>0,k∈{1，2，…，n}

大任務規模：所有子任務的個數記為Size,即Size=n。

從任務的結構可以看出，一個任務就是原問題的一個變量，而當該任務達到搜索策略要求時，翻轉這個任務，使得假子句權重之和減少，真子句權重之和增加，同時通過增加不可滿足子句的權重提高了假子句為真的幾率，加快搜索的進程。當假子句權重之和減少到0時，該變量就找到了一個解。顯然，當假子句權重之和為0的任務集合等于大任務規模時，就得到大任務的一個最優解。因此，要解決原問題，就要解決含有所有子句的大任務，這就要使不同任務間進行相互作用。

任務分配與調度問題是NP完全問題[32]。本文并不關心如何分成適當的子任務,如何將子任務分配給各個處理機，如何安排子任務的執行順序，而是將重點放在子任務的相互作用上。任務分配與調度的主要目的是為了尋找一個合適的分配調度，使得任務執行結束后所花費的時間盡量地小。受此啟發，我們另外設計了兩種任務貪心策略來引導任務的完成。

3.2 貪心策略

本文的另外兩種任務貪心策略分別為分配策略和調度策略。分配策略是提前指導任務貪心搜索的趨勢，它利用原問題本身的信息進行貪心指派任務，本質是減少搜索空間，實際上起到快速找到最優解的作用。調度策略是當不能滿足任務貪心搜索策略條件時，起用調度策略決定翻轉的子任務，有效地防止搜索陷入局部最優，加快搜索進程。

3.2.1 如何任務分配

在SATLAB庫[33]中，“Uniform Random-3-SAT”問題集共有3 700個3-SAT問題，文獻[5,11]表明該問題集已經被大量用于測試求解SAT問題算法的性能,這些問題的子句個數和變量個數之比均為4.3左右，此類問題屬于不可滿足和可滿足的概率幾乎是相等的，屬于難解的一類問題集，所以通過測試這些問題更能反映出算法性能的優越性。根據變量的個數可以將這3 700個問題分成10個集合，分別記為S1,S2,…,S10，以下通過表1給出這10個集合所包含的問題和相應的參數。

Table 1 Uniform Random-3-SAT problems in experiments

SAT問題類似數學約束問題，所以我們可以先分析問題庫中變量之間的關系以及SAT問題的解空間，然后分配一些變量的真值指派，最后通過算法搜索加快解的進程。通過分析SATLAB庫中的每個問題集和每個問題集所對應的解可以發現，最優的真值指派T與問題集中的每個布爾變量的正負比例值有關，即當某個布爾變量的正負比例值大于某個恰當的數或者小于某個合適的數時，此布爾變量的最優真值指派直接確定為真或者假的成功率是90%左右。在GSAT類算法和其他類解決SAT問題的不完備算法中，它們大多數都是通過隨機產生一個真值指派作為搜索的起點[34]。若一個問題的布爾變量個數為n且只有一個最優真值指派，則隨機產生的真值指派有2n種情況且一次產生最優真值指派的概率為1/2n。在2n種情況中，我們的想法是通過每個布爾變量的正負比例值分配一個求解3-SAT問題的初始指派，即提前指導最優真值指派搜索的趨勢，從而加快找到最優解。這種利用每個問題集中每個布爾變量的正負文字比例值確定初始指派的想法，叫做“分配”，以下定義給出了本文算法中所使用的公式。

定義6變量分配度Vad(Variable allocation degree)，?i∈{1,2,…,n}，它的變量分配度等于:

(1)

其中，在一個3-SAT問題中，pi為所有子句中含有正文字i的總個數，ni為所有子句中含有負文字i的總個數(問題集中負文字的形式為-i)，當Vad(i)≥1時，稱為i的正變量分配度，當Vad(i)<1時，稱為i的負變量分配度。pad(positive variable allocation degree)為正變量分配度參數，nad(negative variable allocation degree)為負變量分配度參數。在求解3-SAT問題的過程中，不同的變量分配度參數值對于算法的性能有著直接的影響，在時間運行上，甚至會相差10倍以上，而且也會影響解的成功率。

定義7變量分配值Vav(Variable allocation value)，?i∈1,2,…,n，它的變量分配值等于:

(2)

Vad(i)>pad或者Vad(i)

(3)

若任務不滿足分配策略，則其變量分配值是由隨機數決定的。通過變量分配度的定義我們可以發現，當ni=0或者pi=0時，i一定滿足分配策略，因為此時的i或者-i為純文字，在搜索最優真值指派的過程中，只需要將i或者-i的變量分配值為1或者-1，若此情況對i或者-i進行翻轉，不會使不可滿足子句的總和減少。因此，通過分配策略縮小了搜索空間。

定義8滿足度Sd(Satisfaction degree)，是在一個3-SAT問題中滿足分配策略的任務在大任務中所占的比例 ，即:

(4)

3.2.2 分配的直觀解釋

子句集C4={x1∨x3∨x4，x1∨x2∨x4,x2∨x3∨x4,x2∨x3∨x4}，若nad=0.3，則分別通過計算各個任務所對應的分配度、分配值、分配真值和滿足度，得到任務的分配流程，如表2所示。

Table 2 Distribution flow sheet

表2中，x2和x4的分配值是隨機產生的，而且所有變量的分配值剛好是子句集C4的一個最優真值指派。因為對分配度的定義是為了更好地提前確定容易判定的變量的最優真值指派，減少搜索過程中的翻轉次數和減小搜索的解空間，因而加快算法搜索的進程。若randomf(0,1)表示產生(0,1)的隨機數，Vad(N)={Vad(1),Vad(2),…,Vad(n)},Vav(N)={Vav(1),Vav(2),…,Vav(n)}，則分配策略的具體算法描述如下：

算法1Allocation Strategy

步驟1讀取子句集Cm；

步驟2計算所有任務的分配度Vad(N)；

步驟3計算所有任務的分配值Aav(N)，分配一個搜索的初始指派。

3.2.3 調度策略

算法2Scheduling Strategy

步驟1IFbest_Diff小于或等于0 THEN

從cF中隨機選擇一個子句cr，在該子句中隨機選擇一個變量task1；

步驟2IFtask1滿足分配策略THEN

翻轉task1。

3.3 基于任務分配與調度的GSAT算法

三種任務貪心策略起著不同的作用，我們只有有序地采用上面的三種策略才能達到求解3-SAT問題的目的。在整個搜索過程中，本文算法采用貪心的方式控制任務間的相互作用。設滿足任務貪心搜索策略的第一個任務記為temp，具體描述如下：

輸入：各初始化參數:最大翻轉次數MAXFLIPS,最大嘗試次數MAXTRIES,pad,nad,pad′,nad′,子句集元素總個數,Size,p。

輸出：任務的最優解或“no solution found!”。

步驟1讀取子句集Cm；

步驟2計算每個任務的分配度；

步驟3所有子句的權重初始化為1；

步驟4FORi:=1toMAXTRIESDO

步驟5根據分配策略的條件，計算每個任務的分配值，作為搜索的起點；∥分配策略條件

步驟6FORj:=1toMAXFLIPSDO

步驟7產生一個[0,1)的隨機數r；

步驟8IF (r

步驟9ELSE

步驟10IF(best_Diff>0)THEN 翻轉temp

∥任務貪心搜索策略

步驟11ELSE

步驟12執行任務調度策略；∥調度策略

步驟13IFSizecF不等于0 THEN

從cF中隨機挑選一個子句，并將它的權加1。

步驟14ENDFOR

步驟15ENDFOR

步驟16RETURN “no solution found!”；

4 仿真實驗結果和分析

本文的實驗環境為：處理器(Intel(R) Core(TM)i5-4590 CPU @ 3.30 GHz)，RAM(8.00 GB)，Windows 7 64位操作系統。實驗數據是SATLAB庫中的“Uniform Random-3-SAT”標準問題集。因為GSAT算法容易導致早熟的缺點，自2002年以后，從文獻中可以發現，很少有學者單獨研究GSAT算法求解3-SAT問題，大多都是將GSAT算法與具有全局搜索的算法相結合。2002年以前比較優秀的GSAT算法有WalkSAT、Weighting+WalkGSAT和Learning+Weighting+GSAT，2002年以后在文獻[17]中提到了兩種新的GSAT算法LA-GSATRW和GSATRW。我們主要選擇具有高性能的Weighting+WalkGSAT算法、普通性能的GSATRW算法和2016年將GSAT算法與云計算相結合的遺傳算法進行比較，用于驗證本文算法中分配策略和調度策略的有效性。

將本文算法、Weighting+WalkGSAT算法和GSATRW算法的最大任務(變量)改變次數都設為MAXFLIPS*MAXTRIES=107。若一次運行在規定的時間和最大變量改變次數內找到3-SAT問題的一個最優解，則此次運行成功。成功率是成功運行的次數與總運行次數之比。

實驗中這三種算法每個問題獨立運行10次，而且參數pad和pad′在0.3～0.6，nad和nad′在1.8～2。在表3中分別給出每個問題集中的最大平均變量改變次數、最小平均變量改變次數、總平均變量改變次數和平均成功率，其中將Weighting+WalkGSAT算法在以下表中用WW表示，本文算法用AS表示，GSATRW算法用RW表示，最小平均變量改變次數用MAC表示，總平均變量改變次數用TAC表示，平均成功率用ASR表示。

從表3中的結果可以看出，本文算法具有較好的性能。在這三種算法中，本文算法的成功率是最高的，它對SATLAB庫中的8組問題集中的所有問題都能找到最優真值指派，另外兩組都是只有一個問題沒有完全找到最優解。與Weighting+WalkGSAT算法相比，雖然它們前7組問題集中的每一個問題都能找到解，但是本文算法比Weighting+WalkGSAT算法所需的變量改變次數明顯減少，尤其MAC分別減少了6倍左右;而且對于后3組問題集，其成功率分別提高了5%左右;對于前8組問題集，本文算法都是以更少的變量改變次數得到了更好的結果；對于后2組問題集，雖然本文算法所需的變量改變次數明顯增多，但是其成功率提高了6%左右。這說明Weighting+WalkGSAT算法在規定的時間內找到最優真值指派的比例明顯少于本文算法，即本文算法的時間復雜度明顯較低，體現了本文算法具有更好的時間性能。與GSATRW算法相比，本文算法更具有優勢，其成功率分別提高了10%左右，MAC總體減少了12倍左右，TAC分別減少了5倍左右。因為算法所需變量改變次數的多少影響時間效率，所以在表中沒有列舉出算法花費的時間，即在成功率一樣的情況下，變量改變次數越少，算法花費的時間越少。總體來說，對于前8組問題集，與另外兩種算法相比本文算法都體現了較好的性能，但是對于S9和S10集合它的MAC性能較弱，仍存在一定的改進空間。

Table 3 Results comparison with other improved GSAT algorithms with 10 times running for 3-SAT problem

我們考慮到這些算法都是不完備算法，其結果有一定的隨機性，即在相同實驗環境下，在不同時間段內所測的結果可能會出現很大的偏差，所以為了使算法的性能比較更具有說服力，實驗中對問題集中的每個問題獨立運行10 000次，且參數設置與表3相同。我們考慮到一方面運行次數太多，另一方面隨著變量的不斷增加，解空間的復雜性也隨著增加，算法所花費的時間也隨著增加，其中對于含有100個變量問題集中的某個問題，本文算法需要花費10個小時左右，所以如果對10組問題集中的每個問題都運行10 000次，總共需要花費的時間至少5個月，所以實驗中我們只選擇了前4組問題集進行分別測試。表4分別給出了每個問題集中的最多時間、最少時間、平均時間和總平均變量改變次數。

Table 4 Results comparison with different improved GSAT algorithms with 10000 times running for 3-SAT problem

另外，求解3-SAT問題的本文算法是通過設計兩種新的策略來完成整個貪心過程的，為了進一步明確兩種策略在整個搜索過程中所起的作用，分別對這兩種策略的性能進行了測試分析。我們在10組問題集中隨機選擇了3組問題集進行測試，它們分別為S4、S7和S9，然后逐一對只有分配策略、只有調度策略、無分配策略和調度策略來完成整個貪心搜索過程，其中參數設置與表3中的實驗完全相同，實驗結果見表5。

Table 5 Algorithm comparision

從表5的結果可以看出，分配策略對算法性能的影響比較大，若除去該策略，變量改變次數大多明顯增加，所以相對花費的時間也增加，貪心策略的作用是局部搜索，而分配策略的作用是全局搜索，剛好彌補了貪心策略的不足，通過分配策略指導貪心搜索的全局方向，減小搜索空間，從而減少變量改變次數和相應的搜索時間。另外，調度策略在整個貪心搜索過程中也起到了不同程度的影響，通過調度策略防止算法陷入早熟，加快搜索的進程。

5 結束語

本文根據任務分配與調度的主要目的提出了一種新的求解3-SAT問題的GSAT算法，并結合3-SAT問題的特點設計了兩種相應的貪心策略。實驗中采用標準數據庫中的3-SAT問題對算法進行了全面的測試，并與其他改進的GSAT算法進行了比較，結果表明，不管在成功率方面還是總體平均變量改變次數方面，本文算法都優于所比較的高效和普通性能改進的GSAT算法。