Skip to content

Usage

Jump to bottom
TelosCheney edited this page Jul 28, 2026 · 5 revisions

Usage

This repository exposes two main ways to use NDD:

API Package Best for
JNDD org.ants.jndd Performance-oriented code that is comfortable working with integer node IDs
JavaNDD org.ants.javandd Codebases that already use JavaBDD and want a factory/object-style API

JNDD Quick Start

The low-level API uses integer node IDs.

import org.ants.jndd.diagram.NDD;

int[] fieldBitWidths = {32, 32, 16, 16, 8};

NDD.initNDD(
    10_000_000, // nddTableSize
    1_000_000,  // nddCacheSize
    10_000_000, // bddTableSize
    1_000_000   // bddCacheSize
);

for (int bitWidth : fieldBitWidths) {
    NDD.declareField(bitWidth);
}
NDD.generateFields();

int srcIpHighBit = NDD.getVar(0, 0);
int dstIpHighBit = NDD.getVar(1, 0);
int packet = NDD.and(srcIpHighBit, dstIpHighBit);
double sat = NDD.satCount(packet);

The important ordering rule is:

  1. initNDD(...)
  2. declareField(...) for every field
  3. generateFields()
  4. perform logical operations

generateFields() materializes the shared, right-aligned variable layout. Fields using the same label mode share one backend engine and one variable layout.

Backends may be selected per field. The overload without a mode uses the initialization default, which is BOOLEAN_BDD for the normal initNDD(...) overload:

int src = NDD.declareField(32); // default BOOLEAN_BDD
int dst = NDD.declareField(32, NDD.LabelMode.COMPLEMENTED_BDD);
int protocol = NDD.declareField(256, NDD.LabelMode.FINITE_DOMAIN_ZDD);
NDD.generateFields();

For BDD and complemented-BDD fields, the declaration width is a binary bit width. For finite-domain ZDD fields it is the number of domain values. Operations dispatch edge-label work through the backend belonging to the node's field; labels from different fields/backends are never combined.

To select a non-default edge-label backend, pass a LabelMode to initNDD:

NDD.initNDD(
    10_000_000,
    1_000_000,
    10_000_000,
    1_000_000,
    NDD.LabelMode.FINITE_DOMAIN_ZDD
);

The supported low-level label modes are:

Mode Backend Notes
BOOLEAN_BDD Standard BDD labels Default
COMPLEMENTED_BDD Complemented-edge BDD labels Selected by --bcdd in the NQueens driver
FINITE_DOMAIN_ZDD Finite-domain ZDD labels Selected by --finite-domain-zdd in the NQueens driver

Internally, each label mode used by at least one field is constructed once through a common label-backend factory. NDD operations call the same label API for ref/deref, Boolean or set operations, counting, and GC. Homogeneous diagrams retain a single-backend fast path.

The legacy initNDD(..., mode) overload remains supported: it selects the default used by declareField(width). Explicit per-field modes may still be mixed with that default.

In mixed mode, use getFieldLabelMode(field) to inspect a field and the field-aware refLabel(field, label) / derefLabel(field, label) overloads for raw edge-label handles. The legacy overloads without a field remain available for homogeneous diagrams and reject ambiguous mixed-mode use. Aggregate label statistics are available through getLabelNodeCount() and getLabelTotalCreated(); overloads accepting a LabelMode return per-engine values.

JNDD Reference-Handling Notes

  • and, or, not, diff, and imp return node IDs that are not permanently protected
  • andTo and orTo consume the first operand and are often the cheaper update-style form in tight loops
  • variable nodes created by generateFields() are pinned in the table and are not reclaimed by GC

The NQueens example in application/nqueen/NDDSolution.java shows the intended style for building constraints while explicitly balancing ref / deref.

For field-level cofactors, satisfying-assignment enumeration, quantification, substitution, and the generic Boolean-operation API, see Manipulation APIs.

JavaNDD Quick Start

If you are migrating an existing JavaBDD codebase, use NDDFactory:

import org.ants.javandd.BDD;
import org.ants.javandd.BDDFactory;
import org.ants.javandd.NDDFactory;

int[] fieldBitWidths = {32, 32, 16, 16, 8};

BDDFactory factory = new NDDFactory(1_000_000, 1_000_000);
((NDDFactory) factory).setVarNum(fieldBitWidths, 10_000_000);

BDD one = factory.one();
BDD var = factory.ithVar(0);
BDD result = one.and(var);

Compared with plain JavaBDD, the main conceptual change is that NDD wants the field partition up front. Growing variables one bit at a time is supported poorly or not at all for realistic use cases; declare the full domain layout first whenever possible.

See also: src/main/java/org/ants/javandd/README.md

Running Repository Examples

NQueens Metrics Driver

Build first:

mvn -DskipTests package

Then run the maintained low-level NDD driver:

java -cp target/ndd-1.0.1-jar-with-dependencies.jar application.nqueen.NDDSolution 8 9 10 11 12

To exercise the complemented-BDD label mode:

java -cp target/ndd-1.0.1-jar-with-dependencies.jar application.nqueen.NDDSolution --bcdd 10 11 12

To exercise the finite-domain ZDD label mode:

java -cp target/ndd-1.0.1-jar-with-dependencies.jar application.nqueen.NDDSolution --finite-domain-zdd 10 11 12

The program emits one NQUEENS_METRICS ... line per board size, including runtime, created/alive node counts, and solution counts.

Legacy NQueens Harness

application/nqueen/NQueensExp.java is an older harness that writes a text file under results. It is still useful for quick comparisons, but NDDSolution is the better starting point if you want machine-readable metrics.

JavaNDD Example

application/nqueen/JavaNDDSolution.java shows the factory-style API. It is especially useful if your target codebase already expects BDD, BDDFactory, and ithVar(...).

Network-Verification-Oriented Usage

For network workloads, model each semantic packet field as one declared NDD field, for example:

  • source IP
  • destination IP
  • source port
  • destination port
  • protocol
  • flags or metadata fields

That field boundary is what allows NDD to reuse BDD structure across compatible domains. More on that workflow, plus the WAN/SRE and Batfish examples in this repository, is documented in Network Verification Applications.

Next Reading

Clone this wiki locally