cs.DS — Data Structures and Algorithms

Sorting networks on 13 inputs need 45 comparators

Contributed by Tejasvi Singh Tomar

Let $S(N)$ be the least number of comparators in a sorting network on $N$ inputs (the Bose--Nelson problem). The values are known for $N\le12$, and for $13$ inputs the smallest known sorting network, found by Juill\'e, has $45$ comparators. We prove $S(13)\ge45$, so $S(13)=45$. Deleting the comparators met by the largest and the second largest input leaves a sorting network on $N-2$ inputs, so $S(N)\ge S(N-2)+P(2,N)$, where $P(2,N)$ is the least possible worst-case number of comparators met by these two values. Van Voorhis stated $P(2,N)\ge\lceil\lg F(N)\rceil$ for an explicit function $F$, but Mericanii showed that his proof is invalid. We prove $P(2,N)=\lceil\lg F(N)\rceil$ for $3\le N\le32$ by a finite search, which rests on the structure of the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. With $S(11)=35$ this bound gives only $S(13)\ge44$. For $45$ we apply it to the suffix of a network: if a network with $L$ comparators sorts a set $X$ of $0$-$1$ vectors, then for suitable pairs of inputs the two values meet at most $L-c$ comparators, where $c$ is the cost of sorting the residual set left when their paths are deleted. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with $44$ comparators discards each set for which no single network stays within all these budgets, and no set survives at depth $25$. A separate verifier checks the certificate written by the search. Two proofs in Lean 4 check the same certificate, and in one of them Lean's kernel checks every computation, with only the standard axioms. Juill\'e's network is checked in the kernel as well. As a consequence, each of the twenty lower bounds on $S(N)$ for $13\le N\le32$ that rested on Van Voorhis's inequality is proved and raised by one.