jix
Joined 16 years ago
Karma
171
Submissions
29
Member since
Jan 20
Recent submissions
Comment · 3 years ago
Comment · 5 years ago
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.
Comment · 5 years ago
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.
Comment · 5 years ago
I replied to your other comment :)
Comment · 5 years ago
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 properties, but I also wouldn't be surprised if this was inspired by ILP.
Comment · 5 years ago
Computing s(11) and s(12) together took just below 5 hours on a 24 core server, but it also required almost 200 GB of RAM. Verifying the computation took about 3 days in total on the same server.
Computing s(9) and s(10) with the same approach takes under a second and a few megabytes, so while this is much faster than the previous approach (the one I described in the blog post) it still grows very quickly.
I don't know exactly how much s(13) would take, but extrapolating from the number I have for smaller n, my estimate is that it would take over 20000 TB of RAM and take proportionally longer. Distributing the computation would also slow it down a lot as all cores are doing frequent random accesses to all the used memory.
So s(12) seems to be the end of what's possible with this exact approach, but I think some of the theory I developed might be usable beyond.
Comment · 5 years ago
Author here, in case anyone has questions
Comment · 6 years ago
I haven't read everything, but it does contain a section about something I'm quite familiar with:
The article says "We compute the hashcode of the entire graph by hashing the multiset of WL labels. With one round, we’re just comparing the degree histogram. The more rounds we add, the more likely we are to detect a symmetry-breaker:", which is not correct.
Repeatedly re-labeling a graph by assigning a unique label to each unique neighborhood histogram, until the corresponding partition reaches a fixpoint would compute the one-dimensional Weisfeiler-Lehman refinement. But there are many non-isomorphic graphs that you cannot tell apart with this! It cannot tell apart any two regular graphs of the same size and degree, and you can easily run into those in practice.
Even if the code would repeat this process until a fixpoint is reached, instead of hoping that 10 iterations suffice, non-isomorphic graphs that result in the same WL partition means that "The more rounds we add, the more likely we are to detect a symmetry-breaker" doesn't hold.
There are also more efficient ways of computing this.
Now apart from one-dimensional WL refinement, where you compute a label from the neighborhood of individual vertices, there is also k-dimensional WL refinement, which very roughly speaking looks at all length k sequences of vertices and computes statistics for those. Here it is true that as k reaches |V| you will be able to tell apart any two non-isomorphic graphs, but only because if k=|V| you're trying all permutations! There is no fixed k that will tell apart any two graphs.
If you want to perform graph isomorphism tests in practice, I'd recommend Traces: http://pallini.di.uniroma1.it/
It combines two-dimensional WL refinement with a recursive search to tell apart all graphs, while using computational group theory algorithms to efficiently prune the search space for graphs with many symmetries. It is very efficient in practice.
It is described in https://arxiv.org/abs/0804.4881 (also linked from the website) and also has references for everything I wrote (modulo any mistakes I made while summarizing).
Comment · 6 years ago
That's just defining the term. AFAICT the law only says that an employee has a right to receive fair compensation for a technical improvement in some cases. It explicitly says that apart from that, procedures covering technical improvements are a matter of contracts: https://www.gesetze-im-internet.de/arbnerfg/__20.html
Comment · 9 years ago
For this project I don't really have to say much about the rust side of it. There were no surprises. The only thing special I can think of is the excellent cross-compiling support. That came in handy as I had to produce windows binaries for the 3D artists.
So you do understand why one wouldn't want to deal with a significant part of the user base here given that they behave in such ways, and thus why one might want to avoid any traffic coming from here, but feel that it's not your job to deal with those users, because then their behavior would affect you? I really hope you'll reflect on that...