SSoelvsten / adiar

An I/O-efficient implementation of (Binary) Decision Diagrams
https://ssoelvsten.github.io/adiar/
MIT License
24 stars 13 forks source link

Decrease `ptr_uint64::max_label` to support larger decision diagrams #524

Closed SSoelvsten closed 8 months ago

SSoelvsten commented 1 year ago

Currently, the ptr_uint64 class has the number of bits for the label set to 24 (similar as Sylvan). Yet, after the change #475, we have removed another bit from the level index. This decreases the maximum level size to 3 TiB and the largest BDD at 6 TiB before possibly breaking due to overflow errors.

Choices:

In ascending order of number of bits:

  1. If we fix the number of variables to be 16 bits, i.e. it fits into a uint16_t, then the compiler can give overflow warnings. This might be welcomed by the end-user.

  2. By default, the maximum file size on Linux (with ext4) is 16 TiB. We should at least support a BDD of this size, i.e. where the largest level is up to 8 TiB wide. Hence, we would want to use 39 bits for the level (12 TiB).

  3. In fact, considering #154, we may want to support each level reaching the maximum file size. This would require one more bit, i.e. the id needs 40 bits. Yet, at this point you have a single BDD of at least 32 TiB. Is this even realistic?

Other Tasks:

Additional Context:

For reference, here are the upper bounds in other BDD packages

BDD Package Max Variable Source
BuDDy 221 + 1 - 1 src/buddy/kernel.h #81
CAL 216 + 1 - 2 src/calInt.h #200
CUDD 232 (or 16) + 1 -1 cudd/cuddInt.h #205, #261
JBDD 217 + 1 - 1 src/main/java/de/tum/in/jbdd/BddImpl.java #L68
Lib-BDD 216 + 1 - 1 src/_impl_bdd_variable.rs
OxiDD 232 + 1 - 1 oxidd/crates/oxidd-core/src/lib.rs
PJBDD 232 + 1 - 1 src/org/sosy_lab/pjbdd/bdd/bddNode.java #41
Sylvan 224 + 1 -1 src/sylvan_mtbdd_int.h #L117
SSoelvsten commented 11 months ago

Asking Randy Bryant, Jaco van de Pol, and Anna Blume Jakobsen, they all confirm we can decrease the number of labels with a few bits.

SSoelvsten commented 8 months ago

With #591 we already brought the maximum safe BDD size back up 12 TiB; this seems out of reach for most (and even our own experiments). Hence, I will just close it for now.