基于混合蚁群遗传算法的SAT问题求解

王立冬，王 楠，余 军

(1. 北方民族大学 计算机科学与工程学院，宁夏 银川 750021；2. 大连民族大学 理学院，辽宁 大连 116605)

基于混合蚁群遗传算法的SAT问题求解

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

(1. 北方民族大学 计算机科学与工程学院，宁夏 银川 750021；2. 大连民族大学 理学院，辽宁 大连 116605)

根据SAT问题的特点，通过分析传统蚁群算法和遗传算法在求解SAT问题上的不足，提出一种基于混合蚁群遗传算法的SAT问题求解方法。给出一种新的初始解的生成方式；在迭代过程中，根据较优解的累积信息提出进化算子；利用当前得到的最优解，通过改变不满足子句中文字的取值，增加变异算子。最后选取标准测试集中的20个实例对算法进行测试，实验结果表明：改进后的算法通常仅通过较少次数的迭代就能找到解，能够有效避免蚁群算法和遗传算法过早收敛的缺点，具有较强的寻优能力。

可满足性问题；混合蚁群遗传算法；进化算子；变异算子

可满足性问题(Satisfiability Problem, SAT)是第一个被Cook定理证明的NP完全问题，即多项式复杂程度的非确定性问题，判定对于一个命题范式，是否存在一组范式中变量的赋值使得该范式为真。目前，解决该问题的方法主要有完备方法和不完备方法。完备的方法包括DP算法[1]、DPLL等[2]，该类方法可以正确地判断SAT问题的可满足性，但计算复杂度较高，对于大规模SAT问题，这种算法的效率很低；不完备方法基于Local Search算法[3-4]，包括GSAT[5]，WALKSAT[6]等，这类方法的求解速度往往比完备算法快很多。

国内外许多学者对如何求解SAT问题都做了大量的研究，文献[7]利用启发式函数来计算不满足子句中文字所对应的命题变元的概率分布权值，然后根据变元的权值来选取翻转变元进行翻转，这在求解3-SAT问题方面有突出的表现；文献[8]翻转变元的选取既考虑到可满足子句增加的数目又考虑到变元选取的合理性，避免翻转变元的重复选取，并结合跳出策略避免陷入局部最优解，使得算法朝着能够减少不满足子句数目的方向进行搜索；西安电子科技大学的李阳阳等在文献[9]中提出一种基于量子编码的免疫克隆算法来求解SAT问题；东北大学的郭莹等在文献[10]中提出一种求解SAT问题的离散人工蜂群算法，之后在文献[11]中从完备算法、不完备算法和组合算法3个角度总结了SAT问题的研究进展。

遗传算法(Genetic Algorithm,GA)[12]和蚁群算法(Ant Colony Optimization, ACO)[13]在求解组合优化问题方面有着自身的优势。文献[14]使用并行策略的ACO优化算法解决SAT问题；文献[15]通过评估遗传算子的计算效率和相关参数来求解3-SAT问题；文献[16]在遗传算法的基础上通过扩张和调查算子求解最大化可满足性问题；广西大学的孙如祥等在文献[17]中针对加权SAT问题的特点，以重离散化方式简化蚁群算法模型，提出取值概率的概念，并以之替换传统蚁群算法中的信息素，最后对该算法做并行化改进；中山大学的凌应标等在文献[18]中将SAT问题的结构信息量化为子句权重，增加了学习算子和判定早熟参数，并采用最优染色体保存策略，防止进化过程的发散。

通过随机赋值方法生成的初始解的质量不高，导致接下来的迭代过程中解的收敛速度较慢，影响寻优能力；遗传算法的交叉算子具有较大的盲目性，交叉得到的新解的质量往往并没有提高，没有能够有效利用迭代过程所累积的信息。将遗传算法和蚁群算法进行结合，能够很好地互补。

1 SAT问题的定义

定义1 文字(Literal)

定义2 子句(Clause)

子句c都是由若干个文字通过析取运算符(∨)链接而成，子句中文字的个数称为子句的长度，当子句中至少有一个文字为真时则该子句为真。如长度为2的子句c=(x1∨x2)，当x1=1或x2=0时该子句都为真。

定义3 可满足性问题(SAT)

(1)

显然当fit(S)=0时，该SAT问题在赋值S下是可满足的。为了叙述方便，下文中这样的真值指派S也称为解。

2 基于混合蚁群遗传算法的SAT问题求解

2.1 初始解生成方式的改进

在遗传算法中，先得到N个初始解，而每个解中的文字都被随机赋值为1或-1，这样生成的解具有很大的盲目性，同时解的整体质量不高，在一定程度上影响SAT问题是否可以找到最优解。本文提出一种新的初始解的生成方法，提高了初始解的质量，有利于在后续迭代过程中找到最优解。

(1)初始化解中的部分文字。规则如下：给定两个阈值α1和α2，且满足条件0<α2<α1<1，对每个文字，生成随机数r∈(0,1)。若r<α2时，该文字不被赋值；若α2≤r<α1，则将该文字赋值为-1；若r≥α1，则将该文字赋值为1。为了保证文字被赋值为1或-1的概率相等，即α1和α2的取值应满足2α1=1+α2，而α2的取值直接影响初始被赋值文字的多少。实际上，α2的值越接近于0，总体上被赋值的文字就越多，生成初始解的速度相对越快，初始解的质量越低；反之，α2的值越接近于1，则总体上被赋值的文字就越少，初始解的整体质量越高。α2的取值可以根据具体的问题做相应的调整，如α2=0，则所有文字都被随机赋值，这样得到的初始解与随机生成初始解无异，在没有已知信息的情况下，对初始解进行赋值时，要选取相对较小的α2的值。

(2)根据给定的规则更新子句集合。对每个子句，逐一根据每个文字的赋值情况对其进行更新：如果该子句中的当前文字为真，则将该子句从子句集合中删除；如果当前文字为假，则将该文字从该子句中删除，并用删除文字之后的子句替换原子句；如果当前文字没有被赋值，则该子句不做任何变化。

(3)根据更新之后的子句集合，判断每个子句的长度。如果子句的长度为0，即空子句，那么就将该子句从子句集合中直接删除。如果子句长度为1,则根据该子句中当前文字的正负，将文字赋值使得该子句为真，并统计被赋值文字的个数m，根据m的大小又分两种情况：如果m大于给定的阈值M，则直接返回上一步；如果m≤M，可以再次随机赋值部分文字后返回上一步。M的取值可以根据具体的问题作相应的调整，M越小，生成初始解的速度越慢，解的质量越高。

(4)不断重复步骤(2)、(3)直到子句集合为空，最终得到一个初始解。

改进后的初始解的生成方式可以提高初始解的质量，降低初始解的随机性，更好地作用在接下来的交叉和变异等步骤中，使得问题的解向更优的方向进化，提高了算法的有效性。

2.2 计算适应度函数值

计算每个解的适应度函数值fit(S)，根据fit(S)的大小，对所有解按照从小到大排序。

2.3 选择算子

在确定选择概率的情况下，根据排序结果选择适应度函数值小的解作为算子。这样能够保证较优秀的解在迭代过程中不至于丢失，仅遗传极少部分解到下一代中，能够有效避免算法收敛过快，即陷入局部最优的困境。

2.4 交叉算子

先确定交叉概率，同样根据排序结果选择较优秀的两个解进行交叉操作，将交叉之后得到的新解放到下一代中。由于交叉算子具有很大的盲目性，并不能够保证交叉之后的解较父代更加优秀，所以选择较小的交叉概率，即仅仅交叉生成极少部分解。

2.5 进化算子

若xi=1，

(2)

若xi=-1，

(3)

然后，根据信息素矩阵生成新的解。分为三个步骤：

第二步，根据当前解更新子句集合，更新规则和生成初始解时更新子句集合的规则相同。若存在长度为1的子句，则将该文字赋值使得该子句为真。同时统计剩余子句集合中各个文字出现的次数，若该文字只以正文字出现，则将该文字直接赋值为1；类似的若该文字只以负文字出现，则将该文字赋值为-1。这样，解中又有部分文字可能被赋值，如果此次被赋值的文字相对较多，则可以重新更新子句集合，重复上述过程。

第三步，如果被赋值的文字相对较少，则根据第二步的统计结果将出现次数相对较多的部分文字优先赋值，赋值的方法和第一步类似。不断的重复第二、三步，直到子句集合为空为止。最后将得到的新解加入下一代解的集合中。

在进化算子生成部分新解结束之后，为了避免算法陷入局部最优，累积信息素矩阵内的信息存在一定程度的挥发，挥发系数ρ通常介入0到1之间，更新公式为

A2×n=ρ×A2×n。

(4)

进化算子的流程图如图1。

图1 进化算子流程图

2.6 变异算子

对遗传算法中的变异算子进行改进，使得改进后的变异算子更具有针对性，以增强其找到最优解的能力。采用精英解策略，即选择当前最优的解进行变异操作，分为三步。

第三，判断翻转之后的最优解是否比之前更优，如果是则保存当前解到下一代中；否则重复第二步的过程，如果重复的次数大于给定的限制，则结束这个过程，保存当前的次优解到下一代中。

在迭代过程中，若存在一组真值指派S，使得fit(S)=0，即合取范式F中所有子句都为真时，循环提前结束，并输出当前的真值指派；否则迭代继续进行，直到达到最大的迭代次数为止。

混合蚁群遗传算法流程如图2。

图2 混合蚁群遗传算法

3 实验分析

为了验证混合蚁群遗传算法在求解SAT问题(HAGSAT)时的有效性，从标准测试库SATLIB中选取20个实例进行测试，选取的测试集见表1，其中详细列举了每个测试实例的名称、子句数和变量数。

表1 SAT问题测试实例

利用测试实例对初始解的质量进行测试，测试结果如图3。

图3 初始解的质量对比

从图3中可以看出，和传统随机生成初始解的方式相比，不仅最优解的质量有了显著提高，整个初始解集的质量也有很大的提升，通过本文算法生成的初始解可以满足的子句个数非常接近每个实例的子句总个数，提高了后续迭代寻优过程的效率。

本文算法(HAGSAT)、遗传算法(GASAT)和蚁群算法(ACOSAT)在20个实例中测试结果见表2。N为实例序号；n为种群大小；t为每个实例测试的次数；i为迭代次数；suc为成功找到解的总次数；ave为成功找到解时的平均迭代次数；nf为无法找到解时的不满足子句的平均数。

表2 实验结果对比

通过表2可以看出，本文使用的混合蚁群遗传算法无论在求解速度还是求解质量等方面都要明显优于其它两种算法。

第一，从成功找到解的次数方面来看，本文算法在规定的测试次数内，找到解的次数要明显高于其它两种算法，且成功率高。例如：在实例3的10次测试中，本文算法有8次成功找到问题的解，GASAT没有找到问题的解，ACOSAT只有1次找到问题的解；在实例4的10次测试中，本文算法10次都成功找到问题的解，GASAT有4次找到问题的解，ACOSAT没有找到问题的解；在实例20的50次测试中，本文算法在50次内都成功找到问题的解，GASAT有23次找到问题的解，ACOSAT有28次找问题的解。

第二，从找到解时的平均迭代次数来看，本文算法成功找到解的平均迭代次数要远低于其它两种算法，速度较快。例如：实例1最大迭代15次，本文算法平均迭代2次就能成功找到问题的解，而GASAT需要平均迭代8.7次才可以找到解，ACOSAT平均迭代4.3次找到解；实例5最大迭代30次，本文算法平均迭代2.1次就能成功找到问题的解，GASAT平均迭代11.6次才可以找到解，ACOSAT在30次的迭代过程中没有找到解；实例12最大迭代20次，本文算法平均迭代7.5次就可以找到问题的解，而GASAT和ACOSAT在20次的迭代过程中没有找到解。

第三，从无法找到解时的不满足子句的数量方面来看，本文算法无法找到解时的不满足子句的平均数要低于其它两种算法。例如：在实例6的684个子句中，本文算法在无法找到解时的不满足子句平均个数为1.3个，GASAT算法下的不满足子句平均个数为4.8个，ACOSAT算法下的不满足子句平均个数为为1.5个；在实例13的830个子句中，本文算法在无法找到解时的不满足子句平均个数为2个，GASAT算法下的不满足子句平均个数为7.5个，ACOSAT算法下的不满足子句平均个数为为4.2个；在实例14的875个子句中，本文算法在无法找到解时的不满足子句平均个数为7个，GASAT算法下的不满足子句平均个数为19个，ACOSAT算法下的不满足子句平均个数为为11个。

综上所述，针对不同子句和不同变量个数的SAT问题，本文采用的混合蚁群遗传算法都能够有效的求解测试实例且成功率较高，成功找到解的次数要明显高于遗传算法和蚁群算法，而成功找到解时的平均迭代次数和无法找到解时的不满足的子句的平均数都要低于遗传算法和蚁群算法。

4 结 论

本文根据蚁群算法和遗传算法各自的优势，并结合SAT问题的特点，对两种算法进行了改进和融合，给出了进化算子和变异算子，提高了混合蚁群遗传算法的寻优能力和求解效率。在标准测试库SATLIB中选取了20个实例进行测试，测试结果表明本文算法在求解SAT问题上优于蚁群算法和遗传算法。事实上，通过大多数测试实例的结果可以看出，仅通过较小的种群规模和较少的迭代次数就能找到真解，反过来较大的种群规模和较多迭代次数也不一定能保证找到解。同时注意到初始解集往往对最终的寻优结果有较大的影响，不合适的初始解集意味着更多的迭代次数，甚至陷入局部最优而根本跳不出来。为了避免出现这类情况，可以考虑该算法的并行模式，即同时生成多个种群，每个种群都是独立、互不干扰的，当有某个种群找到真解时，迭代结束。在后续的实验中，可继续对该算法进行完善并改进以适应不同类型的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]. 计算机学报, 2007, 30(2):176-183.

[10] 郭莹, 张长胜, 张斌. 一种求解SAT问题的人工蜂群算法[J]. 东北大学学报(自然科学版), 2014, 35(1):29-32.

[11] 郭莹, 张长胜, 张斌. 求解SAT问题的算法的研究进展[J]. 计算机科学, 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] 孙如祥, 唐天兵, 李炳慧. 并行蚁群算法求解加权MAX-SAT[J]. 计算机应用研究, 2012, 29(1):49-51.

[18] 凌应标, 吴向军, 姜云飞. 基于子句权重学习的求解SAT问题的遗传算法[J]. 计算机学报, 2005, 28(9):1476-1482.

(责任编辑 赵环宇)

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

中央高校基本科研业务费专项资金资助项目(DC201502050201,DC13010318)

王立冬(1955-), 男, 吉林德惠人, 教授, 博士，学校特聘教授，博士生导师，主要从事拓扑动力系统研究。

余军(1982-)，男，河南信阳人，讲师，博士，主要从事智能规划和复杂网络的研究，E-mail:yujun@dlnu.edu.cn。

2096-1383(2017)03-0231-06

TP

A