🧫[EXPERIMENTAL] Very slow implementation of inequality

[jonsterling]

This code is very bad and slow, but it is proof-of-concept. I used ocamlgraphs to implement it. Suggestions or rewrites are welcome.

[favonia]

I suggest avoiding using an external library. A map from vertices to reachable vertices should be more than enough.

[jonsterling]

I agree — I was just getting owned trying to compute the transitive closure by hand and i decided to give my brain a test.

…

On May 19, 2022, at 6:04 AM, favonia ***@***.***> wrote:  I suggest avoiding using an external library. A map from vertices to reachable vertices should be more than enough. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread.

[jonsterling]

OK the code doesn't work anymore, but it can no doubt be fixed. 😆

[favonia]

I want to repeat that I don't recommend following any existing algorithm papers. At least not now. They are not designed with full persistency in mind. According to a preliminary experiment I did 2 years ago (I just revived it: https://github.com/favonia/kusariyarou), none of the "advanced" algorithms work well in our settings. The one you cited (https://pure.tue.nl/ws/files/4393029/319321.pdf) is likely too complicated because we don't delete edges. What we need is incremental reachability testing, but even for that I could not find anything useful with full persistency.

Again, I strongly recommend maintaining just a set of reachable vertices for each vertex. It could take \Theta(n^2)-time to add an edge, but it doesn't matter when the number of vertices is likely very small.

[jonsterling]

@favonia Yes, I agree with you --- the reason I looked at a paper is that I am not interested in graph algorithms so I didn't want to figure out how to implement it myself. But this bit me in the ass since I think the algorithm in the paper I looked up had bugs anyway 😆

[jonsterling]

LMAO what is happening is that in the base case, dimension variables are being "compared" for inequality by their de bruijn level or something LMAO. But I can't figure out how tf this is happening.