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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Belaid Benhamou and Lakhdar Sais. Theoretical study of symmetries in propositional calculus and applications. In CADE’92, pages 281–294, 1992.
May Beresin, Eugene Levine, and John Winn. A chessboard coloring problem. The College Mathematics Journal, 20(2):106–114, 1989.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, Jul 1962.
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.
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.
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.
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.
Charles Fleurent and Jacques A. Ferland. Genetic and hybrid algorithms for graph coloring. Annals of Operations Research, 63:437–461, 1997.
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.
Fred Glover and Manuel Laguna. Tabu Search. Kluwer Academic Publishers, 1998.
Jens Gottlieb, Elena Marchiori, and Claudio Rossi. Evolutionary algorithms for the satisfiability problem. Evolutionary Computation, 10(1):35–50, 2002.
Richard W. Hamming. Error detecting and error correcting codes. The Bell System Technical Journal, 29(2):147–160, April 1950.
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.
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.
Wengi Huang and Renchao Jin. Solar, a quasi physical algorithm for sat. Science in China (Series E), 2(27):179–186, 1997.
Henry Kautz and Bart Selman. Workshop on theory and applications of satisfiability testing (SAT2001). In Electronic Notes in Discrete Mathematics, volume 9, June 2001.
Chu Min Li. Integrating equivalency reasoning into davis-putnam procedure. In Proc. of the AAAI’00, pages 291–296, 2000.
Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proc. of the IJCAI’97, pages 366–371, 1997.
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.
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.
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.
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.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hao, JK., Lardeux, F., Saubion, F. (2003). Evolutionary Computing for the Satisfiability Problem. In: Cagnoni, S., et al. Applications of Evolutionary Computing. EvoWorkshops 2003. Lecture Notes in Computer Science, vol 2611. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36605-9_24
Download citation
DOI: https://doi.org/10.1007/3-540-36605-9_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00976-4
Online ISBN: 978-3-540-36605-8
eBook Packages: Springer Book Archive