TejasviTomar
October 2026 · Preprint

Sorting networks on 13 inputs need 45 comparators

Tejasvi Singh Tomar

In plain words

To sort numbers, a sorting network applies a fixed pattern of compare-and-swap steps, a design suited to chips and graphics processors. How few steps does it need? Bose and Nelson asked this in 1962. Floyd and Knuth answered for up to 8 numbers, and later work for up to 12. For 13 numbers the best network known, found by Juillé, uses 45 steps, and it had been proved that at least 44 are needed. This paper shows that 44 are not enough, so the answer is 45.

Abstract

Let S(N) be the least number of comparators in a sorting network on N inputs. The values are known for N ≤ 12. For 13 inputs the smallest known sorting network, found by Juillé, has 45 comparators, and the best proved lower bound has been 44. We prove S(13) ≥ 45, so S(13) = 45. The proof extends a two-value bound to partial sorting. If a network with L comparators sorts a set X of 0-1 vectors, then for suitable pairs of inputs the largest and the second largest value meet at most L − c comparators, where c is the cost of sorting the residual set left when their paths are deleted. Whether a single network stays within all these budgets is decided by a finite search over the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with 44 comparators discards each set that fails this test. The costs of the residual sets are bounded below using S(11) = 35 and exact costs of 9- and 7-channel sets. No set survives at depth 25. A separate verifier, with its own implementation of the test, checks the certificate written by the search. It trusts Harder's program for the exact 9- and 7-channel costs, the bound S(11) = 35, and this implementation of the test. A second proof, in Lean 4, checks the same certificate with another implementation of the test, which it proves sound, and proves the 9- and 7-channel bounds that it uses; its large computations run as compiled code. A third proof, also in Lean, has every computation checked by Lean's kernel and uses only the standard axioms.

Thirteen horizontal black lines crossed by 45 vertical bars with round ends, coloured by layer (ten layers, with six colours repeating), forming the comparator diagram of a 45-comparator sorting network on 13 inputs.
Illustration of a sorting network on 13 inputs with 45 comparators in 10 layers, from Bert Dobbelaere's list. Each vertical bar compares the values on two wires and swaps them if they are out of order; the colours, which repeat after six, mark the layers. The paper proves that every sorting network on 13 inputs has at least 45 comparators, so 45 is optimal.