The International Arab Journal of Information Technology (IAJIT)

..............................
..............................
..............................


Solving the Maximum Satisfiability Problem Using an Evolutionary Local Search Algorithm

,

The MAXimum propositional SATisfiability problem (MAXSAT) is a well known NP-hard optimization problem with many theoretical and practical applications in artificial intelligence and mathematical logic. Heuristic local search algorithms are widely recognized as the most effective approaches used to solve them. However, their performance depends both on their complexity and their tuning parameters which are controlled experimentally and remain a difficult task. Extremal Optimization (EO) is one of the simplest heuristic methods with only one free parameter, which has proved competitive with the more elaborate general-purpose method on graph partitioning and coloring. It is inspired by the dynamics of physical systems with emergent complexity and their ability to self-organize to reach an optimal adaptation state. In this paper, we propose an extremal optimization procedure for MAXSAT and consider its effectiveness by computational experiments on a benchmark of random instances. Comparative tests showed that this procedure improves significantly previous results obtained on the same benchmark with other modern local search methods like WSAT, simulated annealing and Tabu Search (TS).

 


[1] Bak P. and Sneppen K., “Punctuated Equilibrium and Criticality in a Simple Model of Evolution,” Physical Review Letters, vol. 71, pp. 4083-4086, 1993.

[2] Bak P., Tang C., and Wiesenfeld K., “Self- Organized Criticality: An Explanation of 1/f- Noise,” Physical Review Letters, vol. 86 no. 23, pp. 5211-5214, 1987.

[3] Battiti R. and Protasi M., “Reactive Search: A History-Sensitive Heuristic for MAX-SAT,” ACM Journal of Experimental Algorithmics, vol. 2, 1997.

[4] Boettcher S. and Grigni M., “Jamming Model for the Extremal Optimization Heuristic,” Journal of Physics A: Mathematical and General , vol. 35, pp. 1109-1123, 2002.

[5] Boettcher S. and Percus A. G., “Nature’s Way of Optimizing,” Elsevier Science, Artificial Intelligence , vol. 119, pp. 275-286, 2000.

[6] Boettcher S. and Percus A. G., “Optimization with Extremal Dynamics,” Physical Review Letters , vol. 86, no. 23, pp. 5211-5214, 2001.

[7] Boettcher S. and Percus A. G., “Extremal Optimization for Graph Partitioning,” Physical Review E , vol. 64, pp. 1-13, 2001.

[8] Cook S. A., “The Complexity of Theorem Proving Procedures,” in Proceedings of the 3rd Annual ACM Symposium of the Theory of Computation , pp. 151-158, 1971.

[9] Crescenzi P. and Kann V., “How to Find the Best Approximation Results: A Follow-up to Garey and Johnson,” ACM SIGACT News, vol. 29 no. 4, pp. 90-97, 1998.

[10] Davis M. and Putnam M., “A Computing Procedure for Quantification Theory,” Journal of the ACM, vol. 7. pp. 201-215, 1960.

[11] Dubois O. and Dequen G., “A Backbone-Search Heuristic for Efficient Solving of Hard 3-SAT Formulae,” in Proceedings of the IJCAI’01, pp. 248-253, San Francisco, CA, 2001.

[12] Gent I. and Walsh T., “Unsatisfied Variables in Local Search,” in Hybrid Problems, Hybrid Solutions, Hallam J. (Eds), IOS Press, Amsterdam, pp. 73-85, 1995.

[13] Glover F., “Tabu Search: Part I,” ORSA Journal on Computing , vol. 1, no. 3, pp. 190-206, 1989.

[14] Glover F., “Tabu Search: Part II,” ORSA Journal on Computing , vol. 2, no. 1, pp. +32, 1989.

[15] Hirsch E. A. and Kojevnikov A., “UnitWalk: A New SAT Solver That Uses Local Search Guided by Unit Clause Elimination,” in Proceedings of the 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002) , Cincinnatti, Ohio, USA, pp. 35-42, 2002.

[16] Jiang Y., Kautz H. A., and Selman B., “Solving Problems With Hard and Soft Constraints Using a Stochastic Algorithm for MAX-SAT,” in Proceedings of the 1st International Joint Workshop on Artificial Intelligence and Operations Research , 1995.

[17] Johnson D., “Approximation Algorithms for Combinatorial Problems,” Journal of Computer and System Sciences , vol. 9, pp. 256-278, 1974.

[18] Kautz H. A. and Selman B., “Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search,” in Proceedings of the AAAI’96 , vol. 2, pp. 1194-1201, MIT Press, 1996.

[19] Kirkpatrick S., Gelatt C. D., and Vecchi P. M., “Optimization by Simulated Annealing,” Science, vol. 220, no. 4598, pp. 671-680, 1983.

[20] Li C.M., “Integrating Equivalence Reasoning into Davis-Putnam Procedure,” in Proceedings of the AAAI’00 , pp. 291-296, 2000.

[21] Mazure B., Sais L., and Gregoire E., “Tabu Search for SAT,” in Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference , pp. 281-285, 1997.

[22] Mc Allester D., Selman B., and Kautz H., “Evidence for Invariants in Local Search,” in Proceedings of the IJCAI-97 , 1997.

[23] Menaï M. B. and Batouche M., “EO for MAXSAT,” in Proceedings of the International Conference on Artificial Intelligence (IC-AI’02) , Las Vegas, USA, vol. 3, pp. 954-958, 2002.

[24] Metropolis N., Rosenbluth A. W., Rosenbluth M. N., Teller A. H., and Teller E., “Equation of State Calculations by Fast Computing Machines,” Journal of Chemical Physics, vol. 21, pp 1087- 1092, 1953.

[25] Mitchell D., Selman B., and Levesque H. J., “Hard and Easy Distributions of SAT Problems,” in Proceedings of the Tenth National Conference on Artificial Intelligence , AAAI, San Jose, CA, pp. 459-465, 1992.

[26] Resende M. G. C., Pitsoulis L. S., and Pardalos P. M., “Approximate Solution of Weighted MAX-SAT Problems Using GRASP,” DIMACS Series on Discrete Mathematics and Theoretical Solving the Maximum Satisfiability Problem Using an Evolutionary Local Search Algorithm 161 Computer Science,American Mathematical Society, vol. 35, pp. 393-405, 1997.

[27] Selman B. and Kautz H. A., “An Empirical Study of Greedy Local Search for Satisfiability Testing,” in Proceedings of the 11th National Conference on Artificial Intelligence , pp. 46-51, 1993.

[28] Selman B. and Kautz H. A., “Domain Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems,” in Proceedings of the IJCAI-93 , pp. 290-295, 1993.

[29] Selman B., Kautz H. A., and Cohen B., “Noise Strategies for Improving Local Search,” in Proceedings of the 12th National Conference on Artificial Intelligence , pp. 337-343, 1994.

[30] Selman B., Levesque H., and Mitchell D., “A New Method for Solving Hard Satisfiability Problems,” in Proceedings of the 10th National Conference on Artificial Intelligence , pp. 440- 446, 1992.

[31] Shang Y. and Wah B. W., “A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems,” Journal of Global Optimization , vol. 12, pp. 61-99, 1998.

[32] Spears W. M., “Simulated Annealing for Hard Satisfiability Problems,” in Johnson D. S. and Trick M. A. (Eds), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, vol. 26, pp. 553-558, 1996.

[33] Vieira M. S., “Are Avalanches in Sandpiles a Chaotic Phenomenon?,” Research Report, 2004.

[34] Yannakakis M., “On the Approximation of Maximum Satisfiability,” Journal of Algorithms, vol. 17, pp. 475-502, 1994. Mohamed El Bachir Menai is currently a researcher at the AI Laboratory of the University of Paris 8, France. From 1988 to 2003, he was a researcher and an assistant professor at the Computer Science Department of the University of Tebessa. He received his BSc in computing systems from the University of Annaba in 1994. His main interests are in the areas of problem complexity, heuristic search, evolutionary computation, and quantum computing. Mohamed Batouche received his MSc and PhD degrees in computer science from the Institut National Polytechnique de Lorraine (INPL), France, in 1989 and 1993, respectively. Currently, he is a full- time professor at the University Mentouri of Constantine, Algeria. His research areas include artificial intelligence and pattern recognition.