Email this article A Clonal Selection Algorithm Based Tabu Search for Satisfiability Problems
Abstract
We present in this paper a new memetic algorithm to deal with the Max Sat problem. The objective is to find the best assignment for a set of Boolean variables, which gives the maximum of verified clauses in a Boolean formula. Unfortunately, this problem has been shown to be NP-hard if the number of variables per clause is greater than 3. The proposed approach is based on clonal selection principles and local search method. In order to increase the performance of clonal selection to deal with Max Sat problem, an adaptive fitness function based on weighted clauses has been used. The underlying idea is to harness the optimization capabilities of clonal selection algorithm to achieve good quality solutions for Max SAT problem. A local search based on Tabu Search has been embodied in the clonal selection algorithm leading to an efficient hybrid framework which achieves better balance between exploration and exploitation capabilities of the search process. The obtained results are very encouraging and show the feasibility and effectiveness of the proposed hybrid approach.
Keywords
References
. S.A. Cook, “The Complexity of Theorem Proving Procedures”. In: Proc. 3rd Ann. ACM Symp. On Theory of Computing, Association for Computing Machinery, pp 151–158, 1971.
. A. Biere, A. Cimatti, E., Clarke, and Y. Zhu, “Symbolic model checking without BDDs”, In Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS, 1579: pp. 193–207,1999.
. N. Bouhmala, and O. Granmo, “Solving Graph Coloring Problems Using Learning Automata”. In Proceedings of the Eighth European Conference on Evolutionary Computation in Combinatoral Optimisation, LNCS 4972, pp. 277–288, 2008.
. H. Kautz, and B. Selman, “Pushing the envelope: planning, propositional logic and stochastic search,” Proceedings of the 13th National Conference on Artificial Intelligence (AAAI 96), AAAI Press, pp 1194 -1201, 1996.
. H. Kautz, and B. Selman, “The state of SAT,”.Discrete Applied Mathematics, 155 (12):1514–1524, 2007.
. B. Borchers and J. Furman, “Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems,” Journal of Combinatorial Optimization, Vol. 2, No. 4, pp. 299–306, 1999.
. M . Menai, M. Batouche, “A Backbone-Based Co-evolutionary Heuristic for Partial MAX-SAT,” Artificial Evolution. pp 155–166, 2005.
. H. Zhang, H. Shen, “Exact Algorithms for MAX-SAT,” Electronic Notes in Theoretical Computer Science, Vol. 86, No.1, 2003.
. M. Davis, G. Logemann, D. Loveland, “A machine program for theorem proving,” communication of the ACM, pp 394–397, 1962.
. CM. Li, F. Manyà, J. Planes , “Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers,” In: Proc. of the 11th Int. Conf. on Principles and Practice of Constraint Programming, CP’05, Sitges, Spain, pp. 403–414, 2005.
. J. Gottlieb, E. Marchiori, and C. Rossi, “Evolutionary algorithms for the satisfiability problem,” Evolutionary Computation, Vol.10,No. 2, pp. 35–50,2002
. A. Layeb, D. Saidouni, “A New Quantum Evolutionary Local Search Algorithm for MAX 3-SAT Problem,” In Proc., of the 3rd international Workshop on Hybrid Artificial intelligence Systems. LNAI, Vol. 5271, pp. 172–179, 2008.
. E.S. Skvortsov, “A Theoretical Analysis of Search in GSAT,” Proceedings of the SAT, pp. 265–275, 2009.
. M. Mastrolilli and L. M. Gambardella, “Maximum satisfiability: how good are tabu search and plateau moves in the worst-case?,” European Journal of Operational Research, Vol. 166,No. 1, pp. 63–76, 2005.
. F. Lardeux, F. Saubion, J.K. Hao, “GASAT: A genetic local search algorithm for the satisfiability problem,” Evolutionary Computation, Vol. 14, No. 2, pp. 223–253, 2006.
. Y. Kilani, “Comparing the performance of the genetic and local search algorithms for solving the satisfiability problems,” Applied Soft Computing, Vol. 10, No. 1, pp. 198¬¬¬–207, 2010.
. A. Bhalla, I. Lynce, J. T. de Sousa and J. Marques-Silva, “Heuristic based backtracking for Propositional Satisfiability,” In Proceedings 11th Portuguese Conference on Artificial Intelligence (EPIA’03), Lecture Notes in Artificial Intelligence, vol. 2902, pp. 116–130, 2003.
. L. Kroc , A. Sabharwal , C. P. Gomes and B. Selman, “Integrating systematic and local search paradigms: A new strategy for MaxSAT,” IJCAI, pp 544–551, 2009.
. A. Layeb, A.H. Deneche, M. Meshoul, “A New Artificial Immune System for Solving the Maximum Satisfiability Problem,” In: N. García-Pedrajas et al. (Eds.): IEA/AIE 2010, part II, LNAI, Vol. 6097, pp. 136–142, 2010.
. D. Dasgupta, F. Nino, “Immunological Computation: Theory and Applications,” Auerbach Publications, USA, 2008.
. L.N. De Castro and J. Timmis, “Artificial Immune Systems: A New Computational Intelligence Approach,” Springer, UK, 2002.
. I. Aydin , M. Karakose, E. Akin, “ Artificial immune classifier with swarm learning,” Engineering Applications of Artificial Intelligence, Vol.23, No. 8, pp. 1291–1302 2010.
. L.N.D. Castro and F.J.V. Zuben, “Learning and optimization using the clonal selection principle,” IEEE Trans. on Evolutionary Computation, Vol. 6, No. 3, pp. 239–251, 2002.
. V. Cutello, G. Nicosia , “The Clonal Selection Principle for in silico and in vitro Computing, in Recent Developments in Biologically Inspired Computing,” In de Castro LN, Von Zuben FJ (Eds), 2004.
. F. Glover, “Tabu Search for Nonlinear and Parametric Optimization (with links to genetic algorithms),” Discrete Applied Mathematics, Vol. 49, pp. 231-255, 1994.
. B. Mazure, L. Sais, E. Greroire, “Tabu search for SAT,” In: Proceeding of the AAAI-97/IAAI-97, pp 281–285, 1997.
. M. Davis, H. Putnam, “A computing procedure for quantification theory,” Journal of the ACM, Vol. 7, No. 3, pp. 201–215, 1960.
. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” In Proceedings of 12th International Conference on Computer Aided Verification, LNCS, Vol. 1855, 2001.
. L. Xu, F. Hutter, H.H. Hoos, and K. Leyton-Brown, “SATzilla: portfolio-based algorithm Selection for SAT,” Journal of Artificial Intelligence Research, Vol. 32, pp. 565–606, 2008.
. B. Selman, H. Kautz, B. Cohen, “Local Search Strategies for Satisfiability Testing,”. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26, pp. 521–532, 1993.
. D.A.D. Tompkins, H.H. Hoos, “UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT,” In: Hoos HH and Mitchell DG (Eds.) SAT 2004, LNCS, Vol. 3542, pp. 306–320, 2005.
. S. Rana, D. Whitley, R.B. Heckendorn, “A Tractable Walsh Analysis of SAT and its Implications for Genetic Algorithms,” In proceedings of the 15th National Conference on Artificial Intelligence, pp 392–397, 1998.
. A. Layeb, A.H. Deneche, “Multiple Sequence Alignment by Immune Artificial System,” IEEE/ACS International Conference on Computer Systems and Applications, pp. 336–342, 2007.
. J. Gottlieb, N. Voss, “Adaptive fitness functions for the satisfiability problem,” In: Parallel Problem Solving from Nature - PPSN VI 6th International Conference, LNCS, Vol. 1917, 2000.
. Y. Asahiro, K. Iwama, E. Miyano, “ Random Generation of Test Instanzes with Controlled Attributes,” DIMACS Series on Discr. Math. and Theor. Comp. Sci, Vol. 26, pp. 377–394, 1996.
. D. McAllester, B. Selman, H. Kautz, “Evidence for invariants in local search,” In: Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pp. 321-326, 1997.
. K. Smyth, H.H. Hoos, T. Stützle, “Iterated Robust Tabu Search for MAX-SAT,” In: Canadian Conference on AI, LNCS, Vol. 2671, pp.129-144, 2003.
Full Text: PDF