Proving the optimal size of 11 and 12 input sorting networks

I computed and formally verified the minimal number of required comparators in a sorting network with 11 and 12 inputs, finding two more terms of A003075. This was an open problem for a long time. The candidate networks that I verified to be optimal were already known for 50 years, but there was no proof of their optimality.

The code that I used to compute this as well as the machine checked formal proof that the computed result is correct can be found in the sortnetopt GitHub repository.

To make the computation feasible I had to come up with a new result on sorting networks that allowed me to reduce the search space while still guaranteeing that I would find an optimal size network. This result, how I used it to construct a search algorithm and how I formally verified the computation are described in my paper “An Answer to the Bose-Nelson Sorting Problem for 11 and 12 Channels”.

I’ve also started a series of blog posts summarizing my results and giving a bit more context for the problem.