Investigating Simple Drawings of $K_n$ using SAT

TL;DR

The paper presents a SAT-based framework for investigating simple drawings of the complete graph $K_n$ by encoding rotation systems and finite forbidden substructures into CNF formulas. It translates combinatorial drawing data into a solver-friendly representation using $X_{aib}$ and $Y_{abcd}$ variables, along with symmetry breaking and crossing-encoding to capture drawable configurations and edge crossings. The framework is applied to a broad set of problems, including Rafla's conjecture variants, empty triangles, uncrossed edges, crossing families, and generalized Erdős--Szekeres theorems, yielding both reproved results and new computational insights up to modest $n$ and across several drawing subclasses. It provides certificate-backed results (e.g., DRAT proofs) and a flexible platform for exploring larger instances, with additional attention to aesthetic visualization of the resulting drawings.

Abstract

We present a SAT framework which allows to investigate properties of simple drawings of the complete graph $K_n$ using the power of AI. In contrast to classic imperative programming, where a program is operated step by step, our framework models mathematical questions as Boolean formulas which are then solved using modern SAT solvers. Our framework for simple drawings is based on a characterization via rotation systems and finite forbidden substructures. We showcase its universality by addressing various open problems, reproving previous computational results and deriving several new computational results. In particular, we test and progress on several unavoidable configurations such as variants of Rafla's conjecture on plane Hamiltonian cycles, Harborth's conjecture on empty triangles, and crossing families for general simple drawings as well as for various subclasses. Moreover, based our computational results we propose some new challenging conjectures.

Figures (10)

• Figure 1: The four rotation systems on $4$ elements with their drawings. The second, third, and fourth are isomorphic. The first one represents the second isomorphism class.
• Figure 2: The three obstructions $\Pi_4^\textnormal{o}$, $\Pi_{5,1}^\textnormal{o}$, and $\Pi_{5,2}^\textnormal{o}$ for rotation systems.
• Figure 3: The two obstructions $\Pi_{5,1}^\textnormal{oc}$ (left) and $\Pi_{5,2}^\textnormal{oc}$ (right) for convex drawings. A triangle which is not convex is highlighted in red.
• Figure 4: The obstruction $\Pi_{6}^\textnormal{oh}$ for h-convex drawings. The convex side of the red triangle is the bounded side and for the blue triangle its the unbounded side.
• Figure 5: A perfect matching (red) in a non-convex and strongly c-monotone drawing of $K_8$, which does not contain a plane Hamiltonian cycle not crossing the matching edges. Edges which cross matching edges are marked in grey.

Theorems & Definitions (23)

• Lemma 1
• Proposition 1: AbregoAFHOORSV2015
• Theorem 2
• Conjecture 3: Rafla Rafla1988
• Theorem 4
• Conjecture 5: aov-2024-tcfhcsdcg
• Theorem 6
• Conjecture 7: BFROS2024
• Theorem 8
• Conjecture 9