Automated Symmetric Constructions in Discrete Geometry

TL;DR

This paper introduces a computational method combining SAT solvers and local search to find symmetric point configurations in discrete geometry, leading to new solutions and improved understanding of classical problems.

Contribution

It develops a novel approach embedding rotational symmetry into SAT encodings and introduces a local-search solver, advancing the computational tools for symmetric geometric configurations.

Findings

Found symmetric extremal solutions to the Erd ext{"o}s-Szekeres problem.

Discovered a 21-point solution for the unbalanced-points problem, improving previous results.

Enhanced solution interpretability and computational efficiency through symmetry constraints.

Abstract

We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discovering new solutions to some well-known problems in combinatorial geometry. Our approach takes the usage of SAT solvers in discrete geometry further by directly embedding rotational symmetry into the combinatorial encoding of geometric configurations. Then, to realize concrete point sets corresponding to abstract designs provided by a SAT solver, we introduce a novel local-search realizability solver, which shows excellent practical performance despite the intrinsic $\exists \mathbb{R}$-completeness of the problem. Leveraging this combined approach, we provide symmetric extremal solutions to the Erd\H{o}s-Szekeres problem, as well as a minimal odd-sized solution with 21 points for the everywhere-unbalanced-points problem, improving on the previously known 23-point configuration. The imposed symmetries yield more aesthetically appealing solutions, enhancing human interpretability, and simultaneously offer computational benefits by significantly reducing the number of variables required to encode discrete geometric problems.