Genetic optimisations for satisfiability and Ramsey theory

Andrew Barnes


The art of using evolutionary mechanisms for identifying satisfiability has produced a range of efficient solutions to this otherwise computationally challenging problem. Since their first use these evolutionary methods have been changed and adapted to produce increasingly efficient solutions. This paper introduces two unique alternatives to the optimisation of these methods, the first through the introduction of alternative mutation operators and the second through utilizing a grammatical encoding which has been proven to improve neuroevolution. The goal of this paper is to identify whether these two alternatives are candidates for future investigation in improving evolutionary satisfiability solvers.

Full Text:



S. Cook, “The Complexity of Theorem-Proving Procedures,” in In Proceedings of Third Annual ACM Symposium on Theory of Computing, New York, 1971.

S. Aaronson, “Complexity Zoo,” University of Waterloo, [Online]. Available: [Accessed 01 04 2017].

E. Boyarski, R. Stern and P. Surnek, “Boolean Satisfiability Approach to Optimal Multi-Agent Path Finding under the Sum of Costs Objective,” in In Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, 2016.

E. Weisstein, “Ramsey Number,” Wolfram, [Online]. Available: [Accessed 01 04 2017].

R. E. Greenwood, “Combinatorial Relations and Chromatic Graphs,” Canadian Journal of Mathematics, vol. 7, pp. 1-7, 1955.

A. E. Eiben and J. E. Smith, Introduction to Evolutionary Computing, Berlin: Springer-Verlag Berlin and Heidelberg, 2010.

C. Darwin, The Origin of Species, New York: D.Appleton and Company, 1923.

M. Mitchell, An Introduction to Genetic Algorithms, Cambridge, MA: The MIT Press, 1999.

I. Rechenberg, “Evolution Strategy: Nature's Way of Optimization,” Lecture Notes in Engineering, vol. 47, pp. 106-126, 1965.

J. H. Holland, Adaptation in natural and artificial systems, Cambridge, MA: The MIT Press, 1975.

S. Kwong, K. F. Man and K. S. Tang, Genetic Algorithms, London: Springer, 1999.

E. Marchiori, C. Rossi and J. N. Kok, “An adaptive evolutionary algorithm for the satisfiability problem,” in Proceedings of the 2000 ACM symposium on Applied computing, New York, 2000.

E. Marchiori and C. Rossi, “A Flipping Genetic Algorithm for Hard 3-SAT Problems,” in Proceeding GECCO'99 Proceedings of the 1st Annual Conference on Genetic and Evolutionary Computation, San Francisco, 1999.

M. Davis, G. Logemann and D. Loveland, “A Machine Program for Theorem Proving,” Communications of the ACM, pp. 394-397, 07 1962.

B. Selman, D. Mitchell and H. Levesque, “Generating Hard Satisfiability Problems,” Artificial Intelligence, vol. 81, no. 1, pp. 17-29, 1996.

H. Levesque, D. Mitchell and B. Selman, “A New Method for Solving Hard Satisfiability Problems,” in Proceedings of the Tenth National Conference on Artificial Intelligence, Menlo Park, 1992.

A. Biere, M. Heule, O. Kullman and S. Wieringa, “Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads,” in Proceedings of the 7th International Haifi

Verification Conference on Hardware and Software: Verification and Testing, Berlin, 2011.

M. Heule, O. Kullman and V. Marek, “Solving and Verifying the Boolean Pythagorean Triples Problem via Cub-and-Conquer,” in 19th International Conference on Theory and Applications of Satisfiability Testing, Bordeaux, 2016.

A. Eiben and J. Van Der Hauw, “Solving 3-SAT with adaptive genetic algorithms,” in Proceedings of the Fourth IEEE Conference on Evolutionary Computation, Piscataway, 1997.

J. Gottlieb and N. Voss, “Representations, Fitness Functions and Genetic Operators for the Satisfiability Problem,” in Proceedings of the third european conference on artificial evolution, London, 1997.

J. Gottlieb, E. Marchiori and C. Rossi, “Evolutionary Algorithms for the Satisfiability Problem,” Evolutionary Computing, vol. 1, no. 1, 2002.

K. A. De Jong and W. M. Spears, “Using Genetic Algorithms to solve NP-Complete Problems,” in Proceedings of the third international conference on Genetic Algorithms, San Francisoco, 1989.

E. W. Weisstein, “Conjunctive Normal Form,” Wolfram, [Online]. Available: [Accessed 20 04 2017].

D. Montana and L. Davis, “Training Feedforward Neural Networks Using Genetic Algorithms,” in Proceedings of the 11th International Join Conference on Artificial Intelligence, Detroit, 1989.

T. Back, A. Eiben and M. Vink, “A Superior Evolutionary Algorithm for 3-SAT,” in Proceedings of the 7th International Conference on Evolutionary Programming, London, 1998.

A. P. Barnes, “Evolutionary Party Problem Simulator,” GitHub, [Online]. Available: [Accessed 01 04 2017].

University of British Columbia, “SATLIB - Benchmark Problems,” [Online]. Available: [Accessed 2017 04 23].

H. Kitano, “Designing neural networks using genetic algorithm with graph generation system,” Complex Systems, vol. 4, pp. 461-476, 1990.


  • There are currently no refbacks.

Creative Commons License 
This work is licensed under a Creative Commons Attribution 3.0 License

ISSN 1754-2383 [Online] ©University of Plymouth