周金蓮+郭瑩

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

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

DOIDOI：10.11907/rjdk.172336

中圖分類號：TP301.6

文獻標識碼：A 文章編號：1672-7800（2018）002-0044-03

0 引言

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

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

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

1 初始解基本方法

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

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

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

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

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

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

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

2.1 變量極性差異

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

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

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

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

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

2.2 啟發(fā)式初始解

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

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

3 實驗分析

3.1 實驗設計

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

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

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

3.2 實驗結果分析

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

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

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

4 結語

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

參考文獻：

[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] 郭瑩，張長勝，張斌.一種求解SAT問題的人工蜂群算法[J].東北大學學報：自然科學版，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