Bulletin 99, April 97 

 
Improved local search algorithms for the 3-SAT problem
 
Michael Gerber, Département de Mathématiques, EPF, Lausanne
 
The problem of satisfiability (SAT) is to decide if there exists an assignment for the Boolean variables in a propositional formula that makes the formula true. A list of clauses formed by literals must be satisfied. A literal is a Boolean variable or its negation, and a clause is satisfied if at least one of the literals is true.
 
Cook proved in 1971 that SAT is NP-complete. In fact, this problem is the first for which NP-completeness has been shown. SAT is also of a practical interest, since it can be applied to artificial intelligence and problems of mathematical logic.
 
Two different approaches for solving NP-complete problems are possible : Selman, Levesque and Mitchell showed in 1992 that there is a phase transition with SAT as the ratio alpha of the number of clauses to literals in a problem is varied. The transition is marked by a critical threshold value alpha(c). Below this value the problems are under-constrained and therefore one can easily exhibit a feasible solution. Above this value they become over-constrained which makes it easy to prove that there is no satisfying assignment of the variables. The transition appears at the point where the probability to have a solution abruptly falls from 1 to 0. The most difficult problems to solve are those in the region around the critical value. Selman, Levesque and Mitchell quantified the critical value as alpha(c) = 4.3 for the 3-SAT problem.
 
The best performing heuristics for the 3-SAT problem are the local search algorithms. A solution is evaluated by means of the number of unsatisfied clauses. Two solutions are called neighbors, if one can be obtained from the other by inverting the value of one Boolean variable. The algorithms examined in this project are based on two steps. First the algorithms execute a descent method by going from one solution to a neighbor which satisfies more clauses, until it is no longer possible. At the end of this step, either a feasible solution is found or else the method is stuck in a local minimum. The second step consists of breaking out of such a local minimum. Currently, the best local search method is GSAT, which was proposed by Selman, Levesque and Mitchell in 1992.
 
The originality of this project is the topological description of the 3-SAT problem which can be used to find more efficient ways to break out of a local minimum. A new vocabulary is introduced. The altitude is the number of unsatisfied clauses, and a plateau consists of a local minimum and all the solutions of the same altitude that are neighbors. Hence a plateau is a set of solutions of the same altitude which are either local minima or are solutions that have a descent direction. The latter are called the exits of the plateau.
 
It is instructive to analyze the problem by considering the size of the plateaus, their number of exits, their altitude and their attraction. These characteristics are very different depending on whether the problem is in the critical region or not.
 
The nature of the plateaus varies considerably in function of their altitude. Typically the size and the number of exits of a plateau decrease when the altitude decreases. Hence breaking out of a local minimum at high altitude is easy. For example, by inspecting only a couple of neighbors one might already find a descent direction. On the other hand, at low altitude the exits become increasingly rare.
 
Finally, we propose and discuss a new method, the multiple satisfaction method. Like the other heuristics, it considers the number of satisfied clauses. But solutions with the same number of satisfied clauses are now ranked according to a secondary criterion, i.e. by the number of clauses that are satisfied twice or (in the case of a further tie) three times.
 
I am extremely grateful to Professor Pierre Hansen (GERAD, École des HEC de Montréal) for supporting me in this project.
 
 
References
 
Cook, S., Davis, M. and H. Putnam, Selman, B., H. Levesque and D. Mitchell, Selman, B., H. Levesque and D. Mitchell,  
 
RETURN to previous page.