Reasearch On Genetic Algorithm-based SAT Problem Solving

In Boolean logic, a formula is satisfiable if a variable assignment exists that will make the formula equivalent to true, and the propositional satisfiability problem (SAT) is to determine if a given formula is satisfiable. SAT is one of the most fundamental problems in computer science, and since many relevant combinatorial problems can be encoded into SAT,it is of substantial theoretical and practical interest. Since the birth of genetic algorithm and because of its own advantages, it is widely applied to combinatorial optimization field. But It may be easy to fall in premature trap and be poor efficiency in the searching solution. This paper will introduce the concept of family genealogy tree to the genetic algorithm, and propose with improved genetic operator for solving the SAT problem, which are greedy crossover operator, random walk crossover operator and clause variable punishment crossover operator effectively improving the success rate and convergence speed. As well as other local search algorithms,Genetic algorithm can't determine the SAT problem whether there exists solution.In genetic algorithm, the reason of the population being premature is the matured effect of the genetic operator. In a closed population, individuals can only communicate information with individuals within the population. This kind of information communication can make population information fully shared between individuals, but also brings the problem of assimilation, which is the main reason for the matured effect of genetic operator. Based on the research and exploration of SAT problem solver, such as zChaff and WalkSAT, Firstly, this paper first puts forward the crossover operator based on clause variable punishment strategy with the local search algorithm. By leading the gene exchange can not only keep population diversity, but also improve the efficiency of genetic algorithm. Secondly, based on the population of the independent island model and the simulation of biological evolution process of the concept of family genealogy tree,we divide the population into more family sociology meaning,and put forward a kind of improved genetic algorithm based on hierarchical tree. Its main idea is to split the population into smaller family,and each family has its own evolution operator. After each iteration, the family can be marriage between individual members through manner, so as to produce than the traditional crossover operator is more diverse,which has the potential to the offspring of the individual.In order to compare the proposed algorithm with local search algorithms, such as WalkSAT, some standard SAT problems from SATLIB are programmed. The practical computational results show that the proposed algorithm improves the efficiency and success rate, as well as the scale of the formula which the resolver can deal with. The highest speed ratio is 22, and the success rate is raised by up to 49 percent.