An Organizational Evolutionary Algorithm for SAT Problem
Jing Liu · Chinese Journal of Computers · 2004
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.