From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin's Conjecture via SAT

TL;DR

The paper addresses Norin's antipodal conjecture for edge colorings of the hypercube $Q_n$ by developing a compact SAT-based encoding that verifies the conjecture up to $n=8$ and by reframing parts of Dvořák's asymptotic approach to obtain a tighter bound on color changes: at most $0.3125n + O(1)$. It introduces the $f$ and $ ext{hat}f$ functions and a scalable SAT encoding to compute them, enabling a quantitative asymptotic analysis via a hybrid human-guided proof structure with automated case analysis. A Cube And Conquer parallelization and symmetry-breaking strategies substantially improve practical solvability, allowing large-scale verification and enabling exploration of asymptotics through SAT. The results demonstrate that SAT-based methods can yield both finite-case confirmations and nontrivial asymptotic progress on combinatorial conjectures, with code and methodologies poised for further expansions.

Abstract

Norin (2008) conjectured that any $2$-edge-coloring of the hypercube $Q_n$ in which antipodal edges receive different colors must contain a monochromatic path between some pair of antipodal vertices. While the general conjecture remains elusive, progress thus far has been made on two fronts: finite cases and asymptotic relaxations. The best finite results are due to Frankston and Scheinerman (2024) who verified the conjecture for $n \leq 7$ using SAT solvers, and the best asymptotic result is due to Dvořák (2020), who showed that every $2$-edge-coloring of $Q_n$ admits an antipodal path of length $n$ with at most $0.375n + o(n)$ color changes. We improve on both fronts via SAT. First, we extend the verification to $n = 8$ by introducing a more compact and efficient SAT encoding, enhanced with symmetry breaking and cube-and-conquer parallelism. The versatility of this new encoding allows us to recast parts of Dvořák's asymptotic approach as a SAT problem, thereby improving the asymptotic upper bound to $0.3125n + O(1)$ color changes. Our work demonstrates how SAT-based methods can yield not only finite-case confirmations but also asymptotic progress on combinatorial conjectures.

Figures (5)

• Figure 1: An antipodal coloring of $Q_4$, with monochromatic geodesics between the antipodal vertices $(1,0,1,1)$ and $(0, 1, 0, 0)$ highlighted.
• Figure 2: Overview of conjectures and their implications. Recall that \ref{['conj:norine-geodesic']} holding for $n$ implies \ref{['conj:norine-allcolorings-geodesic']} for $n-1$.
• Figure 3: Illustration of the proof for \ref{['thm:asymptotic']}, following the method of dvorakNoteNorinesAntipodalColouring2020. The dotted lines show the improved antipodal geodesic by local changes.
• Figure 4: Edge coloring $c_4$ for the hypercube $Q_4$.
• Figure 5: Experimental results.

Theorems & Definitions (12)

• theorem 1
• theorem 2
• theorem 3: dvorakNoteNorinesAntipodalColouring2020 dvorakNoteNorinesAntipodalColouring2020
• lemma 1
• proof
• lemma 2: Proven computationally
• lemma 3
• proof
• lemma 4
• proof