Advertisement

Evolutionary Computing for the Satisfiability Problem

  • Jin-Kao Hao
  • Frédéric Lardeux
  • Frédéric Saubion
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2611)

Abstract

This paper presents GASAT, a hybrid evolutionary algorithm for the satisfiability problem (SAT). A specific crossover operator generates new solutions, that are improved by a tabu search procedure. The performance of GASAT is assessed using a set of well-known benchmarks. Comparisons with state-of-the-art SAT algorithms show that GASAT gives very competitive results. These experiments also allow us to introduce a new SAT benchmark from a coloring problem.

Keywords

Local Search Tabu Search Conjunctive Normal Form Tabu List Evolutionary Computing 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Belaid Benhamou and Lakhdar Sais. Theoretical study of symmetries in propositional calculus and applications. In CADE’92, pages 281–294, 1992.Google Scholar
  2. 2.
    May Beresin, Eugene Levine, and John Winn. A chessboard coloring problem. The College Mathematics Journal, 20(2):106–114, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, Jul 1962.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Kenneth A. De Jong and William M. Spears. Using genetic algorithm to solve NP-complete problems. In Proc. of the Third Int. Conf. on Genetic Algorithms, pages 124–132, San Mateo, CA, 1989.Google Scholar
  5. 5.
    Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier. SAT versus UNSAT. In Second DIMACS implementation challenge: cliques, coloring and satis fiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 415–436, 1996.Google Scholar
  6. 6.
    Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Bernhard Nebel, editor, Proc. of the IJCAI’01, pages 248–253, San Francisco, CA, 2001.Google Scholar
  7. 7.
    Agoston E. Eiben, Jan K. van der Hauw, and Jano I. van Hemert. Graph coloring with adaptive evolutionary algorithms. Journal of Heuristics, 4(1):25–46, 1998.zbMATHCrossRefGoogle Scholar
  8. 8.
    Charles Fleurent and Jacques A. Ferland. Genetic and hybrid algorithms for graph coloring. Annals of Operations Research, 63:437–461, 1997.CrossRefGoogle Scholar
  9. 9.
    Michael R. Garey and David S. Johnson. Computers and Intractability, A Guide to the Theory of NP-Completeness. W.H. Freeman & Company, San Francisco, 1978.Google Scholar
  10. 10.
    Fred Glover and Manuel Laguna. Tabu Search. Kluwer Academic Publishers, 1998.Google Scholar
  11. 11.
    Jens Gottlieb, Elena Marchiori, and Claudio Rossi. Evolutionary algorithms for the satisfiability problem. Evolutionary Computation, 10(1):35–50, 2002.CrossRefGoogle Scholar
  12. 12.
    Richard W. Hamming. Error detecting and error correcting codes. The Bell System Technical Journal, 29(2):147–160, April 1950.MathSciNetGoogle Scholar
  13. 13.
    Jin-Kao Hao and Raphael Dorne. A new population-based method for satisfiability problems. In Proc. of the 11th European Conf. on Artificial Intelligence, pages 135–139, Amsterdam, 1994.Google Scholar
  14. 14.
    Edward A. Hirsch and Arist Kojevnikov. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. PDMI preprint 9/2001, Steklov Institute of Mathematics at St.Petersburg, 2001.Google Scholar
  15. 15.
    Wengi Huang and Renchao Jin. Solar, a quasi physical algorithm for sat. Science in China (Series E), 2(27):179–186, 1997.Google Scholar
  16. 16.
    Henry Kautz and Bart Selman. Workshop on theory and applications of satisfiability testing (SAT2001). In Electronic Notes in Discrete Mathematics, volume 9, June 2001.Google Scholar
  17. 17.
    Chu Min Li. Integrating equivalency reasoning into davis-putnam procedure. In Proc. of the AAAI’00, pages 291–296, 2000.Google Scholar
  18. 18.
    Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proc. of the IJCAI’97, pages 366–371, 1997.Google Scholar
  19. 19.
    Chu Min Li, Bernard Jurkowiak, and Paul W. Purdom. Integrating symmetry breaking into a dll procedure. In Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT2002), pages 149–155, 2002.Google Scholar
  20. 20.
    Bertrand Mazure, Lakhdar Saís, and Éric Grégoire. Tabu search for SAT. In Proc. of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI-97/IAAI-97), pages 281–285, Providence, Rhode Island, 1997.Google Scholar
  21. 21.
    Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha.: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC’01), Jun 2001.Google Scholar
  22. 22.
    Bart Selman, Henry A. Kautz, and Bram Cohen. Noise strategies for improving local search. In Proc. of the AAAI, Vol. 1, pages 337–343, 1994.Google Scholar
  23. 23.
    Bart Selman, Hector J. Levesque, and David G. Mitchell. A new method for solving hard satisfiability problems. In Proc. of the AAAI’92, pages 440–446, San Jose, CA, 1992.Google Scholar
  24. 24.
    Laurent Simon, Daniel Le Berre, and Edward A. Hirsch. The sat2002 competition. Technical report, Fifth International Symposium on the Theory and Applications of Satisfiability Testing, May 2002.Google Scholar
  25. 25.
    William M. Spears. Simulated annealing for hard satisfiability problems. In Second DIMACS implementation challenge: cliques, coloring and satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 533–558, 1996.Google Scholar
  26. 26.
    Hantao Zhang. SATO: An efficient propositional prover. In Proc. of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 272–275, Berlin, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Jin-Kao Hao
    • 1
  • Frédéric Lardeux
    • 1
  • Frédéric Saubion
    • 1
  1. 1.LERIAUniversité d'AngersAngers Cedex 01

Personalised recommendations