A SAT attack on the Erdős–Szekeres Conjecture

---

Homepage

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]

Abstract:

A classical conjecture of Erdős and Szekeres states that every set of 2^k-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 2^k-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 K³_N 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.

Usage:

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'.

Results:

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

• Coloring of K³₁₇ with no red 4-path and with no 7-gon [TXT, 2 kB]
• Coloring of K³₂₆ with no red 5-path, no blue 6-path, and with no 7-gon [TXT, 8 kB]
• Coloring of K³₂₇ with no red 5-path and with no 7-gon [TXT, 9 kB]
• Coloring of K³₃₁ with no red 6-path, no blue 6-path, and with no 7-gon [TXT, 14 kB]
• Coloring of K³₃₂ with no red 6-path and with no 7-gon [TXT, 15 kB]
• Coloring of K³₃₃ with with no 7-gon [TXT, 33 kB]
• Coloring of K³₂₃ with no red 4-path and with no 8-gon [TXT, 6 kB]
• Coloring of K³₃₀ 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