ZDD

A zero-suppressed decision diagram (ZDD) is a graph-based representation of a finite family of finite subsets. Given a set of variables \(X = {x_1, \dots, x_n}\), a ZDD is a directed acyclic graph with non-terminal verices \(N\), also called decision vertices, and two terminal vertices \(\top\) and \(\bot\). Each vertex \(v \in N\) is associated with variable \(V(v) \in X\) and has two successor vertices \({\rm HI}(v), {\rm LO}(v) \in N \cup \{\top, \bot\}\). The vertices on a directed path to a terminal vertex follow a fixed variable order which guarantees the canonicity of the ZDD.

Given two ZDDs \(f\) and \(g\), the following list of operations is part of what is called a ZDD family algebra. These operations are implemented in the package.

Choose
Difference	\(f \;\backslash\; g = \{\alpha \, | \, \alpha \in f \; \text{and} \; \alpha \notin g\}\)
Intersection	\(f \cap g = \{\alpha \, | \, \alpha \in f \; \text{and} \; \alpha \in g\}\)
Join	\(f \sqcup g = \{\alpha \cup \beta \, | \, \alpha \in f \; \text{and} \; \beta \in g\}\)
Nonsupersets	\(f \searrow g = \{\alpha \in f\, | \, \beta \in g \; \text{implies} \; \alpha \nsupseteq \beta\}\)
Tautology
Union	\(f \cup g = \{\alpha \, | \, \alpha \in f \; \text{or} \; \alpha \in g\}\)

ZDD base

class bill::zdd_base

A zero-suppressed decision diagram (ZDD).

NOTE: This is a simple implementation. I would advise against its use when high-performance is a requirement.

Limitations:

• The number of variables N must be known at instantiation time.

Variables are numbered from 0 to N - 1.

Public Functions

inline node_index bottom() const

Returns the node index corresponding to the empty family

inline node_index top() const

Returns the node index corresponding to the unit family

inline node_index elementary(uint32_t var)

Returns the node-id corresponding to the elementary family {{var}}

inline node_index ref(node_index index, int32_t i = 1)

Increase the reference count of a node.

inline void deref(node_index index)

Decrease the reference count of a node.