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

TL;DR

This paper advances the understanding of Norin's conjecture on 2-edge-colorings of hypercubes by extending finite case verification to n=8 and improving asymptotic bounds using enhanced SAT encodings.

Contribution

It introduces a more efficient SAT encoding that extends finite case verification and improves asymptotic bounds on the conjecture.

Findings

Verified the conjecture for n=8 using SAT solvers.

Improved asymptotic bound to 0.3125n + O(1) color changes.

Demonstrated SAT methods can advance combinatorial conjecture analysis.

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\v{r}\'ak (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\v{r}\'ak'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.