Post A84xdSJDvsRbvRGRaC by jix@mathstodon.xyz
(DIR) More posts by jix@mathstodon.xyz
(DIR) Post #A84xdSJDvsRbvRGRaC by jix@mathstodon.xyz
2020-12-09T08:29:06Z
0 likes, 0 repeats
My paper where I prove the optimality of the smallest known sorting networks with 11 and 12 channels is out on arXiv: https://arxiv.org/abs/2012.04400Those were known since 1969, but whether smaller exist was an open problem since. 1/n
(DIR) Post #A84xdSnM7qXzQtMVY8 by jix@mathstodon.xyz
2020-12-09T08:31:26Z
0 likes, 0 repeats
This is also known as the Bose-Nelson Sorting Problem. For up to 7 channels, Floyd & Knuth determined the optimal sizes in 1966. In 1972 Van Voorhis published a result (which I'll mention again) that extends this to 8. Solving 9 and 10 took quite a bit longer... 2/n
(DIR) Post #A84xdTGQNlnct2xirI by jix@mathstodon.xyz
2020-12-09T08:31:26Z
0 likes, 0 repeats
In 2014 Codish, Cruz-Filipe, Frank & Schneider-Kamp used a new approach to compute the optimal size for 9 channels. This took over a week on a cluster. Van Voorhis's result, again, extends this to 10 channels. Later Cruz-Filipe & Schneider-Kamp formally verified this result. 3/n
(DIR) Post #A84xdThMlbLmEbZEqu by jix@mathstodon.xyz
2020-12-09T08:31:27Z
0 likes, 0 repeats
I'd been using sorting networks for encoding some problems for SAT solving. Last year I wondered whether I could find smaller ones. This lead me to the work of Codish et al. and I improved a subroutine that is the bottleneck in their approach: https://github.com/jix/sortnetopt-gnp 4/n
(DIR) Post #A84xdU7xAkcLZ40TIG by jix@mathstodon.xyz
2020-12-09T08:33:41Z
0 likes, 0 repeats
Frăsinaru and Răschip had already improved that subroutine, reducing the overall time to a few hours. My improvements got it down to under one hour. Scaling this up to 11 channels seemed impossible though. The memory requirements alone would be prohibitive. 5/n
(DIR) Post #A84xdUafRzaP07RP3A by jix@mathstodon.xyz
2020-12-09T08:33:42Z
0 likes, 0 repeats
I couldn't stop thinking about this: Van Voorhis's result is that s(n) ≥ s(n - 1) + ⌈log₂ n⌉ where s(n) is the optimal size for n channels. It happens to be strict for n = 8 and n = 10, even though the algorithm used to compute s(9) doesn't practically scale to s(10). 6/n
(DIR) Post #A84xdUz7z39UDyswAy by jix@mathstodon.xyz
2020-12-09T08:33:43Z
0 likes, 0 repeats
This lead me to believe that there is a structure that is exploited by Van Voorhis's bound that's completely unused by previous algorithms for computing s(n). After a lot of experiments I managed to generalize Van Voorhis's bound to what I call partial sorting networks. 7/n
(DIR) Post #A84xdVP0QpqtWEzbVo by jix@mathstodon.xyz
2020-12-09T08:36:02Z
0 likes, 0 repeats
These only have to sort a given subset of input sequences. Looking at a subset is not a new idea per se, but this definition allowed me to generalize Van Voorhis's bound and provided the basis for a new dynamic programming algorithm for computing s(n). 8/n
(DIR) Post #A84xdVrii4owxIQXGi by jix@mathstodon.xyz
2020-12-09T08:36:02Z
0 likes, 0 repeats
Since my generalization results in a bound that involves Huffman's algorithm I've been calling it the Huffman bound for partial sorting networks. Huffman's not only data compression ;) Using this in my dynamic programming algorithm then allowed me to compute s(9) in seconds! 9/n
(DIR) Post #A84xdWJN3GwGL3McMq by jix@mathstodon.xyz
2020-12-09T08:38:16Z
0 likes, 0 repeats
After some more optimization and fine tuning I was able to compute s(11) a bit over a year ago. Again, Van Voorhis's bound produced s(12) for free. I wasn't confident enough that my result is correct though, so I decided to also formally verify my result. 10/n
(DIR) Post #A84xdWn9GYl3pPIOmW by jix@mathstodon.xyz
2020-12-09T08:38:16Z
0 likes, 0 repeats
Formally verifying an optimized implementation of my algorithm seemed too hard, so like Cruz-Filipe & Schneider-Kamp I decided to instead have the algorithm produce a certificate and formally verify a checker for that. That's an approach I've also known from SAT solving. 11/n
(DIR) Post #A84xdXERd4anC44CKO by jix@mathstodon.xyz
2020-12-09T08:38:17Z
0 likes, 0 repeats
My initial attempts would have produced a certificate that is too large and slow to check with such a checker. Here I noticed that I could get a smaller certificate by reusing the routine of Codish et al. that I had previously optimized. 12/n
(DIR) Post #A84xdXh9uJYqd7V85I by jix@mathstodon.xyz
2020-12-09T08:40:36Z
0 likes, 0 repeats
This worked, but I still had to formally verify my certificate checker. For this I looked at several proof assistants and went with Isabelle/HOL. End of last year I then had a fully formally verified certificate checker and was certain that my result holds. 13/n
(DIR) Post #A84xdY9AEBxk1ybUjg by jix@mathstodon.xyz
2020-12-09T08:40:37Z
0 likes, 1 repeats
I pushed all my source code and formal proofs to GitHub (https://github.com/jix/sortnetopt), but hadn't written anything suitable for human consumption yet. Over the course of this year, with some breaks, I then wrote the paper with all the details, that I just put on arXiv. 14/n
(DIR) Post #A84xdYZOeewjLKsRcm by jix@mathstodon.xyz
2020-12-09T08:45:24Z
0 likes, 1 repeats
And since I forgot to include them with my first tweet, (https://twitter.com/jix_/status/1336588447902011393) here are some figures to look at :) 15/15