Visualization

Visualization

DOT export currently exists only on the feature/c branch. The feature/go port has no equivalent yet — if you need to visualize an NDD produced by the Go engine, temporarily swap in the feature/c .so and re-run.

MTPNDD (feature/c) can export any NDD subgraph as a Graphviz DOT description for visual inspection and debugging. Rendering is done offline with the standard dot CLI.

C API

Declared in mtpndd/mtpndd_node.h:

void mtpndd_fprint_dot(FILE *out, mtpndd_t *root);
void mtpndd_print_dot(mtpndd_t *root, const char *path);

• mtpndd_fprint_dot — write DOT to any FILE * (e.g. stdout, a pipe, or a file you opened)
• mtpndd_print_dot — convenience wrapper that opens path for writing and calls fprint_dot

The output is a single directed graph covering all nodes reachable from root, with:

• MTPNDD nodes as boxes labelled with their field id
• Edges labelled by the BDD representing that edge's label (rendered as a compact string)
• Terminal True / False as distinct leaves
• Multi-terminal arithmetic leaves (from mtpndd_arith.*) rendered with their value

There is no Java-side DOT export yet; render from the C side (e.g. from a unit test in mtpndd/test/) if you need it.

Example

mtpndd_t *f = mtpndd_and(x, y);
mtpndd_print_dot(f, "/tmp/f.dot");

Then render:

dot -Tpng /tmp/f.dot -o /tmp/f.png
dot -Tsvg /tmp/f.dot -o /tmp/f.svg
xdg-open /tmp/f.png

Built-In Dumps from the N-Queens Test

mtpndd_nqueens_test writes intermediate formulas to nqueens_dots/ in the current working directory when MTPNDD_NQUEENS_ENABLE_DOT=ON (default). Run it from a scratch directory so you don't litter the repo:

mkdir -p /tmp/nq && cd /tmp/nq
/path/to/build/mtpndd/mtpndd_nqueens_test 4
ls nqueens_dots/
dot -Tpng nqueens_dots/stage_final.dot -o final.png

Turn the dumps off at configure time with:

cmake -B build -DMTPNDD_NQUEENS_ENABLE_DOT=OFF

Tips

• Graphs for N ≥ 8 nqueens are unreadable as images. Use DOT export for small-scale debugging and rely on mtpndd_satcount / mtpndd_leafcount for sanity-checking large problems.
• If edge labels look garbled, it usually means the BDD-label printer is hitting very large BDDs; consider projecting onto a smaller variable set before exporting.