基于混合蟻群遺傳算法的SAT問題求解

王立冬，王 楠，余 軍

(1. 北方民族大學(xué) 計(jì)算機(jī)科學(xué)與工程學(xué)院，寧夏 銀川 750021；2. 大連民族大學(xué) 理學(xué)院，遼寧 大連 116605)

基于混合蟻群遺傳算法的SAT問題求解

王立冬1,2，王 楠1，余 軍2

(1. 北方民族大學(xué) 計(jì)算機(jī)科學(xué)與工程學(xué)院，寧夏 銀川 750021；2. 大連民族大學(xué) 理學(xué)院，遼寧 大連 116605)

根據(jù)SAT問題的特點(diǎn)，通過分析傳統(tǒng)蟻群算法和遺傳算法在求解SAT問題上的不足，提出一種基于混合蟻群遺傳算法的SAT問題求解方法。給出一種新的初始解的生成方式；在迭代過程中，根據(jù)較優(yōu)解的累積信息提出進(jìn)化算子；利用當(dāng)前得到的最優(yōu)解，通過改變不滿足子句中文字的取值，增加變異算子。最后選取標(biāo)準(zhǔn)測(cè)試集中的20個(gè)實(shí)例對(duì)算法進(jìn)行測(cè)試，實(shí)驗(yàn)結(jié)果表明：改進(jìn)后的算法通常僅通過較少次數(shù)的迭代就能找到解，能夠有效避免蟻群算法和遺傳算法過早收斂的缺點(diǎn)，具有較強(qiáng)的尋優(yōu)能力。

可滿足性問題；混合蟻群遺傳算法；進(jìn)化算子；變異算子

可滿足性問題(Satisfiability Problem, SAT)是第一個(gè)被Cook定理證明的NP完全問題，即多項(xiàng)式復(fù)雜程度的非確定性問題，判定對(duì)于一個(gè)命題范式，是否存在一組范式中變量的賦值使得該范式為真。目前，解決該問題的方法主要有完備方法和不完備方法。完備的方法包括DP算法[1]、DPLL等[2]，該類方法可以正確地判斷SAT問題的可滿足性，但計(jì)算復(fù)雜度較高，對(duì)于大規(guī)模SAT問題，這種算法的效率很低；不完備方法基于Local Search算法[3-4]，包括GSAT[5]，WALKSAT[6]等，這類方法的求解速度往往比完備算法快很多。

國(guó)內(nèi)外許多學(xué)者對(duì)如何求解SAT問題都做了大量的研究，文獻(xiàn)[7]利用啟發(fā)式函數(shù)來計(jì)算不滿足子句中文字所對(duì)應(yīng)的命題變?cè)母怕史植紮?quán)值，然后根據(jù)變?cè)臋?quán)值來選取翻轉(zhuǎn)變?cè)M(jìn)行翻轉(zhuǎn)，這在求解3-SAT問題方面有突出的表現(xiàn)；文獻(xiàn)[8]翻轉(zhuǎn)變?cè)倪x取既考慮到可滿足子句增加的數(shù)目又考慮到變?cè)x取的合理性，避免翻轉(zhuǎn)變?cè)闹貜?fù)選取，并結(jié)合跳出策略避免陷入局部最優(yōu)解，使得算法朝著能夠減少不滿足子句數(shù)目的方向進(jìn)行搜索；西安電子科技大學(xué)的李陽陽等在文獻(xiàn)[9]中提出一種基于量子編碼的免疫克隆算法來求解SAT問題；東北大學(xué)的郭瑩等在文獻(xiàn)[10]中提出一種求解SAT問題的離散人工蜂群算法，之后在文獻(xiàn)[11]中從完備算法、不完備算法和組合算法3個(gè)角度總結(jié)了SAT問題的研究進(jìn)展。

遺傳算法(Genetic Algorithm,GA)[12]和蟻群算法(Ant Colony Optimization, ACO)[13]在求解組合優(yōu)化問題方面有著自身的優(yōu)勢(shì)。文獻(xiàn)[14]使用并行策略的ACO優(yōu)化算法解決SAT問題；文獻(xiàn)[15]通過評(píng)估遺傳算子的計(jì)算效率和相關(guān)參數(shù)來求解3-SAT問題；文獻(xiàn)[16]在遺傳算法的基礎(chǔ)上通過擴(kuò)張和調(diào)查算子求解最大化可滿足性問題；廣西大學(xué)的孫如祥等在文獻(xiàn)[17]中針對(duì)加權(quán)SAT問題的特點(diǎn)，以重離散化方式簡(jiǎn)化蟻群算法模型，提出取值概率的概念，并以之替換傳統(tǒng)蟻群算法中的信息素，最后對(duì)該算法做并行化改進(jìn)；中山大學(xué)的凌應(yīng)標(biāo)等在文獻(xiàn)[18]中將SAT問題的結(jié)構(gòu)信息量化為子句權(quán)重，增加了學(xué)習(xí)算子和判定早熟參數(shù)，并采用最優(yōu)染色體保存策略，防止進(jìn)化過程的發(fā)散。

通過隨機(jī)賦值方法生成的初始解的質(zhì)量不高，導(dǎo)致接下來的迭代過程中解的收斂速度較慢，影響尋優(yōu)能力；遺傳算法的交叉算子具有較大的盲目性，交叉得到的新解的質(zhì)量往往并沒有提高，沒有能夠有效利用迭代過程所累積的信息。將遺傳算法和蟻群算法進(jìn)行結(jié)合，能夠很好地互補(bǔ)。

1 SAT問題的定義

定義1 文字(Literal)

定義2 子句(Clause)

子句c都是由若干個(gè)文字通過析取運(yùn)算符(∨)鏈接而成，子句中文字的個(gè)數(shù)稱為子句的長(zhǎng)度，當(dāng)子句中至少有一個(gè)文字為真時(shí)則該子句為真。如長(zhǎng)度為2的子句c=(x1∨x2)，當(dāng)x1=1或x2=0時(shí)該子句都為真。

定義3 可滿足性問題(SAT)

(1)

顯然當(dāng)fit(S)=0時(shí)，該SAT問題在賦值S下是可滿足的。為了敘述方便，下文中這樣的真值指派S也稱為解。

2 基于混合蟻群遺傳算法的SAT問題求解

2.1 初始解生成方式的改進(jìn)

在遺傳算法中，先得到N個(gè)初始解，而每個(gè)解中的文字都被隨機(jī)賦值為1或-1，這樣生成的解具有很大的盲目性，同時(shí)解的整體質(zhì)量不高，在一定程度上影響SAT問題是否可以找到最優(yōu)解。本文提出一種新的初始解的生成方法，提高了初始解的質(zhì)量，有利于在后續(xù)迭代過程中找到最優(yōu)解。

(1)初始化解中的部分文字。規(guī)則如下：給定兩個(gè)閾值α1和α2，且滿足條件0<α2<α1<1，對(duì)每個(gè)文字，生成隨機(jī)數(shù)r∈(0,1)。若r<α2時(shí)，該文字不被賦值；若α2≤r<α1，則將該文字賦值為-1；若r≥α1，則將該文字賦值為1。為了保證文字被賦值為1或-1的概率相等，即α1和α2的取值應(yīng)滿足2α1=1+α2，而α2的取值直接影響初始被賦值文字的多少。實(shí)際上，α2的值越接近于0，總體上被賦值的文字就越多，生成初始解的速度相對(duì)越快，初始解的質(zhì)量越低；反之，α2的值越接近于1，則總體上被賦值的文字就越少，初始解的整體質(zhì)量越高。α2的取值可以根據(jù)具體的問題做相應(yīng)的調(diào)整，如α2=0，則所有文字都被隨機(jī)賦值，這樣得到的初始解與隨機(jī)生成初始解無異，在沒有已知信息的情況下，對(duì)初始解進(jìn)行賦值時(shí)，要選取相對(duì)較小的α2的值。

(2)根據(jù)給定的規(guī)則更新子句集合。對(duì)每個(gè)子句，逐一根據(jù)每個(gè)文字的賦值情況對(duì)其進(jìn)行更新：如果該子句中的當(dāng)前文字為真，則將該子句從子句集合中刪除；如果當(dāng)前文字為假，則將該文字從該子句中刪除，并用刪除文字之后的子句替換原子句；如果當(dāng)前文字沒有被賦值，則該子句不做任何變化。

(3)根據(jù)更新之后的子句集合，判斷每個(gè)子句的長(zhǎng)度。如果子句的長(zhǎng)度為0，即空子句，那么就將該子句從子句集合中直接刪除。如果子句長(zhǎng)度為1,則根據(jù)該子句中當(dāng)前文字的正負(fù)，將文字賦值使得該子句為真，并統(tǒng)計(jì)被賦值文字的個(gè)數(shù)m，根據(jù)m的大小又分兩種情況：如果m大于給定的閾值M，則直接返回上一步；如果m≤M，可以再次隨機(jī)賦值部分文字后返回上一步。M的取值可以根據(jù)具體的問題作相應(yīng)的調(diào)整，M越小，生成初始解的速度越慢，解的質(zhì)量越高。

(4)不斷重復(fù)步驟(2)、(3)直到子句集合為空，最終得到一個(gè)初始解。

改進(jìn)后的初始解的生成方式可以提高初始解的質(zhì)量，降低初始解的隨機(jī)性，更好地作用在接下來的交叉和變異等步驟中，使得問題的解向更優(yōu)的方向進(jìn)化，提高了算法的有效性。

2.2 計(jì)算適應(yīng)度函數(shù)值

計(jì)算每個(gè)解的適應(yīng)度函數(shù)值fit(S)，根據(jù)fit(S)的大小，對(duì)所有解按照從小到大排序。

2.3 選擇算子

在確定選擇概率的情況下，根據(jù)排序結(jié)果選擇適應(yīng)度函數(shù)值小的解作為算子。這樣能夠保證較優(yōu)秀的解在迭代過程中不至于丟失，僅遺傳極少部分解到下一代中，能夠有效避免算法收斂過快，即陷入局部最優(yōu)的困境。

2.4 交叉算子

先確定交叉概率，同樣根據(jù)排序結(jié)果選擇較優(yōu)秀的兩個(gè)解進(jìn)行交叉操作，將交叉之后得到的新解放到下一代中。由于交叉算子具有很大的盲目性，并不能夠保證交叉之后的解較父代更加優(yōu)秀，所以選擇較小的交叉概率，即僅僅交叉生成極少部分解。

2.5 進(jìn)化算子

若xi=1，

(2)

若xi=-1，

(3)

然后，根據(jù)信息素矩陣生成新的解。分為三個(gè)步驟：

第二步，根據(jù)當(dāng)前解更新子句集合，更新規(guī)則和生成初始解時(shí)更新子句集合的規(guī)則相同。若存在長(zhǎng)度為1的子句，則將該文字賦值使得該子句為真。同時(shí)統(tǒng)計(jì)剩余子句集合中各個(gè)文字出現(xiàn)的次數(shù)，若該文字只以正文字出現(xiàn)，則將該文字直接賦值為1；類似的若該文字只以負(fù)文字出現(xiàn)，則將該文字賦值為-1。這樣，解中又有部分文字可能被賦值，如果此次被賦值的文字相對(duì)較多，則可以重新更新子句集合，重復(fù)上述過程。

第三步，如果被賦值的文字相對(duì)較少，則根據(jù)第二步的統(tǒng)計(jì)結(jié)果將出現(xiàn)次數(shù)相對(duì)較多的部分文字優(yōu)先賦值，賦值的方法和第一步類似。不斷的重復(fù)第二、三步，直到子句集合為空為止。最后將得到的新解加入下一代解的集合中。

在進(jìn)化算子生成部分新解結(jié)束之后，為了避免算法陷入局部最優(yōu)，累積信息素矩陣內(nèi)的信息存在一定程度的揮發(fā)，揮發(fā)系數(shù)ρ通常介入0到1之間，更新公式為

A2×n=ρ×A2×n。

(4)

進(jìn)化算子的流程圖如圖1。

圖1 進(jìn)化算子流程圖

2.6 變異算子

對(duì)遺傳算法中的變異算子進(jìn)行改進(jìn)，使得改進(jìn)后的變異算子更具有針對(duì)性，以增強(qiáng)其找到最優(yōu)解的能力。采用精英解策略，即選擇當(dāng)前最優(yōu)的解進(jìn)行變異操作，分為三步。

第三，判斷翻轉(zhuǎn)之后的最優(yōu)解是否比之前更優(yōu)，如果是則保存當(dāng)前解到下一代中；否則重復(fù)第二步的過程，如果重復(fù)的次數(shù)大于給定的限制，則結(jié)束這個(gè)過程，保存當(dāng)前的次優(yōu)解到下一代中。

在迭代過程中，若存在一組真值指派S，使得fit(S)=0，即合取范式F中所有子句都為真時(shí)，循環(huán)提前結(jié)束，并輸出當(dāng)前的真值指派；否則迭代繼續(xù)進(jìn)行，直到達(dá)到最大的迭代次數(shù)為止。

混合蟻群遺傳算法流程如圖2。

圖2 混合蟻群遺傳算法

3 實(shí)驗(yàn)分析

為了驗(yàn)證混合蟻群遺傳算法在求解SAT問題(HAGSAT)時(shí)的有效性，從標(biāo)準(zhǔn)測(cè)試庫(kù)SATLIB中選取20個(gè)實(shí)例進(jìn)行測(cè)試，選取的測(cè)試集見表1，其中詳細(xì)列舉了每個(gè)測(cè)試實(shí)例的名稱、子句數(shù)和變量數(shù)。

表1 SAT問題測(cè)試實(shí)例

利用測(cè)試實(shí)例對(duì)初始解的質(zhì)量進(jìn)行測(cè)試，測(cè)試結(jié)果如圖3。

圖3 初始解的質(zhì)量對(duì)比

從圖3中可以看出，和傳統(tǒng)隨機(jī)生成初始解的方式相比，不僅最優(yōu)解的質(zhì)量有了顯著提高，整個(gè)初始解集的質(zhì)量也有很大的提升，通過本文算法生成的初始解可以滿足的子句個(gè)數(shù)非常接近每個(gè)實(shí)例的子句總個(gè)數(shù)，提高了后續(xù)迭代尋優(yōu)過程的效率。

本文算法(HAGSAT)、遺傳算法(GASAT)和蟻群算法(ACOSAT)在20個(gè)實(shí)例中測(cè)試結(jié)果見表2。N為實(shí)例序號(hào)；n為種群大??；t為每個(gè)實(shí)例測(cè)試的次數(shù)；i為迭代次數(shù)；suc為成功找到解的總次數(shù)；ave為成功找到解時(shí)的平均迭代次數(shù)；nf為無法找到解時(shí)的不滿足子句的平均數(shù)。

表2 實(shí)驗(yàn)結(jié)果對(duì)比

通過表2可以看出，本文使用的混合蟻群遺傳算法無論在求解速度還是求解質(zhì)量等方面都要明顯優(yōu)于其它兩種算法。

第一，從成功找到解的次數(shù)方面來看，本文算法在規(guī)定的測(cè)試次數(shù)內(nèi)，找到解的次數(shù)要明顯高于其它兩種算法，且成功率高。例如：在實(shí)例3的10次測(cè)試中，本文算法有8次成功找到問題的解，GASAT沒有找到問題的解，ACOSAT只有1次找到問題的解；在實(shí)例4的10次測(cè)試中，本文算法10次都成功找到問題的解，GASAT有4次找到問題的解，ACOSAT沒有找到問題的解；在實(shí)例20的50次測(cè)試中，本文算法在50次內(nèi)都成功找到問題的解，GASAT有23次找到問題的解，ACOSAT有28次找問題的解。

第二，從找到解時(shí)的平均迭代次數(shù)來看，本文算法成功找到解的平均迭代次數(shù)要遠(yuǎn)低于其它兩種算法，速度較快。例如：實(shí)例1最大迭代15次，本文算法平均迭代2次就能成功找到問題的解，而GASAT需要平均迭代8.7次才可以找到解，ACOSAT平均迭代4.3次找到解；實(shí)例5最大迭代30次，本文算法平均迭代2.1次就能成功找到問題的解，GASAT平均迭代11.6次才可以找到解，ACOSAT在30次的迭代過程中沒有找到解；實(shí)例12最大迭代20次，本文算法平均迭代7.5次就可以找到問題的解，而GASAT和ACOSAT在20次的迭代過程中沒有找到解。

第三，從無法找到解時(shí)的不滿足子句的數(shù)量方面來看，本文算法無法找到解時(shí)的不滿足子句的平均數(shù)要低于其它兩種算法。例如：在實(shí)例6的684個(gè)子句中，本文算法在無法找到解時(shí)的不滿足子句平均個(gè)數(shù)為1.3個(gè)，GASAT算法下的不滿足子句平均個(gè)數(shù)為4.8個(gè)，ACOSAT算法下的不滿足子句平均個(gè)數(shù)為為1.5個(gè)；在實(shí)例13的830個(gè)子句中，本文算法在無法找到解時(shí)的不滿足子句平均個(gè)數(shù)為2個(gè)，GASAT算法下的不滿足子句平均個(gè)數(shù)為7.5個(gè)，ACOSAT算法下的不滿足子句平均個(gè)數(shù)為為4.2個(gè)；在實(shí)例14的875個(gè)子句中，本文算法在無法找到解時(shí)的不滿足子句平均個(gè)數(shù)為7個(gè)，GASAT算法下的不滿足子句平均個(gè)數(shù)為19個(gè)，ACOSAT算法下的不滿足子句平均個(gè)數(shù)為為11個(gè)。

綜上所述，針對(duì)不同子句和不同變量個(gè)數(shù)的SAT問題，本文采用的混合蟻群遺傳算法都能夠有效的求解測(cè)試實(shí)例且成功率較高，成功找到解的次數(shù)要明顯高于遺傳算法和蟻群算法，而成功找到解時(shí)的平均迭代次數(shù)和無法找到解時(shí)的不滿足的子句的平均數(shù)都要低于遺傳算法和蟻群算法。

4 結(jié) 論

本文根據(jù)蟻群算法和遺傳算法各自的優(yōu)勢(shì)，并結(jié)合SAT問題的特點(diǎn)，對(duì)兩種算法進(jìn)行了改進(jìn)和融合，給出了進(jìn)化算子和變異算子，提高了混合蟻群遺傳算法的尋優(yōu)能力和求解效率。在標(biāo)準(zhǔn)測(cè)試庫(kù)SATLIB中選取了20個(gè)實(shí)例進(jìn)行測(cè)試，測(cè)試結(jié)果表明本文算法在求解SAT問題上優(yōu)于蟻群算法和遺傳算法。事實(shí)上，通過大多數(shù)測(cè)試實(shí)例的結(jié)果可以看出，僅通過較小的種群規(guī)模和較少的迭代次數(shù)就能找到真解，反過來較大的種群規(guī)模和較多迭代次數(shù)也不一定能保證找到解。同時(shí)注意到初始解集往往對(duì)最終的尋優(yōu)結(jié)果有較大的影響，不合適的初始解集意味著更多的迭代次數(shù)，甚至陷入局部最優(yōu)而根本跳不出來。為了避免出現(xiàn)這類情況，可以考慮該算法的并行模式，即同時(shí)生成多個(gè)種群，每個(gè)種群都是獨(dú)立、互不干擾的，當(dāng)有某個(gè)種群找到真解時(shí)，迭代結(jié)束。在后續(xù)的實(shí)驗(yàn)中，可繼續(xù)對(duì)該算法進(jìn)行完善并改進(jìn)以適應(yīng)不同類型的SAT問題求解。

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

[2] MARQUES-SILVA J P, SAKALLAH K A. GRASP: A search algorithm for propositional satisfiability[J]. IEEE Transactions on Computers, 1999, 48(5):506-521.

[3] GU J. Efficient local search for very largescale satisfiability problems [J]. Sigart Bulletin, 1992, 3(1):8-12.

[4] CRAWFORD J M. Solving satisfiability problems using a combination of systematic and local search [J]. Rutgers University, 1996.

[5] SELMAN B, LEVESQUE H, MITCHELL D. A new method for solving hard satisfiability problems [J]. AAAI, 1999:440-446.

[6] WALKER S, BRETT S. Noise strategies for improving local search [C]// Proceedings of the twelfth national conference on Artificial intelligence (vol. 1). American Association for Artificial Intelligence, 1994:337-343.

[7] BALINT A, FROHLICH A. Improving stochastic local search for SAT with a new probability distribution[C]// Springer-Verlag Berlin Heidelberg, 2010:10-15.

[8] LUO C, SU K, CAI S. More efficient two-mode stochastic local search for random 3-satisfiability [J]. Applied Intelligence, 2014, 41(3):665-680.

[9] 李陽陽, 焦李成. 求解SAT問題的量子免疫克隆算法[J]. 計(jì)算機(jī)學(xué)報(bào), 2007, 30(2):176-183.

[10] 郭瑩, 張長(zhǎng)勝, 張斌. 一種求解SAT問題的人工蜂群算法[J]. 東北大學(xué)學(xué)報(bào)(自然科學(xué)版), 2014, 35(1):29-32.

[11] 郭瑩, 張長(zhǎng)勝, 張斌. 求解SAT問題的算法的研究進(jìn)展[J]. 計(jì)算機(jī)科學(xué), 2016, 43(3):8-17.

[12] HOLLAND J H. Adaptation in natural and artificial systems [M]. Ann Arbor: The University of Michigan Press,1975:21-24.

[13] COLORNI A, DORIGO M, MANIEZZO V. Distributed optimization by Ant Colonies [C]//European Conference on Artificial Life,1991:134-142.

[14] YOUNESS H, IBRAHEIM,A, MONESS M, et al. An efficient implementation of Ant Colony optimization on GPU for the satisfiability problem[J]. 23rd Euromicro International Conference on Parallel, Distributed and Network-Based Processing,2015:230-235.

[15] ZHANG Y A, LI B, MENG Q, et al. The experimental analysis of the efficiency of genetic algorithm based on 3-satisfiability problem[C]// International Conference on Natural Computation. IEEE,2015.

[16] GORBERKO A, POPOV V. A genetic algorithm with expansion and exploration operators for the maximum satisfiability problem[J]. Applied Mathematical Sciences, 2013(21):1183-1190.

[17] 孫如祥, 唐天兵, 李炳慧. 并行蟻群算法求解加權(quán)MAX-SAT[J]. 計(jì)算機(jī)應(yīng)用研究, 2012, 29(1):49-51.

[18] 凌應(yīng)標(biāo), 吳向軍, 姜云飛. 基于子句權(quán)重學(xué)習(xí)的求解SAT問題的遺傳算法[J]. 計(jì)算機(jī)學(xué)報(bào), 2005, 28(9):1476-1482.

(責(zé)任編輯 趙環(huán)宇)

SolvingtheSATProblemBasedonHybridAntColonyandGeneticAlgorithm

WANGLi-dong1,2，WANGNan1，YUJun2

(1.CollegeofComputerScienceandEngineering,BeifangUniversityofNationalities,YinchuanNingxia750021,China；2.SchoolofScience,DalianMinzuUniversity,DalianLiaoning116605,China)

According to the characteristics of the satisfiability problem (SAT), in the analysis of the weakness of the traditional ant colony algorithm and genetic algorithm in solving the SAT problem, we put forward a new kind of solving method of SAT problem based on hybrid ant colony and genetic algorithm (HAG). Improvements are given in the following aspects. Firstly a new method for generating initial solutions is proposed. Then an evolution operator is presented depending on the accumulated information of the suboptimal solutions in the process of iteration. Meanwhile a mutation operator is added by changing literal value in the unsatisfied clause under the condition of current optimal solution. Finally 20 instances are selected from benchmarking sets to test the algorithm. The experimental results showed that in most cases our algorithm has better global searching performance and is able to find the optimal solution through only a few iterations, which has high searching performance and can effectively avoid the premature convergence of ant colony algorithm and genetic algorithm.

satisfiability problem (SAT); hybrid ant colony and genetic algorithm (HAG); evolution operator; mutation operator

2017-02-05；最后

2017-03-28

中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金資助項(xiàng)目(DC201502050201,DC13010318)

王立冬(1955-), 男, 吉林德惠人, 教授, 博士，學(xué)校特聘教授，博士生導(dǎo)師，主要從事拓?fù)鋭?dòng)力系統(tǒng)研究。

余軍(1982-)，男，河南信陽人，講師，博士，主要從事智能規(guī)劃和復(fù)雜網(wǎng)絡(luò)的研究，E-mail:yujun@dlnu.edu.cn。

2096-1383(2017)03-0231-06

TP

A