Hash function
Closed this issue · 3 comments
In https://www.cmi.ac.in/~madhavan/courses/verification-2011/andersen-bdd.pdf Chap 5, use pair and a prime as hash function.
If this approach works faster than fxhash?
That is a good suggestion. I made a quick comparison of the "raw performance" of the two approaches here (run cargo bench to see the results).
On my i5-6500, they are both essentially equal:
fx hash time: [294.96 ps 296.39 ps 298.21 ps]
andersen hash time: [294.32 ps 294.94 ps 295.59 ps]
However, note that this is without the remainder operation, which would need to be performed twice for the "andersen hash" (or we'd need a hash table which is always prime-sized, which rust tables aren't). Another important note is that this does not account for the price of collisions. I am not sure which hash will be more resilient to those, but from what I've seen, it is hard to come up with anything more robust than fxhash on non-adversarial data.
With sufficiently large BDDs, the limiting performance factor usually becomes the random memory access as the hash table will not fit into the L3 cache. So for these situations, anything that can compute the hash fast enough will be bottlenecked by RAM latency anyway :)
However, I'd be happy to accept a pull request if it turns out this hash is indeed significantly faster in practice.
Thanks for your reply. I have no more idea about it. You can close this pr if necessary.
I will post some other ideas about this repo later.
Cool! Ideas are always welcome. Also, if you need some API which we currently don't have, feel free to submit an issue for that. We are mostly adding features as we need them, so if you have a use case for something that we haven't thought of already, we'd be happy to add it.