Optimal size

Best known bounds

The following table displays the best known bounds for the minimal number of comparators needed to sort n inputs. For up to 8, the exact value has been known since 1973. Our contributions in the article Twenty-Five Comparators is Optimal when Sorting Nine Inputs (and Twenty-Five for Ten) raised the lower bounds for 9 and up, resulting in the exact values for 9 and 10.

n	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16
upper bound	0	1	3	5	9	12	16	19	25	29	35	39	45	51	56	60
old lower bound	0	1	3	5	9	12	16	19	23	27	31	35	39	43	47	51
improved lower bound									25	29	33	37	41	45	49	53

Log files and Informal Checker

The following table contains the (concatenated and compressed) logs of the generate-and-prune approach and the verification output for 7 to 9 inputs.

# inputs	7	8	9
logs	logs_7.bz2 (250 KB)	logs_8.bz2 (8 MB)	logs_9.bz2 (747 MB)
result	verification_7.txt	verification_8.txt	verification_9.txt

The following shell command was used to run the Java verifier on the log file for 9 inputs with the help of a Bash shell script:

./verifier.sh 9

Formally Certified Checker

We formalized the theory of size-optimal sorting networks in coq. You can download the formalization and the generated documentation (or browse the documentation online).

The following shell commands were used to first run the pre-processor on the log file for 9 inputs with the help of a Bash shell script:

./preprocessor.sh 9

The pre-processing step creates 25 oracle files oracle_9_1 to oracle_9_25 which serve as the input to the extracted verifier via its frontend. Compiling the certified extracted checker and its frontend as well as running it with the oracle files for 9 inputs can be done with the help of a Bash shell script:

./checker.sh 9 25