A SAT attack on the Erdős–Szekeres conjecture

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