组织进化算法求解SAT问题

基于组织的概念设计了一种新的进化算法——求解SAT问题的组织进化算法(Organizational Evolutionary Algorithm for SAT problem，0EASAT)．OEASAT将SAT问题分解成若干子问题，然后用每个子问题形成一个组织，并根据SAT问题的特点设计了三种组织进化算子——自学习算子、吞并算子和分裂算子以引导组织的进化．根据组织的适应度，将所有组织分成两个种群——最优种群和非最优种群，然后用进化的方式来控制各算子，以协调各组织间的相互作用．OEASAT通过先解决子问题，再协调相冲突变量的方式来求解SAT问题．由于子问题的规模较小，相对于原问题来说较容易解决，这样就达到了降低问题复杂度的目的．实验用标准SATLIB库中变量个数从20-250的3700个不同规模的标准SAT问题对OEASAT的性能作了全面的测试，并与著名的WalkSAT和RFEA2的结果作了比较．结果表明，OEASAT具有更高的成功率和更高的运算效率．对于具有250个变量、1065个子句的SAT问题，OEASAT仅用了1．524s，表现出了优越的性能．

An Organizational Evolutionary Algorithm for SAT Problem

Based on the concept of organization, a novel evolutionary algorithm, Organizational Evolutionary Algorithm for SAT problem (OEASAT), is proposed to deal with the satisfiability problem. OEASAT first divides a SAT problem into several sub-problems, and forms an organization by each sub-problem. Three new evolutionary operators, the self-learning operator, the annexing operator and the splitting operator, are designed with the intrinsic properties of SAT problems in mind. Furthermore, all organizations are divided into two populations according to their fitness. One is the best population, and the other is the not best population. Then, the evolutionary operators are controlled by means of evolution, so that the populations can evolve. The idea of OEASAT is to solve the sub-problem first, and then synthesize the solution of the original problem. Since the scale of the sub-problems is smaller than that of the original problem, this method can reduce the complexity of the problems. In the experiments, 3700 benchmark SAT problems in SATLIB are used to test the performance of OEASAT. The number of variables of these problems ranges from 20 to 250. Moreover, the performance of OEASAT is compared with those of two well-known algorithms, WalkSAT and RFEA2. All experimental results show that OEASAT has a higher success ratio and a lower computational cost. OEASAT can solve the problems with 250 variables and 1065 clauses by only 1 524 seconds and outperforms all other algorithms.