A Clausal Genetic Representation and its Evolutionary Procedures for Satisfiability Problems

  • Jin-Kao Hao


This paper presents a clausal genetic representation for the satisfiability problem (SAT). This representation, CR for short, aims to conserve the intrinsic relations between variables for a given SAT instance. Based on CR, a set of evolutionary algorithms (EAs) are defined. In particular, a class of hybrid EAs integrating local search into evolutionary operators are detailed. Various fitness functions for measuring clausal individuals are identified and their relative merits analyzed. Some preliminary results are reported.


Local Search Genetic Operator Local Search Procedure Evolutionary Procedure Satisfying Assignment 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Collective paper of Bahia project. “Comparative study of three formalisms in prepositional logic” (in French). 5ème Journées Nationales PRC-GDR en Intelligence Artificielle, Nancy, February 1995.Google Scholar
  2. [2]
    De Jong K.A. and Spears W.M. “Using genetic algorithms to solve NP-complete problems”. Intl. Conf. on Genetic Algorithms (ICGA’89), Fairfax, Virginia, June 1989, pp l24–132.Google Scholar
  3. [3]
    Dorne R. and Hao J.K. “New genetic operators based on a stratified population for SAT” (in French). Evolution Artificielle, Toulouse, France, September 1994.Google Scholar
  4. [4]
    Garey M.R. and Johnson D.S. “Computers and intractability: a guide to the theory of NP-completeness”. Freeman, San Francisco, CA, 1979.MATHGoogle Scholar
  5. [5]
    Glover F. and Laguna M. “Tabu search”. In [12].Google Scholar
  6. [6]
    Gu J. “Efficient local search for very large-scale satisfiability problems”. SIGART Bulletin, Vol. 3, No. 1, January 1992.Google Scholar
  7. [7]
    Hao J.K. and Dome R. “A new population-based method for satisfiability problems”. Proc. of 11th European Conf. on Artificial Intelligence (ECAI’94), Amsterdam, Aug. 94, pp 135–139.Google Scholar
  8. [8]
    Kirkpatric S., Gelatt C.D. and Vecchi M.P. “Optimization by simulated annealing”. Science, Vol. 220, May 1983, pp 671–680.MathSciNetCrossRefGoogle Scholar
  9. [9]
    Koutsoupias E. and Papadimitriou C.H. “On the greedy algorithm for satisfiability”. Information Processing Letters, Vol. 43 1992, pp 53–55.MathSciNetMATHCrossRefGoogle Scholar
  10. [10]
    Lawrence D. “Handbook of genetic algorithms”. Van Nostrand Reinhold, New York, 1991.Google Scholar
  11. [11]
    Mitchell M., Selman B. and Levesque H., “Hard and easy distributions of SAT problem”. Proc. of the AAAI’92, San Jose, CA, 1992, pp 459–465.Google Scholar
  12. [12]
    Reeves C.R. (Ed.) “Modern heuristic techniques for combinatorial problems”. Blackwell Scientifique Publications, Oxford, 1993.MATHGoogle Scholar
  13. [13]
    Selman B., Levesque H. and Mitchell M. “A new method for solving hard satisfiability problems”. Proc. of the AAAI’92, San Jose, CA, 1992, pp 440–446.Google Scholar
  14. [14]
    Selman B., Kautz H.A. and Bram C. “Noise strategies for improving local search”. Proc. of the AAAI’94, Seattle, WA, 1994.Google Scholar
  15. [15]
    Spears W.M. “Simulated annealing for hard satisfiability problems”. NCARAI Technical Report #AIC-93-015, Washington D.C. July 1993.Google Scholar
  16. [16]
    Young R.A. and Reel A. “A hybrid genetic algorithm for a logic problem”. Proc. of the 9th European Conf. on Artificial Intelligence, Stockholm, Sweden, Aug. 1990, pp 744–746.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Jin-Kao Hao
    • 1
  1. 1.LGI2P EMA-EERIENîmesFrance

Personalised recommendations