Network Decision Diagram (NDD) is a new decision diagram, built on the classical Binary Decision Diagram (BDD). For BDD, each node looks at a single bit each time, and branches based on whether the bit is true or false; in contrast, each NDD node looks at a field consisting of a fixed number of bits each time, and branches based on what set of values the field takes. But different from the classical multi-valued decision diagram (MDD), where a branch takes one concrete value from a domain, each branch in NDD takes a symbolic value, i.e., a subset of values from a domain.
The branching conditions are compactly encoded with external data structures, including BDD, complemented-edge BDD (BCDD), and zero-suppressed decision diagrams (ZDD), etc. In this sense, NDD can be seen as wrapping a lower-level decision diagram with an outer field-aware layer, and therefore the name of NDD can also be interpreted as "Nested Decision Diagram".
An example of NDD In the above figure, we represent Hadamard matrix H4's values on each coordinate (x0x1, y0y1) as a BDD (in (b)) and an NDD (in (c)). Each NDD node represents a 2-bit field (f1 and f2), and the branching condition is encoded with 2 BDDs (in (d)).
The following table shows the benchmark for N-Queens with N=12 and N=13.
| Implementation | Language | N=12 time (s) | N=13 time (s) |
|---|---|---|---|
| BuDDy | C | 53.601 | >500 |
| CUDD | C | 31.968 | 224.422 |
| JDD | Java | 26.878 | 219.003 |
| JavaBDD-C | Java/C | 24.439 | 230.309 |
| JavaBDD | Java | 27.867 | 293.619 |
| DD-BDD | C# | 15.511 | 105.936 |
| DD-CBDD | C# | 13.055 | 83.637 |
| NDD | Java | 3.823 | 27.172 |
For more details, please refer to N-Queens Benchmark.
The NDD library provides offers the following APIs.
apply(): apply a logical operation on two NDDs,simplify():restrict(): fix a field value and obtain its cofactorsatCount(),anySat,allSat: count the number of satisfiable assignmentsexist(): existential quantification over one or more fields:substitute():
Refer to the API guide for more details.
NDD supports both homogeneous and mixed label backends: each field may select BDD, BCDD, or
set-family ZDD labels. Every width-w field has the same Boolean domain of 2^w bit vectors,
independent of its backend. Fields of the same type share one backend engine and right-aligned
variable layout. See the Usage and
Design Notes pages for details.
The former finite-domain ZDD experiment used a different, one-of-w domain and has been retired.
Its archived N-Queens measurements are identified as legacy data in
results/nqueens_backend_results.md; they are not results for
the current ZDD backend.
NDD was originally proposed for network verification, where each NDD node represents a packet header field (destination IP address) We observed NDD was more efficient than BDD in terms of memory and computation. The reason is due to the locality of field-based matching semantics, NDD can significantly reduce the number of nodes.
The current NDD libary is by far not the end, and we are working on extending it to support: (1) multiple terminals, (2) parallel computation, (3) using NDD for more applications like modeling checking.
- Main: Featuring an efficient design of node table.
- Reuse: Featuring the reuse of label decision-diagram variables among all fields.
- Original: The original prototype for NSDI '25 paper.
@inproceedings{NDD,
title={NDD: A Decision Diagram for Network Verification},
author={Li, Zechun and Zhang, Peng and Zhang, Yichi and Yang, Hongkun},
booktitle={22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25)},
pages={237--258},
year={2025}
}- Peng Zhang (p-zhang@xjtu.edu.cn)
- Yichi Zhang (augists@outlook.com)
- Zechun Li (1467874668@qq.com)
Apache-2.0. See LICENSE.