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

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.