Abstract
In this paper, we present several recombination operators that are specially designed for SAT problems. These operators take into account the semantic information induced by the structure of the given problem instance under consideration. Studies are carried out to assess the relative performance of these recombination operators on the one hand, and to show the high effectiveness of one of them when it is embedded into a hybrid genetic local search algorithm on the other hand.
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
Benhamou, B., Sais, L.: Theoretical study of symmetries in propositional calculus and applications. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 281–294. Springer, Heidelberg (1992)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962)
De Jong, K.A., Spears, W.M.: Using genetic algorithm to solve NP-complete problems. In: Proc. of the Third Int. Conf. on Genetic Aalgorithms, San Mateo, CA, pp. 124–132 (1989)
Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: Nebel, B. (ed.) Proc. of the IJCAI 2001, San Francisco, CA, pp. 248–253 (2001)
Fleurent, C., Ferland, J.A.: Object-oriented implementation of heuristic search methods for graph coloring, maximum clique, and satisfiability. In: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 619–652 (1994)
Garey, M.R., Johnson, D.S.: Computers and Intractability, A Guide to the Theory of NP-Completeness. W.H. Freeman & Company, San Francisco (1978)
Gottlieb, J., Marchiori, E., Rossi, C.: Evolutionary algorithms for the satisfiability problem. Evolutionary Computation 10(1), 35–50 (2002)
Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Computing 44(4), 279–303 (1990)
Hao, J.-K., Lardeux, F., Saubion, F.: Evolutionary computing for the satisfiability problem. In: Raidl, G.R., Cagnoni, S., Cardalda, J.J.R., Corne, D.W., Gottlieb, J., Guillot, A., Hart, E., Johnson, C.G., Marchiori, E., Meyer, J.-A., Middendorf, M. (eds.) EvoIASP 2003, EvoWorkshops 2003, EvoSTIM 2003, EvoROB/EvoRobot 2003, EvoCOP 2003, EvoBIO 2003, and EvoMUSART 2003. LNCS, vol. 2611, pp. 259–268. Springer, Heidelberg (2003)
Hirsch, E.A., Kojevnikov, A.: 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)
Jaumard, B., Stan, M., Desrosiers, J.: Tabu search and a quadratic relaxation for the satisfiability problem. In: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 457–478 (1994)
Li, C.M.: Integrating equivalency reasoning into davis-putnam procedure. In: Proc. of the AAAI 2000, pp. 291–296 (2000)
Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proc. of the IJCAI 1997, pp. 366–371 (1997)
Marchiori, E., Rossi, C.: A flipping genetic algorithm for hard 3-SAT problems. In: Proceedings of the Genetic and Evolutionary Computation Conference, vol. 1, pp. 393–400 (1999)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. of the AAAI, vol. 1, pp. 337–343 (1994)
Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proc. of the AAAI 1992, San Jose, CA, pp. 440–446 (1992)
Simon, L., Le Berre, D., Hirsch, E.A.: The SAT 2002 competition. Technical report, Fifth International Symposium on the Theory and Applications of Satisfiability Testing (May 2002)
Yagiura, M., Ibarak, T.: Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: Experimental evaluation. Journal of Heuristics 7(5), 423–442 (2001)
Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 272–275. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lardeux, F., Saubion, F., Hao, JK. (2004). Recombination Operators for Satisfiability Problems. In: Liardet, P., Collet, P., Fonlupt, C., Lutton, E., Schoenauer, M. (eds) Artificial Evolution. EA 2003. Lecture Notes in Computer Science, vol 2936. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24621-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-24621-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21523-3
Online ISBN: 978-3-540-24621-3
eBook Packages: Springer Book Archive