一种ABCSAT算法的启发式初始解策略

周金莲+郭莹

摘 要：为了改善初始解在解空间中的分布状况，根据SAT问题的变量极性差异约束，提出一种启发式初始解策略，以解决人工蜂群算法求解策略问题。该方法不仅保留了随机思想，而且设置了变量的取值倾向。实验证明，新策略能够进一步节约求解时间和内存消耗，提高求解成功率。

关键词：布尔可满足性问题；人工蜂群算法；初始解；启发式

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]是近年来兴起的一种群智能进化算法，在许多优化问题上表现出了比差分进化、粒子群和遗传算法等更好的性能[8]。本文提出一种新的ABCSAT算法[9]，已经成功利用ABC算法初步求解SAT问题。

ABCSAT求解算法继承了标准ABC算法的基本思想。首先随机生成SN个蜜源，并计算其适应度；雇佣蜂与蜜源一一对应，对每个蜜源邻域进行搜索，发现更优解时则进行替换；跟随蜂根据一定概率选择跟随的雇佣蜂，深入局部搜索；侦察蜂放弃连续limit次没有被改进的雇佣蜂或跟随蜂，并重新初始一个解；觅食过程是雇佣蜂、跟随蜂和侦察蜂3个觅食阶段的反复迭代过程，直到达到搜索终止条件或找到问题的解。

1 初始解基本方法

在ABC算法中，一个蜜源表示待优化问题的一个可能解，蜜源的丰富程度代表解的质量（即适应度），蜜蜂觅食的过程便是寻找具有最大适应度值的最优解过程。初始化时，通过式（1）随机生成含有SN（Solution Number）个解的初始蜂群，每个雇佣蜂被赋予一个初始位置，本文用D维向量Xi表示第i个蜜源，其中Xi=xij（i=1，2，3，…，SN， j=1，2，…D）。

ABCSAT求解算法是一种基于群体寻优的算法，算法运行时以蜂群的形式在搜索空间内搜索。蜂群表示雇佣蜂和跟随蜂对应的蜜源，每个蜜源对应问题的一个可能解。

蜂群中蜜源的数量SN称为蜜源大小或种群规模，表示可能解的数量，一般是一个不变的常数，通常蜜源的个数等于雇佣蜂或跟随蜂的个数。在一些特殊情况下，蜜源大小也可能采用与迭代次数相关的变量，以获取更好的优化效果。一般来说，当SN很小时，陷入局部最优的可能性就会增大。但随着SN的增大，运行时间也将增大，并且当SN增长至一定水平时收敛速度将非常慢。如果不考虑运行时间因素，可以采用大的种群，但在运行时间要求很短且配置环境不是非常好的情况下，建议采用较小的种群。本文对不同规模的种群进行了实验分析，建议选用种群大小为20。

初始蜂群是算法搜索的起点，在解空间中的分布状况会对算法搜索性能产生影响，一般采用随机方法产生。初始化时，随机生成SN个蜜源，雇佣蜂和跟随蜂的个数均为SN，其中雇佣蜂与蜜源一一对应。由于SAT问题的每个变量均为布尔变量，因此随机产生ξij∈U（0，1），Sij通过公式（2）生成：

算法初始候选解后，循环执行雇佣蜂、跟随蜂和侦察蜂觅食步骤，直到找到问题的解或达到最大迭代次数。

2 启发式初始解方法

初始解的好坏对搜索性能影响很大，然而，完全随机的初始解可能经过很多搜索步骤也难以找到一个可行解[10]。因此，本文尝试从研究问题的约束入手，在随机初始化过程中加入启发式方法。

2.1 变量极性差异

由于任何一个命题逻辑公式都可在多项式时间内转化为合取范式（Conjunctive Normal Form，简称CNF），主流的SAT求解算法通常假设目标公式已被处理为CNF形式。CNF公式指由若干子句合取构成的公式，可简单描述为式（3）：

式（3）中，k表示每个子句中文字的个数，m表示子句的个数，li，j表示出现在第i个子句的第j个文字。

对任意变量xi，符号xi和xi是其文字，称xi是正文字，xi是负文字。文字的正负称作符号（sign）或相（phase）。用L表示所有文字的集合，l表示某个文字，L={l1，l2，l3，…，lk}。

定义1（变量出现次数，Variable Occurrence Number，简称von）：vonx=count（C）（C∈φ∧（x∈C∨x∈C）），表示出现变量x的子句个数。vonlx=count（C）（C∈φ∧x∈C），表示出现变量x正文字形式的子句个数。vonlx=count（C）（C∈φ∧x∈C），表示出现变量x负文字形式的子句个数。存在式（4）成立：

定义2（变量极性差异，Variable Polarity Difference，简称vpd）：变量正负文字出现的次数之差占变量出现总次数的比例，如式（5）所示，当vpd=1时，变量以纯文字形式出现，vpd大于0时表示正文字出现次数多于负文字出现次数，反之则表示负文字出现次数多于正文字出现次数，vpd取值范围为[-1，1]。

2.2 启发式初始解

通过对公式的一次遍历扫描就可方便地对原始公式中各变量正负文字出现次数vonj和vonj进行统计。显然，若一个变量以纯文字形式出现，当仅以正文字形式出现时，可将该变量赋值为1，反之，当仅以负文字形式出现时则可立即将该变量赋值为0。此操作可立即使该变量出现的所有子句变为可满足状态，从而减少求解空间。endprint

根据式（6）生成的初始解，如果变量以正文形式出现次数多，则倾向于取初值为1，反之取值为0。同时继续保留设置随机参数ξij，保证了初始解的多样性。

3 实验分析

3.1 实验设计

本实验重点验证启发式初始解策略在求解随机类CNF问题上的作用。SAT2014國际竞赛的随机类实例均为可满足的，本节从中随机选取20个实例进行测试，问题规模分大中小型，如表1所示。

实验环境：Intel（R） Core（TM） i5650@3.20GHZ 4核处理器、4G内存、64位操作系统，在Oracle VM VirtualBox5.0虚拟机上安装64位Ubuntu Linux操作系统、分配2核CPU、1G内存。编译环境为GCC 4.8.4，选择C++语言工具。

从求解成功率suc、求解时间消耗t、内存消耗m等指标角度与传统方法进行整体性能评价分析。为了检验算法的平均性能与稳定性，对每个实例求解10次，结果记录其平均值。

3.2 实验结果分析

实验采用传统的完全随机方法及启发式随机赋值方法，求解结果如表2所示。

可以看出，不同的初始解方法能影响求解性能，采取启发式随机赋值后能够进一步节约求解时间和内存消耗，提高求解成功率。

启发式方法立足问题本身特征，初始解更接近于问题的最终解，从而减少了搜索过程的迭代次数，保留了随机化思想，保证了初始解的多样性。

4 结语

初始解是算法进行搜索的起点，其在解空间中的分布状况会对算法性能产生影响。本文提出了一种基于变量极性差异的启发式初始解策略，实验证明了这种方法的有效性。

参考文献：

[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