A SAT attack on the Erdős–Szekeres Conjecture


Here we store the experimental results described in

  • M. Balko and P. Valtr. A SAT attack on the Erdős–Szekeres Conjecture, Extended abstract in Electronic Notes in Discrete Mathematics 49, pages 425-431, 2015. [DOI]

A classical conjecture of Erdős and Szekeres states that every set of 2k-2+1 points in the plane in general position contains k points in convex position. In 2006, Peters and Szekeres introduced the following stronger conjecture: every red-blue coloring of the edges of the ordered complete 3-uniform hypergraph on 2k-2+1 vertices contains an ordered k-vertex hypergraph consisting of a red and a blue monotone path which are vertex disjoint except for the common end-vertices.

Applying the state of art SAT solver, we refute the conjecture of Peters and Szekeres. We also apply techniques of Erdős, Tuza, and Valtr to refine the Erdős–Szekeres conjecture in order to tackle it with SAT solvers.

In our experiments we used the Glucose SAT solver.

Further details can be found in the paper.

C++ generator:

All SAT instances are automatically generated by a simple C++ program 'generator.cpp'. For given positive integers a, u, k, and N, the generator produces a SAT formula that is satisfiable if and only if there is a coloring of K3N with no red a-path, no blue u-path, and with no k-gon. The output formula is saved in the DIMACS format and it can be used as an input for Glucose.


To use the program 'generator.cpp' under a Linux system do the following.

  • Save the program 'generator.cpp' on your computer.
  • Change the following parameters defined in the beginning of the file:
    • a = the length of the forbidden red monotone path,
    • u = the length of the forbidden blue monotone path,
    • k = the size of a forbidden gon,
    • N = the size of the complete 3-uniform hypergraph whose edges are colored red and blue.
  • Compile the program with the command 'g++ generator.cpp -o generator'.
  • Run the program with the command './generator > output.cnf'.
    • We note that the output can be very large even for rather small values of a, u, k, and N.
  • Run your favorite SAT solver on 'output.cnf'.

Every coloring of K3N is stored as a {0,1}-vector whose length is the number of edges of K3N. The ith coordinate of this vector represents the color of the ith edge of K3N in the lexicographic ordering of the edges. The red color is represented by 1, the blue color by 0.

  • Coloring of K317 with no red 4-path and with no 7-gon [TXT, 2 kB]
  • Coloring of K326 with no red 5-path, no blue 6-path, and with no 7-gon [TXT, 8 kB]
  • Coloring of K327 with no red 5-path and with no 7-gon [TXT, 9 kB]
  • Coloring of K331 with no red 6-path, no blue 6-path, and with no 7-gon [TXT, 14 kB]
  • Coloring of K332 with no red 6-path and with no 7-gon [TXT, 15 kB]
  • Coloring of K333 with with no 7-gon [TXT, 33 kB]
  • Coloring of K323 with no red 4-path and with no 8-gon [TXT, 6 kB]
  • Coloring of K330 with no red 4-path and with no 9-gon [TXT, 12 kB]

A compressed directory with all colorings: [ZIP, 5 kB]

Last update: 28.11.2016

Valid XHTML 1.0 Transitional