jix
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...
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.
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.
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).
Incremental Solving and Proofs (Sat Solver Written in Rust)
Refactoring Varisat: 4. Heuristics (Sat Solver in Rust)
Refactoring Varisat: 3. Conflict Driven Clause Learning
Not Even Coppersmith's Attack
I took a quick look at F1 just now though. The way it makes use of the nametable and patterns is very similar to what I do. There are precomputed fully solid patterns at a fixed location and the non-solid patterns seem to be bump allocated.
It makes use of both layers though, drawing the street on one and everything else on the other. I think it uses per scanline scrolling to apply correct perspective to the street.
I can't say anything about how it actually renders into the tile map for now. That would require a lot more than looking at the VDP (graphics chip) debugger in an emulator.
There actually was an extension I did, that was scrapped because it just didn't look good. At some point there was support for dithering. That helps with the low color precision of the Mega Drive (3-bit/channel). It only supported 50% checkerboard dither though, which looked odd when animated. I toyed with some ideas on how to improve upon that and discussed them within our demo group, but in the end the decision was to not use dithering.
As the biggest part (but not all) of the demoscene is based in Europe, most demos target PAL hardware. The same is true for our demo group. NTSC ports can be very difficult if not impossible as PAL often does have a slight advantage in CPU cycles per frame. This is also the case on the Mega Drive.
Porting the polygon renderer shouldn't be a problem as it renders in an off-screen CPU RAM buffer. In the worst case it would have to skip more frames, having a lower effective framerate.
A lot of the other effects have very critical timing though. I've been told that porting some of them to NTSC is just impossible.
Pushing Polygons on the Mega Drive
I'm currently working on a write-up of the polygon to tile drawing routine used for the fullscreen 3D scenes.
I'm not sure about the time frame yet, but they will be posted at http://www.pouet.net/prod.php?which=69648 and/or http://www.pouet.net/topic.php?which=11035.
I don't think any of the known weaknesses of MD5 would help you in finding MD5(x) = x.
From the copyright headers he worked on it starting in 2009 and had the first public release in 2014 (actually 2010, see comment below). He certainly worked on other stuff in between too. This is also not a toy implementation. While I have no idea how it compares to state of the art engines, it does feature a whole bunch of optimizations and a JIT compiler.
a) use a random order for starting (and restarting) http://bl.ocks.org/jix/30e55ae16b99efe94bfc/ab5a84881174512a... and
b) start from the center and always restart with the innermost free cell http://bl.ocks.org/jix/30e55ae16b99efe94bfc/aeaced224b45a413...