一种求解SAT问题的人工蜂群算法

针对SAT问题，提出一种求解该问题的离散人工蜂群算法——ABCSAT算法，建立了相应的优化算法模型，解决了问题编码和转化、适应度函数、蜜蜂觅食策略、离散操作等关键问题.不同于处理连续优化问题，ABCSAT将适应度函数定义为当前不可满足子句数.根据问题的特点设计了多种觅食策略，并利用各子句和变量之间约束关系的启发式信息对各阶段的候选解进行离散操作.最后在标准SATLIB测试集上对提出的算法进行了测试并与相关算法进行了比较，结果验证了ABCSAT算法在中小规模SAT问题上的有效性，表明算法能更加有效地解决该问题.

An Artificial Bee Colony Algorithm for Solving SAT Problem

For SAT problem， a discrete artificial bee colony algorithm named ABCSAT algorithm was proposed. The corresponding optimization model was established， and the key issues such as problem encoding and transition， fitness function， bee’s foraging strategy， discrete operation etc. were solved. Different from dealing with continual optimization problem， fitness function was defined as the number of unsatisfied clauses in the ABCSAT algorithm. According the character of SAT problem， series of foraging strategy were designed and discrete operations on candidate solutions were performed by using the heuristic information of constraint relations among each clause and variable. Through experiments on the standard SATLIB benchmarks， the algorithm was tested and compared with related algorithms. The results validated the effectiveness of ABCSAT algorithm on middle/small scale SAT problems， and showed that the algorithm could be more effectively on solving this problem.