Combinatorial Geometry of Erd\H{o}s--Szekeres Type Problems: SAT/ASP Modeling and Linear Subreduction

TL;DR

This paper introduces a computational framework combining SAT/ASP modeling and geometric inequalities to solve variations of the Erd ext{o}s--Szekeres problem, enabling efficient realization of configurations and establishing new exact bounds.

Contribution

It presents the linear subreduction method for geometric realization, integrating logical models with inequalities to accelerate SMT solving and find exact combinatorial bounds.

Findings

Proved that any bicolored set of 26 points contains an empty monochromatic quadrilateral.

Developed a unified approach for realizing geometric configurations from abstract models.

Established new exact values for Erd ext{o}s--Szekeres type functions.

Abstract

This paper investigates several classical and novel variations of the Erd\H{o}s--Szekeres problem, including multicolored point sets, convex hexagons with a given number of interior points, and polygons with constraints on edge colors. We propose a comprehensive computational framework combining combinatorial modeling within the SAT/ASP paradigms with the geometric realization of configurations. To determine point coordinates, we developed the \textbf{linear subreduction method}. The core idea consists of combining the complete logical model of the problem with a system of geometric inequalities, followed by fixing the abscissae to linearize the constraints. This approach enables a simultaneous search for a realization across the entire space of admissible abstract configurations (signotopes) rather than examining them individually, while linearization significantly accelerates the SMT solving process. Using this framework, we established new exact values for several functions; in particular, we proved $h_{nc}(4,0; 4,0)=26$: any bicolored set of 26 points in general position must contain the vertices of an empty monochromatic quadrilateral.