Solving Satisfiability Problem With Improved Ant Colony Optimization

Boolean satisfiability problem (SAT) is to determine whether a Conjunctional NormalForm (CNF) is satisfiable. It is a basic problem in logistics while it is the first provedNP-complete problem.SAT is also the core problem of computer science; it has a wide rangeof practical applications in different fields, such as formal verification of circuits, automatedreasoning, artificial intelligence, resource scheduling, etc.SAT draws the attention of many researchers due to its theoretical and practical value. Alot of efficient algorithms have been proposed, which fall into two categories: completealgorithms and incomplete algorithms. Incomplete algorithms include local search methods,intelligent algorithms, statistical-physical methods, etc. Survey Propagation (SP) is anefficient statistical method proposed in recent years. SP first calculates the probabilitydistribution for each variable, and then fixes a part of the variables according to thedistribution. It then simplify the problem and repeat the previous iteration on the sub problemuntil the sub problem becomes easy or it enters into an non-convergence state.SP can solveproblems with millions of variables, its excellent performance draws the attention of manyscholars.Ant Colony Optimization(ACO) is one of the intelligent algorithms.ACO solve problemsin a way like natural ants forage for food.Ants have no vision, but ants can find the right pathby releasing pheromone on the road. For a given period, there will be more ants passing theshorter paths than the longer paths, thus more pheromone will be accumulated on shorterpaths. Paths with more pheromone will be chose with higher probability. The pheromonemakes the whole ant colony behave in coordination. Ants exchange path information underthe effect of pheromone and finally find the shortest path leads to food. ACO has been appliedin all kinds of practical problems, including Traveling Salesman Problem (TSP), SAT, etc.It is found in numerical experiments that SP tends not to converge for hard SATproblems which is possibly caused by early mistakes that SP assigns wrong values to severalvariables which results in an unsatisfiable sub problem. In this paper, the probabilitydistribution in SP was processed and used as heuristic information in ACO in hopes that it canguide the search, thus overcome the defect that ACO converges slowly in early period causedby lack of pheromone. All the pheromones were limited in a range to prevent the pheromonefrom rapidly increasing which can easily cause stagnation. Besides, local search was added tofurther improve the local convergence and make the search process more efficient.In this paper, the improved ACO was programmed in C and evaluated by4groups of hard instances. The experimental results validate the efficiency of the improved ACO, whichcan solve more hard problems than SP, and more quickly in most cases.