Use Pastva and Henzinger's Unique Node Table (Trie buckets)

[ssoelvsten]

As noted in #697 , the design of the unique node table from #444 can be improved for cache-locality. In #697 , we proposed a simplified variation that might work out well enough due to #722 . Assuming we can identify some other "bad" case, we should further improve on the table by changing the buckets to be a trie .

Tasks

• Also, replace the next pointer in entry<T> with next_0, and next_1. These two values correspond to edges in something quite similar to a prefix-trie. This trie is traversed bit-by-bit based on the hash-value of the variable label and the index of the other child, i.e. the maximum one. While evaluating this requires a few more CPU cycles (and an extra if-statement) it completely collapses the depth of each buckets.

  Note: I am unsure how the deal with hash collisions in [Pastva2023]. In both cases, we can ignore the minimum node for the hash, since it is fixed.

  • Without Level-Agnostic Unique Node Table #722, the node is uniquely identified via its maximum child index and the parent's level.
  • With Level-Agnostic Unique Node Table #722, the parent has no level. But, we now care about both the maximum child's level and index. One can play around with zipping the maximum nodes level and index.

  Note: Note that, unlike a prefix-trie one does not traverse up to a unique prefix before being given the result. Instead, nodes are placed as early as possible on a path that matches its prefix. This is a vital insight to be able to include the next_0 and the next_1 pointers within entry<T>.

  Note: One can maybe draw inspiration from the Anatree I implemented (for an entirely different project) a few years ago.

References

• [Lovato2014] Alberto Lovato, Damiano Macedonio, and Fausto Spoto. “A Thread-Safe Library for Binary Decision Diagrams”. In: Software Engineering and Formal Methods (2014)

• [Pastva2023] Samuel Pastva and Thomas Henzinger. “Binary Decision Diagrams on Modern Hardware”. In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (2023)

[ssoelvsten]

As noted by Tom van Dijk (trolando/sylvan#54), the list version in #697 is already good because of its simplicity. The combination of #728 and especially #722 might also address the extreme cases more than enough to not make this an optimisation (in practice).