A Multilevel Greedy Algorithm for the Satisfiability Problem
Noureddine Bouhmala, Xing Hui Cai · InTech eBooks · 2008
In this chapter, we have described and tested a new approach to solving the SAT problem based on combining the multilevel paradigm with the GSAT greedy algorithm. The resulting MLVGSAT algorithm progressively coarsens the problem, provides an initial assignment at the coarsest level, and then iteratively refines it backward level by level. In order to get a comprehensive picture of the new algorithm’s performance, we used a benchmark set consisting of SAT-encoded problems from various domains. Based on the analysis of the results, we observed that within the same computational time, MLVGSAT provides higher quality solution compared with that of GSAT. Other conclusions that we may draw from the results are that the multilevel paradigm can either speed up GSAT or even improve its asymptotic convergence. Results indicated that the larger the instance, the higher the difference between the mean percentage excess deviation from the solution. An obvious subject for further work would be the use of efficient data structures in order to minimize the overhead during the coarsening and refinement phases. It would be of great interest to further validate or contradict the conclusions of this work by extending the range of problem classes. Finally, obvious subjects for further work include designing different coarsening strategies and tuning the refinement process.