Skip to content

Design Notes

TelosCheney edited this page Aug 5, 2026 · 5 revisions

Design Notes

This page gives the implementation-level rationale behind the optimized branch.

It is meant for readers who already understand what NDD is and want to know how this repository's array-backed implementation is organized internally.

Overview

The optimized branch keeps the same conceptual model:

  • one NDD node corresponds to one field
  • each outgoing edge is guarded by a lower-level decision-diagram label
  • logical operations recurse over fields and labels

What changes is the storage and execution strategy used to implement that model efficiently in Java.

1. Array-Backed Node Table

The original implementation represented each node as an object with nested edge structures. In this branch, NodeTable.java stores node state in parallel arrays.

That means:

  • node metadata lives in dense primitive arrays
  • edge payloads are stored in shared arrays
  • canonical nodes reference edge blocks by index rather than owning separate edge containers

This is the main memory-layout change behind the current NDD implementation.

2. Global Edge Collection

During recursive logical operations, the implementation accumulates candidate edges in one shared stack-like structure instead of allocating temporary maps inside each call. Each recursive operation owns a stack frame [frameStart, stackTop) in that shared buffer.

Two helpers in NDD.java manage the frame:

  • edgeCollect(target, label) appends one edge to the current frame in O(1). It does not deduplicate on the way in: duplicate targets are tolerated and merged later. The earlier implementation merged duplicates on every collect, which cost an O(D^2) linear scan per node at high fan-out D; deferring the merge keeps this hot path branch-free.
  • edgeFlush(field) turns the frame into a canonical node. It (1) sorts the frame by target, (2) merges runs of equal targets with a consuming OR on their labels, then (3) creates or reuses the node through NodeTable.mk, which requires a sorted, deduplicated edge order.

The sort inside edgeFlush is size-adaptive:

  • small/medium frames use an in-place quicksort that falls back to insertion sort for short runs. NDD fan-out is usually tiny, so this matches the cost of the previous insertion-sort path in the common case.
  • large frames — at or above ndd.radixThreshold (default 64) — use an O(n) LSD radix sort over the packed (target, label) pairs, which avoids the comparison-sort blow-up at high fan-out.

Safe-point maintenance after the recursion unwinds keeps retired stack and edge slots reusable.

The point of this design is to keep the hot collect path allocation-free, then defer the single canonicalization step (sort + merge) to one place that can pick the right algorithm for the frame size.

3. Deferred Field Materialization

declareField(...) and generateFields() are deliberately separate.

Why:

  • the implementation needs to know every field width before laying out shared BDD variables
  • that global view is what makes right-aligned reuse possible within each label backend
  • it also keeps the field model explicit for packet-processing applications

For mixed diagrams, fields are grouped by LabelMode. Each group computes its own maximum width and creates one shared right-aligned variable layout, so BDD, BCDD, and set-family ZDD fields do not allocate duplicate engines or lose reuse among fields of the same type.

This is why the library expects users to commit to a field partition and its label modes early.

4. Safe-Point Recycling

The array-backed layout introduces a constraint that the implementation must respect: recursive operations may still hold raw edge-array positions while the recursion stack is active.

Because of that, edge compaction and retired-slot reuse happen only at safe points after recursion unwinds. Relevant methods include:

  • NDD.runSafePointMaintenance()
  • NodeTable.compactEdgesIfNeeded()
  • NodeTable.compactEdgesAtSafePoint()

5. Label Backend Abstraction

The low-level implementation supports multiple edge-label engines behind one internal backend interface:

  • standard BDD labels
  • complemented-edge BDD labels
  • set-family ZDD labels

declareField(width, mode) selects a backend per field. The overload without a mode uses the initialization default. A small backend registry creates at most one engine for each active LabelMode; unused modes allocate no engine.

An edge does not store a backend tag. Its parent NDD node already stores a field index, and that field determines the backend used to interpret, reference, combine, count, or release the edge label. Labels are combined only when recursive operations reach the same field, so handles from different engines never participate in the same label operation even if their integer values coincide.

Common label operations such as ref, deref, and, or, diff, not, matches, satCount, node counting, and GC go through the same backend API. The edge collector carries the owning field when it may release a label; NodeTable.mk and NDD GC similarly derive the backend from the node's field. This avoids adding a backend array to the node or edge table.

Set-family ZDD counting uses an engine-level primitive DoubleCache, and the enclosing NDD count separately memoizes macro-node states. The cache is cleared with the other ZDD caches after node-table GC, so cached handles cannot outlive recycled nodes. This avoids both exponential revisits in JDD's original ZDD.count() and per-call boxed maps.

Homogeneous diagrams retain a direct labelBackend fast path. Diagrams that actually mix modes use materialized field-to-backend and field-to-mode arrays rather than list/interface lookup in hot loops. Per-engine node creation counters are used for statistics because the legacy JDD counter is process-global and cannot distinguish simultaneous BDD and ZDD engines.

NDD difference is an ordered, memoized macro operation. It applies native backend diff to edge residuals directly; or, not, and diff do not synthesize a full label complement followed by intersection. This matters especially for sparse ZDD families, where a temporary universe-relative complement can be much larger than the desired residual. ZDD also caches the frequent intersect(1, x) empty-set-membership query.

Each label mode can be assigned an independent initial node-table/cache capacity with configureBackendCapacity(mode, tableSize, cacheSize) after initNDD and before the first field of that mode is declared. The default remains the common sizes passed to initNDD; independent sizing is an optional, workload-measurement-based optimization for mixed deployments.

The complemented-BDD backend uses integer handles whose low bit is the complement attribute. Internal nodes are stored in primitive structure-of-arrays tables; the high child is normalized to a regular handle, so a function and its complement share the same regular node and not only flips one bit. Primitive unique/apply/count/minimum-path caches avoid boxed keys. External label references and permanently protected variable roots drive mark/sweep collection; GC rebuilds the unique table and invalidates all handle caches. andTo and orTo follow the JDD ownership contract: they reference the result and consume the owned left operand.

All three backends describe the same logical field domain. A width-w field denotes 2^w Boolean bit vectors. BDD and BCDD encode a set of assignments as a Boolean characteristic function. ZDD encodes it as a family of subsets: a subset contains exactly the bit variables that are true in that assignment.

This distinction requires an explicit universe for each ZDD field. ZDD terminal 1 is the family containing only the empty set, not the family of all assignments. During generateFields(), NDD therefore builds and retains the powerset of the field's right-aligned bit variables. Positive and negative literal labels select, respectively, the members containing or omitting one variable; intersection, union, and difference then implement Boolean AND, OR, and complement relative to that field universe. The removed finite-domain ZDD backend instead treated a width as a one-of-w domain and is no longer part of the API.

The current mixed-mode boundaries are deliberate:

  • substitute requires source and target fields to use the same backend and width
  • raw-label refLabel / derefLabel calls require a field in mixed mode
  • toBDD and toNDD remain homogeneous standard-BDD conversion helpers

6. API Shape

JNDD

The low-level API uses integer node IDs. This matches the array-backed representation and avoids wrapper allocation on the hot path.

JavaNDD

The NDDFactory layer keeps a BDDFactory-style API for compatibility with codebases built around JavaBDD.

That compatibility layer is especially relevant for the Batfish-style integration documented in Network Verification Applications.

7. Interpreting The Benchmark Variants

When reading the result pages:

  • NDD-Origin is the baseline implementation
  • NDD-Reuse isolates the effect of shared-BDD-variable reuse
  • NDD adds the array-backed node table and stack-based edge collection

That split is useful because it shows which gains come from better symbolic structure and which come from the new runtime representation.

Clone this wiki locally