  The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external
memory. This enables handling big BDDs, but the performance suffers when
dealing with moderate-sized BDDs. This is mostly due to initializing expensive
external memory data structures, even if their contents can fit entirely inside
internal memory.
  The contents of these auxiliary data structures always correspond to a graph
cut in an input or output BDD. Specifically, these cuts respect the levels of
the BDD. We formalise the shape of these cuts and prove sound upper bounds on
their maximum size for each BDD operation.
  We have implemented these upper bounds within Adiar. With these bounds, it
can predict whether a faster internal memory variant of the auxiliary data
structures can be used. In practice, this improves Adiar's running time across
the board. Specifically for the moderate-sized BDDs, this results in an average
reduction of the computation time by 86.1% (median of 89.7%). In some cases,
the difference is even 99.9\%. When checking equivalence of hardware circuits
from the EPFL Benchmark Suite, for one of the instances the time was decreased
by 52 hours.
