Table of Contents
Fetching ...

Happy Ending: An Empty Hexagon in Every Set of 30 Points

Marijn J. H. Heule, Manfred Scheucher

TL;DR

The paper resolves Erdős’ long-standing question by proving $h(6)=30$: every planar point set in general position with $30$ points contains a $6$-hole. It achieves this with a compact, domain-consistent $O(n^4)$ SAT encoding for $k$-gons and $k$-holes, augmented by a partitioning strategy that enables near-linear speedups across thousands of cores and parallel proof checking via LRAT. The authors provide extensive optimization, empirical evaluation, and rigorous verification, including concurrent solving/checking and reencoding proofs, demonstrating that SAT techniques can solve deep open mathematical problems. This work not only tightens bounds on geometric existence problems but also showcases scalable, verifiable SAT-based methodology for tackling complex combinatorial geometry questions.

Abstract

Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein's exploration of unavoidable shapes in planar point sets in general position showed that every set of five points includes four points in convex position. For a long time, it was open if an empty hexagon, i.e., six points in convex position without a point inside, can be avoided. In 2006, Gerken and Nicolás independently proved that the answer is no. We establish the exact bound: Every 30-point set in the plane in general position contains an empty hexagon. Our key contributions include an effective, compact encoding and a search-space partitioning strategy enabling linear-time speedups even when using thousands of cores.

Happy Ending: An Empty Hexagon in Every Set of 30 Points

TL;DR

The paper resolves Erdős’ long-standing question by proving : every planar point set in general position with points contains a -hole. It achieves this with a compact, domain-consistent SAT encoding for -gons and -holes, augmented by a partitioning strategy that enables near-linear speedups across thousands of cores and parallel proof checking via LRAT. The authors provide extensive optimization, empirical evaluation, and rigorous verification, including concurrent solving/checking and reencoding proofs, demonstrating that SAT techniques can solve deep open mathematical problems. This work not only tightens bounds on geometric existence problems but also showcases scalable, verifiable SAT-based methodology for tackling complex combinatorial geometry questions.

Abstract

Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein's exploration of unavoidable shapes in planar point sets in general position showed that every set of five points includes four points in convex position. For a long time, it was open if an empty hexagon, i.e., six points in convex position without a point inside, can be avoided. In 2006, Gerken and Nicolás independently proved that the answer is no. We establish the exact bound: Every 30-point set in the plane in general position contains an empty hexagon. Our key contributions include an effective, compact encoding and a search-space partitioning strategy enabling linear-time speedups even when using thousands of cores.
Paper Structure (26 sections, 3 theorems, 23 equations, 9 figures, 2 tables)

This paper contains 26 sections, 3 theorems, 23 equations, 9 figures, 2 tables.

Key Result

theorem thmcountertheorem

$h(6) = 30$.

Figures (9)

  • Figure 1: An illustration for the proof of $h(4)= 5$: The three possibilities of how five points can be placed. Each possibility implies a $4$-hole.
  • Figure 2: The four ways a point $p_i$ can be inside triangle $\{p_a,p_b,p_c\}$ based on whether $i < b$ (left two images) and whether $p_c$ is above the line $p_ap_b$ (first and third image).
  • Figure 3: An illustration of triple orientations.
  • Figure 4: All possibilities to place four points, when points are sorted from left to right.
  • Figure 5: Three types of $6$-gons: left, all points are on one side of line (2 cases); middle, three points are on one side and one point is on the other side of line (8 cases); and right, two points are on either side of line (6 cases). If the marked triangle is empty, we can conclude that there exists a $6$-hole.
  • ...and 4 more figures

Theorems & Definitions (4)

  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • lemma thmcounterlemma: Scheucher2020
  • proof