Notes on the 33-point Erd\H{o}s--Szekeres problem

TL;DR

This paper introduces a SAT-based computational approach to the 33-point Erd ext{"o}s--Szekeres problem, providing certificates for certain configurations and highlighting computational challenges like heavy-tailed runtime variability.

Contribution

It develops a novel SAT encoding for the 33-point case of the Erd ext{"o}s--Szekeres problem, including new constraints and analysis of computational complexity.

Findings

Generated UNSAT certificates for anchored subfamilies.

Observed heavy-tailed runtime variability in computations.

Provided insights into the computational difficulty of the 33-point case.

Abstract

The determination of $ES(7)$ is the first open case of the planar Erd\H{o}s--Szekeres problem, where the general conjecture predicts $ES(7)=33$. We present a SAT encoding for the 33-point case based on triple-orientation variables and a 4-set convexity criterion for excluding convex 7-gons, together with convex-layer anchoring constraints. The framework yields UNSAT certificates for a collection of anchored subfamilies. We also report pronounced runtime variability across configurations, including heavy-tailed behavior that currently dominates the computational effort and motivates further encoding refinements.