A Multilevel Tabu Search for the Maximum Satisfiability Problem

Noureddine Bouhmala, Sirar Salih

Department of Information and Communication Technology, University of Agder, Grimstad, Norway.
Department of Maritime Technology and Innovation, Vestfold University College, Horten, Norway.

DOI: 10.4236/ijcns.2012.510068                

Abstract

The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.

Keywords

Maximum Satisfiability Problem; Tabu Search; Multilevel Techniques

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	S. A. Cook, “The Complexity of Theorem-Proving Procedures,” Proceedings of the Third ACM Symposium on Theory of Computing, Shaker Heights, 3-5 May 1971, pp. 151-158.
[2]	R. J. Wallace and E. C. Freuder, “Comparative Study of Constraint Satisfaction and Davisputnam Algorithms for Maximum Satisfiability Problems,” In: D. Johnson and M. Trick, Eds., Cliques, Coloring, and Satisfiability, 1996, pp. 587-615.
[3]	M. Yagiura and T. Inaraki, “Analyses on the 2 and 3-Flip Neighborhoods for the MAXSAT,” Journal of Combinatorial Optimization, Vol. 3, No. 1, 1999, pp. 95-114. doi:10.1023/A:1009873324187
[4]	A. Strohmaier, “Multi-Flip Networks for SAT,” In: Proceedings of KI-98, Lecture Notes in Computer Science, Springer Verlag, Berlin, 1998.
[5]	N. Bouhmala, “A Multilevel Memetic Algorithm for Large SAT-Encoded Problems. Evolutionary Computation,” MIT Press, 2012, pp. 1-24.
[6]	B. Selman, H. A. Kautz and B. Cohen, “Noise Strategies for Improving Local Search. Proceedings of AAAI’94,” MIT Press, 1994, pp. 337-343.
[7]	I. Gent and T. Walsh, “Unsatisfied Variables in Local Search,” In: J. Hallam, Ed., Hybrid Problems, Hybrid Solutions, IOS Press, 1995, pp. 73-85.
[8]	P. Hansen and B. Jaumand, “Algorithms for the Maximum Satisfiability Problem,” Computing, Vol. 44, No. 4, 1990, pp. 279-303. doi:10.1007/BF02241270
[9]	W. Spears, “Adapting Crossover in Evolutionary Algorithms,” Proceedings of the Fourth Annual Conference on Evolutionary Programming, MIT Press, 1995, pp. 367-384.
[10]	A. E. Eiben and J. K. Van der Hauw, ”Solving 3-SAT with Adaptive Genetic Algorithms,” Proceedings of the 4th IEEE Conference on Evolutionary Computation, 1997, pp. 81-86.
[11]	D. S. Johnson and M. A. Trick, “Cliques, Coloring, and Satisfiability, Volume 26 of DIMACS Series on Discrete Mathematics and Theoretical Computer Science,” American Mathematical Society, 1996.
[12]	C. M. Li, W. Wei and H. Zhang, “Combining Adaptive Noise and Look-Ahead in Local Search for SAT,” Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing(SAT-07), volume 4501 of Lecture Notes in Computer Science, 2007, pp. 121-133.
[13]	D. J. Patterson and H. Kautz, “Auto-Walksat: A Self-Tuning Implementation of Walksat,” Electronic Notes on Discrete Mathematics, Vol. 9, 2001.
[14]	O. C. Granmo and N. Bouhmala, “Solving the Satisfiability Problem Using Finite Learning Automata,” International Journal of Computer Science and Applications, Vol. 4, No. 3, 2007, pp. 15-29.
[15]	A. R. KhudaBukhsh, L. Xu, H. H. Hoos and K. Leyton-Brown, “SATenstein: Automatically Building Local Search SAT Solvers from Components,” Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI-09), 2009.
[16]	L. Xu, F. Hutter, H. Hoos and K. Leyton-Brown, “SATzilla: Portfolio-Based Algorithm Selection for SAT,” Journal of Artificial Intelligence Research, Vol. 32, 2008, pp. 565-606.
[17]	F. Glover, “Tabu Search-Part 1. ORSA,” Journal on Computing, Vol. 1, No. 3, 1989, pp. 190-206. doi:10.1287/ijoc.1.3.190
[18]	S. T. Barnard and H. D. Simon, “A Fast Multilevel Implementation of Recursive Spectral Bisection for Partitioning Unstructured Problems,” Concurrency: Practice and Experience, Vol. 6, No. 2, 1994, pp. 101-117. doi:10.1002/cpe.4330060203
[19]	R. Hadany and D. Harel, “A Multi-Scale Algorithm for Drawing Graphs Nicely. Tech.Rep.CS99-01, Weizmann Inst.Sci., Faculty Maths.Comp.Sci, 1999.
[20]	B. Hendrickson and R. Leland, “A Multilevel Algorithm for Partitioning Graphs,” Proceedings of Supercomputing’95, San Diego, 1995.
[21]	G. Karypis and V. Kumar, “A Fast and High Quality Multilevel Scheme for Partitioning Irregular Graphs,” SIAM Journal on Scientific Computing, Vol. 20, No. 1, 1998, pp. 359-392. doi:10.1137/S1064827595287997
[22]	G. Karypis and V. Kumar, “Multilevel K-Way Partitioning Scheme for Irregular Graphs,” Journal of Parallel and Distributed Computing, Vol. 48, No. 1, 1998, pp. 96-129. doi:10.1006/jpdc.1997.1404
[23]	C. Walshaw and M. Cross, “Mesh Partitioning: A Multi-Level Balancing and Refinement Algorithm,” SIAM Journal on Scientific Computing, Vol. 22, No. 1, 2000, pp. 63-80. doi:10.1137/S1064827598337373
[24]	C. Walshaw, “A Multilevel Approach to the Traveling Salesman Problem,” Operations Research, Vol. 50, No. 5, 2002, pp. 862-877. doi:10.1287/opre.50.5.862.373
[25]	C. Walshaw, “A Multilevel Lin-Kernighan-Helsgaun Algorithm for the Travelling Salesman Problem,” Tech. Report 01/IM/80, Comp. Math. Sci., Univ. Greenwich, 2001.
[26]	D. Rodney, A. Soper and C. Walshaw, “The Application of Multilevel Refinement to the Vehicle Routing Problem,” In: D. Fogel, et al., Eds., IEEE Symposium on Computational Intelligence in Scheduling, 2007, pp. 212-219. doi:10.1109/SCIS.2007.367692
[27]	C. Walshaw, “A Multilevel Algorithm for Forced-Directed Graph-Drawing,” Journal of Graph Algorithms and Applications, Vol. 7, No. 3, 2003, pp. 253-285. doi:10.7155/jgaa.00070
[28]	C. Blum, J. Puchinger, G. R. Raidl and A. Roli, “Hybrid Metaheuristics in Combinatorial Optimization: A Survey,” Applied Soft Computing, Vol. 11, 2011, pp. 4135-4151. doi:10.1016/j.asoc.2011.02.032
[29]	C. Walshaw, “Multilevel Refinement for Combinatorial Optimization: Boosting Metaheuristic Performance,” In: C. Blum, et al., Ed., Springer, Berlin, 2008, pp. 261-289.
[30]	B. Mazure, L. Sas and E. Gregoire, “Tabu Search for SAT,” AAAI-97 Proceedings, 1997, pp. 281-285.