Abstrakt
A classical conjecture of Erdős and Szekeres states that every set of 2^(k MINUS SIGN 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 MINUS SIGN 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.