Proving 50-Year-Old Sorting Networks Optimal: Part 1 • Hacker News Board

Re: Proving 50-Year-Old Sorting Networks Optimal: Part 1

#11

Post by jix » Thu, May 06, 2021, 2:04 PM UTC

magicalhippo wrote: post #10

Fun stuff, and a very nice post! This is one of those topics where my mind starts racing. How many optimal, distinct networks per order are there (ie ignoring trivial exchanges in the sequence of comparators)? What if you have additional constraints, like maybe limited temporary storage (ie not all inputs can be loaded at once)? This isn't my field, but it's fun just trying to think about it.

Those are interesting questions! For example generating and looking at all networks of optimal size which have distinct circuits (assuming unlabeled inputs, so that rearranging those doesn't count as distinct) is something I still want to do at some point. Extending my search to produce this wouldn't be too complicated... but I haven't found the time for this so far.

Re: Proving 50-Year-Old Sorting Networks Optimal: Part 1

#12

Post by YeGoblynQueenne » Thu, May 06, 2021, 2:15 PM UTC

jix wrote: post #7

YeGoblynQueenne wrote: post #5

Nice piece of work, if a bit esoteric (or maybe that's the best part!). I was struck by this paragraph, towards the end (edited to remove copying artifacts): >> This is not quite yet the full approach used by Codish et al. Instead of using set inclusion to compare output sets, they define a relation called subsumption. Remember that above, where we introduced sorting networks, we noted that unconditional exchanges do…

Interesting :) Codish et al. have a background in SAT solving, which is somewhat related to logic programming. In SAT solving subsumption of clauses usually doesn't involve any substitutions. That's the notion of subsumption I was familiar with before reading Codish et al. Given that, extending subsumption to handle the symmetries inherent in the problem felt like a natural extension as it maintains all the relevant…

>> In SAT solving subsumption of clauses usually doesn't involve any substitutions.

I guess not, because SAT is propositional so just substituting variables for terms would yield a ground propositional clause. Actually I wasn't even sure we say "clause" in propositional logic. Anyway Plotkin's subsumption is really based off Robinson's unification algorithm and it makes a lot more sense in that context and in the context of resolution theorem proving. Or I'm just hopelessly stuck forever thinking in the first order.

Do you know if Codish et al. were based on an earlier paper for their definition of subsumption? It really sounds like they are simply describing it, rather than introducing it as a new concept.

Edit: of course, the obvious question in my mind now is whether it would be possible to learn sorting networks using one of the ILP approaches that build on Plotkin's work and don't have to perform an expensive search of a large hypothesis space.

Re: Proving 50-Year-Old Sorting Networks Optimal: Part 1

#13

Post by jix » Thu, May 06, 2021, 2:25 PM UTC

YeGoblynQueenne wrote: post #12

jix wrote: post #7

Earlier quoted context omitted.

Interesting :) Codish et al. have a background in SAT solving, which is somewhat related to logic programming. In SAT solving subsumption of clauses usually doesn't involve any substitutions. That's the notion of subsumption I was familiar with before reading Codish et al. Given that, extending subsumption to handle the symmetries inherent in the problem felt like a natural extension as it maintains all the relevant…

>> In SAT solving subsumption of clauses usually doesn't involve any substitutions. I guess not, because SAT is propositional so just substituting variables for terms would yield a ground propositional clause. Actually I wasn't even sure we say "clause" in propositional logic. Anyway Plotkin's subsumption is really based off Robinson's unification algorithm and it makes a lot more sense in that context and in the con…

The paper where they introduce subsumption is "Michael Codish, Luís Cruz-Filipe, Michael Frank, and Peter Schneider-Kamp. 2016. Sorting nine inputs requires twenty-five comparisons. Journal of Computer and System Sciences 82, 3 (May 2016), 551–563." and I just realized that I lost the actual citation while editing my blog post, fixed that now.

Re: Proving 50-Year-Old Sorting Networks Optimal: Part 1

#14

Post by YeGoblynQueenne » Thu, May 06, 2021, 3:49 PM UTC

jix wrote: post #13

YeGoblynQueenne wrote: post #12

Earlier quoted context omitted.

>> In SAT solving subsumption of clauses usually doesn't involve any substitutions. I guess not, because SAT is propositional so just substituting variables for terms would yield a ground propositional clause. Actually I wasn't even sure we say "clause" in propositional logic. Anyway Plotkin's subsumption is really based off Robinson's unification algorithm and it makes a lot more sense in that context and in the con…

The paper where they introduce subsumption is "Michael Codish, Luís Cruz-Filipe, Michael Frank, and Peter Schneider-Kamp. 2016. Sorting nine inputs requires twenty-five comparisons. Journal of Computer and System Sciences 82, 3 (May 2016), 551–563." and I just realized that I lost the actual citation while editing my blog post, fixed that now.

Thanks. I thought there was a citation missing! I'll have a look at the paper.