Pinned toot

Going to start my Mastodon account with a result I put quite a bit of work into: Sorting 11 inputs using a sorting network requires 35 comparisons and sorting 12 inputs requires 39 comparisons. I still haven't finished writing the paper (and should be working on that instead), but all the code including a formal proof in Isabelle/HOL is on github: github.com/jix/sortnetopt

Being a rust project it still builds and works perfectly fine AFAICT, but some of the dependencies are seriously out of date or unmaintained/abandoned. Also I need to setup CI for it again, as I stopped using the provider I chose when I was still actively working on that project

TFW an open source project you didn't find time to maintain for over a year suddenly gets quite a bit of traffic… I did plan to get back to it (to rewrite large parts and rearchitect it quite a bit) but now I feel somewhat compelled to clean up the bit rot before I get to that

It seems Bellman called it successive approximation. AFAICT that term didn't really catch on. I like it though, so I'm going to use it. In context: "Given some recurrence we can get a DP algorithm using memoization and a different one using successive approximation."

Personally I think of it as "abstract interpretation of the plain DP algorithm", but if there is an established term in DP literature it'd be a good idea to mention that in what I'm currently writing.

For a problem w/ optimal substructure, i.e. where dynamic programming works, there is a common pattern where you compute bounds on the solution of each subproblem and refine those iteratively in some way instead of just caching complete solutions.

Does it have a name?

E.g. the Bellman-Ford algorithm uses this (with one sided bounds), and for that Wikipedia calls this "relaxation" which seems like it could fit, but to me it doesn't seem like it's commonly used to describe this approach.

I released a new version 0.2.0 of my vec_mut_scan crate 🦀️📦️

github.com/jix/vec_mut_scan

The crate offers an improved variant of std's nightly only Vec::drain_filter, but which works on stable rust today and is a bit more flexible. It's an operation I often need when efficiently implementing various algorithms.

🆕️ Minor API tweaks
🆕️ Better docs of internals, covering all use of unsafe, including cute ASCII diagrams:

@11011110 I just realized that ref [5] in the paper contains the number of unlabeled sona curves for $$n \le 10$$ and drawings for $$n \le 4$$. It's also in OEIS: oeis.org/A008981

Some of the linked related sequences have additional literature references, overall containing a good part of the ideas I had.

I haven't found my exact approach, though, which I think might scale to larger n, and also not something counting curves with labeled inner faces, so I might still go ahead with that.

As I already mentioned, I still need to finish writing the paper for this. There is a bit more detail in the slides files.jix.one/s/20200707.pdf of talk I gave, but it wasn't recorded and the slides aren't that self-contained. I'm always happy to answer any questions about this, though :)

I worked around that by using the ideas behind Codish, Cruz-Filipe, Frank & Schneider-Kamp's computer search to minimize the generated certificate down to 3GB. That takes another 72 hours of processing on a 24 core server, but the resulting certificate can be checked using a formally verified checker within 3 hours on a laptop.

To have a result that can be trusted, I also wanted to formally verify it. Formally verifying the whole algorithm doesn't seem feasible to me though. Instead I used the common strategy to emit a certificate during the search and wrote a much simpler checker and verified that. Problem the certificate would be _much_ larger than 180GB and processing it with a verified (and thus not as optimized) checker also isn't feasible.

Based on that new bound, I came up with a search using dynamic programming and canonicalization. That allowed me to compute $$s_{11}$$ and $$s_{12}$$. It took 5 hours and 180GB of RAM on a big server with 24 cores. In comparison my search finds $$s_9$$ in 5 seconds and 40MB (different units!) on a laptop, which shows how fast this gets difficult with growing $$n$$.

So I set out to find a way to use the idea behind Van Voorhis's bound as part of a computer search. For that I found a generalized version of it, that gives a lower bound for a comparator network required to sort only a given subset of the possible input sequences. You recover Van Voorhis's bound when that set contains all possible inputs. Maybe surprisingly, Huffman's algorithm makes an appearance in the generalized bound.

Van Voorhis's bound states that $$s_n \ge s_{n-1} + \lceil \log_2 n \rceil$$ where $$s_n$$ is the number of comparators required for a sorting netowrk on $$n$$ inputs. We get an equality for 2,3,4,6,8,10 and it turns out 12 inputs. Given that computing the result for 9 inputs took so much effort, this seemed like a really powerful bound to me.

For 10 inputs already, their approach would take way too long and require too much memory. Luckily, Van Voorhis's bound (doi.org/10.1109/TC.1972.500902) which already solved the 8 inputs case, happens to match the known upper bound for 10 inputs again, based on the exact result for 9 inputs.

For 9 inputs they did a computer search on a cluster that took over a week: doi.org/10.1016/j.jcss.2015.11 That wasn't brute force search though, they came up with a nice way to prune large parts of the search space. Optimizing their algorithm allows the same computation to finish on a single server within a few hours (e.g. doi.org/10.1007/978-3-030-1921 or github.com/jix/sortnetopt-gnp).

The problem of determining the minimal number of required comparators in a sorting network is also known as the Bose-Nelson Sorting problem. Floyd and Knuth first computed it exactly for up to 7 inputs. A bound by Van Voorhis extended that to 8 inputs. After that it took over 40 years for further progress: in 2014 Codish, Cruz-Filipe, Frank & Schneider-Kamp computed it for up to 10 inputs.

Going to start my Mastodon account with a result I put quite a bit of work into: Sorting 11 inputs using a sorting network requires 35 comparisons and sorting 12 inputs requires 39 comparisons. I still haven't finished writing the paper (and should be working on that instead), but all the code including a formal proof in Isabelle/HOL is on github: github.com/jix/sortnetopt

New post: Sona enumeration, 11011110.github.io/blog/2020/0

Given $$n$$ points in the plane, how many different ways are there to draw a unicursal self-crossing curve that places exactly one point in each of the regions of the plane that it surrounds?

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!