一種ABCSAT算法的啟發(fā)式初始解策略

周金蓮+郭瑩

摘 要：為了改善初始解在解空間中的分布狀況，根據(jù)SAT問(wèn)題的變量極性差異約束，提出一種啟發(fā)式初始解策略，以解決人工蜂群算法求解策略問(wèn)題。該方法不僅保留了隨機(jī)思想，而且設(shè)置了變量的取值傾向。實(shí)驗(yàn)證明，新策略能夠進(jìn)一步節(jié)約求解時(shí)間和內(nèi)存消耗，提高求解成功率。

關(guān)鍵詞：布爾可滿足性問(wèn)題；人工蜂群算法；初始解；啟發(fā)式

DOIDOI：10.11907/rjdk.172336

中圖分類號(hào)：TP301.6

文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1672-7800（2018）002-0044-03

0 引言

布爾可滿足性問(wèn)題[1]（Boolean Satisfiability Problem，簡(jiǎn)稱SAT問(wèn)題）的基本形式是：給定一個(gè)命題變量集合X和一個(gè)X上的合取范式φ（X），判斷是否存在一個(gè)真值賦值t（X），使得φ（X）為真。如果能找到，則稱φ（X）是可滿足的（satisfiable），否則稱φ（X）是不可滿足的（unsatisfiable）。SAT問(wèn)題是世界上第一個(gè)被證明的NPC問(wèn)題[2]，在計(jì)算機(jī)科學(xué)、人工智能等理論和應(yīng)用領(lǐng)域起著重要作用[3-5]，其中SAT問(wèn)題求解是目前的一個(gè)重要研究分支[6]。

人工蜂群（Artificial Bee Colony，簡(jiǎn)稱ABC）算法[7]是近年來(lái)興起的一種群智能進(jìn)化算法，在許多優(yōu)化問(wèn)題上表現(xiàn)出了比差分進(jìn)化、粒子群和遺傳算法等更好的性能[8]。本文提出一種新的ABCSAT算法[9]，已經(jīng)成功利用ABC算法初步求解SAT問(wèn)題。

ABCSAT求解算法繼承了標(biāo)準(zhǔn)ABC算法的基本思想。首先隨機(jī)生成SN個(gè)蜜源，并計(jì)算其適應(yīng)度；雇傭蜂與蜜源一一對(duì)應(yīng)，對(duì)每個(gè)蜜源鄰域進(jìn)行搜索，發(fā)現(xiàn)更優(yōu)解時(shí)則進(jìn)行替換；跟隨蜂根據(jù)一定概率選擇跟隨的雇傭蜂，深入局部搜索；偵察蜂放棄連續(xù)limit次沒(méi)有被改進(jìn)的雇傭蜂或跟隨蜂，并重新初始一個(gè)解；覓食過(guò)程是雇傭蜂、跟隨蜂和偵察蜂3個(gè)覓食階段的反復(fù)迭代過(guò)程，直到達(dá)到搜索終止條件或找到問(wèn)題的解。

1 初始解基本方法

在ABC算法中，一個(gè)蜜源表示待優(yōu)化問(wèn)題的一個(gè)可能解，蜜源的豐富程度代表解的質(zhì)量（即適應(yīng)度），蜜蜂覓食的過(guò)程便是尋找具有最大適應(yīng)度值的最優(yōu)解過(guò)程。初始化時(shí)，通過(guò)式（1）隨機(jī)生成含有SN（Solution Number）個(gè)解的初始蜂群，每個(gè)雇傭蜂被賦予一個(gè)初始位置，本文用D維向量Xi表示第i個(gè)蜜源，其中Xi=xij（i=1，2，3，…，SN， j=1，2，…D）。

ABCSAT求解算法是一種基于群體尋優(yōu)的算法，算法運(yùn)行時(shí)以蜂群的形式在搜索空間內(nèi)搜索。蜂群表示雇傭蜂和跟隨蜂對(duì)應(yīng)的蜜源，每個(gè)蜜源對(duì)應(yīng)問(wèn)題的一個(gè)可能解。

蜂群中蜜源的數(shù)量SN稱為蜜源大小或種群規(guī)模，表示可能解的數(shù)量，一般是一個(gè)不變的常數(shù)，通常蜜源的個(gè)數(shù)等于雇傭蜂或跟隨蜂的個(gè)數(shù)。在一些特殊情況下，蜜源大小也可能采用與迭代次數(shù)相關(guān)的變量，以獲取更好的優(yōu)化效果。一般來(lái)說(shuō)，當(dāng)SN很小時(shí)，陷入局部最優(yōu)的可能性就會(huì)增大。但隨著SN的增大，運(yùn)行時(shí)間也將增大，并且當(dāng)SN增長(zhǎng)至一定水平時(shí)收斂速度將非常慢。如果不考慮運(yùn)行時(shí)間因素，可以采用大的種群，但在運(yùn)行時(shí)間要求很短且配置環(huán)境不是非常好的情況下，建議采用較小的種群。本文對(duì)不同規(guī)模的種群進(jìn)行了實(shí)驗(yàn)分析，建議選用種群大小為20。

初始蜂群是算法搜索的起點(diǎn)，在解空間中的分布狀況會(huì)對(duì)算法搜索性能產(chǎn)生影響，一般采用隨機(jī)方法產(chǎn)生。初始化時(shí)，隨機(jī)生成SN個(gè)蜜源，雇傭蜂和跟隨蜂的個(gè)數(shù)均為SN，其中雇傭蜂與蜜源一一對(duì)應(yīng)。由于SAT問(wèn)題的每個(gè)變量均為布爾變量，因此隨機(jī)產(chǎn)生ξij∈U（0，1），Sij通過(guò)公式（2）生成：

算法初始候選解后，循環(huán)執(zhí)行雇傭蜂、跟隨蜂和偵察蜂覓食步驟，直到找到問(wèn)題的解或達(dá)到最大迭代次數(shù)。

2 啟發(fā)式初始解方法

初始解的好壞對(duì)搜索性能影響很大，然而，完全隨機(jī)的初始解可能經(jīng)過(guò)很多搜索步驟也難以找到一個(gè)可行解[10]。因此，本文嘗試從研究問(wèn)題的約束入手，在隨機(jī)初始化過(guò)程中加入啟發(fā)式方法。

2.1 變量極性差異

由于任何一個(gè)命題邏輯公式都可在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)化為合取范式（Conjunctive Normal Form，簡(jiǎn)稱CNF），主流的SAT求解算法通常假設(shè)目標(biāo)公式已被處理為CNF形式。CNF公式指由若干子句合取構(gòu)成的公式，可簡(jiǎn)單描述為式（3）：

式（3）中，k表示每個(gè)子句中文字的個(gè)數(shù)，m表示子句的個(gè)數(shù)，li，j表示出現(xiàn)在第i個(gè)子句的第j個(gè)文字。

對(duì)任意變量xi，符號(hào)xi和xi是其文字，稱xi是正文字，xi是負(fù)文字。文字的正負(fù)稱作符號(hào)（sign）或相（phase）。用L表示所有文字的集合，l表示某個(gè)文字，L={l1，l2，l3，…，lk}。

定義1（變量出現(xiàn)次數(shù)，Variable Occurrence Number，簡(jiǎn)稱von）：vonx=count（C）（C∈φ∧（x∈C∨x∈C）），表示出現(xiàn)變量x的子句個(gè)數(shù)。vonlx=count（C）（C∈φ∧x∈C），表示出現(xiàn)變量x正文字形式的子句個(gè)數(shù)。vonlx=count（C）（C∈φ∧x∈C），表示出現(xiàn)變量x負(fù)文字形式的子句個(gè)數(shù)。存在式（4）成立：

定義2（變量極性差異，Variable Polarity Difference，簡(jiǎn)稱vpd）：變量正負(fù)文字出現(xiàn)的次數(shù)之差占變量出現(xiàn)總次數(shù)的比例，如式（5）所示，當(dāng)vpd=1時(shí)，變量以純文字形式出現(xiàn)，vpd大于0時(shí)表示正文字出現(xiàn)次數(shù)多于負(fù)文字出現(xiàn)次數(shù)，反之則表示負(fù)文字出現(xiàn)次數(shù)多于正文字出現(xiàn)次數(shù)，vpd取值范圍為[-1，1]。

2.2 啟發(fā)式初始解

通過(guò)對(duì)公式的一次遍歷掃描就可方便地對(duì)原始公式中各變量正負(fù)文字出現(xiàn)次數(shù)vonj和vonj進(jìn)行統(tǒng)計(jì)。顯然，若一個(gè)變量以純文字形式出現(xiàn)，當(dāng)僅以正文字形式出現(xiàn)時(shí)，可將該變量賦值為1，反之，當(dāng)僅以負(fù)文字形式出現(xiàn)時(shí)則可立即將該變量賦值為0。此操作可立即使該變量出現(xiàn)的所有子句變?yōu)榭蓾M足狀態(tài)，從而減少求解空間。endprint

根據(jù)式（6）生成的初始解，如果變量以正文形式出現(xiàn)次數(shù)多，則傾向于取初值為1，反之取值為0。同時(shí)繼續(xù)保留設(shè)置隨機(jī)參數(shù)ξij，保證了初始解的多樣性。

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

3.1 實(shí)驗(yàn)設(shè)計(jì)

本實(shí)驗(yàn)重點(diǎn)驗(yàn)證啟發(fā)式初始解策略在求解隨機(jī)類CNF問(wèn)題上的作用。SAT2014國(guó)際競(jìng)賽的隨機(jī)類實(shí)例均為可滿足的，本節(jié)從中隨機(jī)選取20個(gè)實(shí)例進(jìn)行測(cè)試，問(wèn)題規(guī)模分大中小型，如表1所示。

實(shí)驗(yàn)環(huán)境：Intel（R） Core（TM） i5650@3.20GHZ 4核處理器、4G內(nèi)存、64位操作系統(tǒng)，在Oracle VM VirtualBox5.0虛擬機(jī)上安裝64位Ubuntu Linux操作系統(tǒng)、分配2核CPU、1G內(nèi)存。編譯環(huán)境為GCC 4.8.4，選擇C++語(yǔ)言工具。

從求解成功率suc、求解時(shí)間消耗t、內(nèi)存消耗m等指標(biāo)角度與傳統(tǒng)方法進(jìn)行整體性能評(píng)價(jià)分析。為了檢驗(yàn)算法的平均性能與穩(wěn)定性，對(duì)每個(gè)實(shí)例求解10次，結(jié)果記錄其平均值。

3.2 實(shí)驗(yàn)結(jié)果分析

實(shí)驗(yàn)采用傳統(tǒng)的完全隨機(jī)方法及啟發(fā)式隨機(jī)賦值方法，求解結(jié)果如表2所示。

可以看出，不同的初始解方法能影響求解性能，采取啟發(fā)式隨機(jī)賦值后能夠進(jìn)一步節(jié)約求解時(shí)間和內(nèi)存消耗，提高求解成功率。

啟發(fā)式方法立足問(wèn)題本身特征，初始解更接近于問(wèn)題的最終解，從而減少了搜索過(guò)程的迭代次數(shù)，保留了隨機(jī)化思想，保證了初始解的多樣性。

4 結(jié)語(yǔ)

初始解是算法進(jìn)行搜索的起點(diǎn)，其在解空間中的分布狀況會(huì)對(duì)算法性能產(chǎn)生影響。本文提出了一種基于變量極性差異的啟發(fā)式初始解策略，實(shí)驗(yàn)證明了這種方法的有效性。

參考文獻(xiàn)：

[1] BIERE A， HEULE M， VAN MAAREN H. Handbook of satisfiability[M].IOS Press，2009.

[2] COOK S A. The complexity of theorem proving procedures[C].Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing，New York，1971：151-158.

[3] KUMAR D， MISHRA K K. Artificial bee colony as a frontier in evolutionary optimization： a survey[M]. Advances in Computer and Computational Sciences. Springer， Singapore，2017：541-548.

[4] AKAY B， KARABOGA D. A survey on the applications of artificial bee colony in signal， image， and video processing[J].Signal， Image and Video Processing，2015，9（4）：967-990.

[5] TEODOROVIC' D， ELMIC' M， DAVIDOVIC' T. Bee colony optimization-part II： the application survey[J]. Yugoslav Journal of Operations Research，2015，25（2）：185-219.

[6] BALYO T， HEULE M J H， JRVISALO M. SAT competition 2016： recent developments[C]. Proc. the thirty-first AAAI conference on artificial intelligence， AAAI，2017：5061-5063.

[7] KARABOGA D， BASTURK B. A powerful and efficient algorithm for numerical function optimization： artificial bee colony （ABC） algorithm[J]. Journal of global optimization，2007，39（3）：459-471.

[8] KARABOGA D， GORKEMLI B， OZTURK C， et al. A comprehensive survey： artificial bee colony （ABC） algorithm and applications[J].Artificial Intelligence Review，2014，42（1）：21-57.

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

[10] BALINT A. Engineering stochastic local search for the satisfiability problem[D]. Universitt Ulm：Fakultt für Ingenieurwissenschaften und Informatik，2014.endprint