A library for Network Decision Diagram

This is a prototype implementation of the following paper:

Zechun Li, Peng Zhang, Yichi Zhang, and Hongkun Yang. "NDD: A Decision Diagram for Network Verification", NSDI 2025

Introduction

Network Decision Diagram (NDD) is a new decision diagram customized for network verification. It is more efficient than BDD when used for network verification, in terms of memory and computation. NDD wraps BDD with another layers of decision diagram, such that each node represents a field of the network, and each edge is labeled with a BDD encoding the values of that field. Due to the locality of fields in networks, NDD can significantly reduce the redundant nodes.

As an example, the figure below shows three BDDs in (a), and three equivalent NDDs in (c), each edge of which is labelled by per-field BDDs in (b).

Atomized Network Decision Diagram (Atomized NDD) is an extension of NDD, which offers a native support for equivalence classes, a key technique underlying most network verifiers. In atomized NDD, the label of each edge is a set of atoms, instead of a BDD as in standard NDD. Using atomized NDD, network verifiers do not need to implement their own algorithms for computing and updating equivalence classes.

Project Structure

• /doc stores an api documentation generated by javadoc.
• /lib stores the third party jar packages.
  • jdd-111.jar is a modified version of jdd library. The jar has been decompiled into /src/main/java/jdd so it can be edited directly.
  • javabdd_1.0b2.tar.gz is the original version of javabdd (for comparison).
• /results stores some experimental results generated by codes in /src/experiment.
• /src stores source code.

Getting Started

• lib
  • /lib/ndd-1.0-jar-with-dependencies.jar
  • /lib/jdd-111.jar

add <dependency> in pom.xml

<dependencies>
    <dependency>
        <groupId>org.ants</groupId>
        <artifactId>ndd</artifactId>
        <version>1.0</version>
        <scope>system</scope>
        <systemPath>${project.basedir}/lib/ndd-1.0-jar-with-dependencies.jar</systemPath>
    </dependency>
</dependencies>

After Maven sync, jndd and javandd can be chosen to import by:

import org.ants.jndd.*;
// or
import org.ants.javandd.*;

JNDD

/**
 * init NDD library
 * define cache size by `initNDD(NDD_TABLE_SIZE, NDD_CACHE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE)` if required (default 10000)
 */
NDD.initNDD(NDD_TABLE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE);

/**
 * declare ndd fields based on the situation {x, y, z}
 * declareField() only records the bit count, does not create BDD variables yet
 */
for (int i = 0; i < n; i++) {
    NDD.declareField(n);    // same number of variables in every field in nqueens
}

/**
 * generate fields after all declarations
 * this creates shared BDD variables with right-alignment for maximum node reuse
 */
NDD.generateFields();

/**
 * ndd logical operation
 */
NDD[] orBatch = new NDD[n];
for (int i = 0; i < n; i++) {
    /**
     * `getTrue()` or `getFalse()` to get NDD terminal nodes
     */
    NDD condition = NDD.getFalse();
    for (int j = 0; j < n; j++) {
        /**
         * `getVar(field_num, num)` same as `ithVar` after `createVar` in BDD
         * `orTo` will free (`deref`) the NDD variable in the first parameter
         * use `or` instead to keep it
         */
        condition = NDD.orTo(condition, NDD.getVar(i, j));
    }
    orBatch[i] = condition;
}

NDD queen = NDD.getTrue();

/**
 * sat count for result
 */
NDD.satCount(queen);

JavaNDD

If you are using a BDD version of factory and changing to NDD, please refer to src/main/java/org/ants/javandd/README.md

BDDFactory factory = new NDDFactory(BDD_TABLE_SIZE, BDD_CACHE_SIZE);

int[] fields = {}; // partion fields

factory.setVarNum(fields, NDD_TABLE_SIZE);

BDD TRUE = factory.one();
BDD FALSE = factory.zero();

BDD[] bdd_list = {};
for () {
    // or use `factory.getVar(field_num, num)` but it is incompatible with other factory
    // `ithVar(i)` will find its `field_num` first
    bdd_list[i] = factory.ithVar(i);
}

for (BDD bdd : bdd_list) {
    TRUE.and(bdd);
    FALSE.orWith(bdd);  // `applyWith` will free (`deref`) the BDD in parameter
}

return TRUE.satCount();

It is our first time to get access to the APIs in JavaBDD. If some are misunderstood, please contact us or Pull Request if you can. Your contribution to Network Decision Diagram is much appreciated.

GC Log Output

NDD provides optional GC (Garbage Collection) log output for debugging and performance analysis. When enabled, detailed logs will be printed before and after GC operations for both JDD (BDD layer) and NDD layers.

Enable GC Log

import jdd.util.Options;

// Enable GC log output
Options.gc_log = true;

// Disable GC log output (default)
Options.gc_log = false;

Log Output Format

When Options.gc_log = true, GC operations will output logs like:

[JDD GC] Start: table_size=10000, free_nodes=500, dead_nodes=100
[NDD GC] Start (triggered by JDD prehook): currentSize=5000, tableSize=100000
[NDD GC] End (triggered by JDD prehook): freed=200, currentSize=4800, time=15ms
[JDD GC] End: #5, freed=300, free_nodes=800, time=25ms

For JavaNDD (NDDFactory), the log prefix is [JavaNDD GC] instead of [NDD GC].

The triggered by field indicates whether the NDD GC was:

• JDD prehook: Called automatically before JDD GC to ensure NDD nodes are cleaned up first
• NDD self: Triggered by NDD's own table size limit

Benchmark

Benchmark (time second) on NQueens

N	BDD (JDD)	BDD (JavaBDD - JFactory)	NDD (JNDD)
6	0.017	0.056	0.012
7	0.023	0.072	0.019
8	0.04	0.109	0.038
9	0.223	0.28	0.176
10	0.615	0.913	0.344
11	2.567	4.424	2.257
12	19.109	33.024	12.417

Bibtex

@inproceedings {NDD,
  author = {Zechun Li, Peng Zhang, Yichi Zhang, Hongkun Yang},
  title = {{NDD}: A Decision Diagram for Network Verification},
  booktitle = {22th USENIX Symposium on Networked Systems Design and Implementation (NSDI 25)},
  year = {2025},
  isbn = {},
  address = {},
  pages = {},
  url = {https://www.usenix.org/conference/nsdi25/presentation},
  publisher = {USENIX Association},
  month = apr
}

Contact

• Zechun Li (1467874668@qq.com)
• Peng Zhang (p-zhang@xjtu.edu.cn)
• Yichi Zhang (augists@outlook.com)
• Hongkun Yang (hkyang@google.com)

License

Apache-2.0 License, see LICENSE.