TdZdd
1.1
A top-down/breadth-first decision diagram manipulation framework
|
A DD has one root node and two terminal nodes (⊤ and ⊥). Every non-terminal node of an N-ary DD has N outgoing edges.
The above picture shows an example of binary DD structure, where the ⊥ terminal node and all edges to it are omitted for visibility; dashed and solid lines are 0- and 1-edges respectively. The DD represents a set of all 3-combinations out of 5 items. Note that levels of DD nodes are defined in descending order; the root node has the highest level and the terminal nodes have the lowest.
The following code from apps/test/example1.cpp is a DD specification of a binary DD structure representing a set of all k-combinations out of n items.
Class Combination
inherits from tdzdd::DdSpec<Combination,int,2>
, of which the first template parameter is the derived class itself, the second one is the type of its state, and the third one declares the out-degree of non-terminal DD nodes (N). The class contains public member functions int getRoot(int& state)
and int getChild(int& state, int level, int value)
.
getRoot
initializes the state
argument by the state of the root node and returns its level. getChild
receives state
and level
of a non-terminal node and integer value
in the range [0, N-1] selecting one of the N branches. It computes the state and the level of the child node. If the child node is not a terminal, it updates state
and returns the level. If the child node is ⊥ or ⊤, it returns 0 or -1 respectively; state
is not used in those cases.
A DD represented by a DD specification can be dumped in "dot" format for Graphviz visualization tools.
tdzdd::DdStructure<2>
is a class of explicit binary DD structures. Its object can be constructed from a DD specification object.
A DD structrue can be reduced as a BDD or ZDD using its void bddReduce()
or void zddReduce()
member function, and also can be dumped in "dot" format.
A DD structure can be evaluated from the bottom to the top. The following code from apps/test/testSizeConstraint.cpp is a DD evaluator to find the size of the largest itemset represented by a ZDD.
It is used as follows.
The construction and evaluation functions can also be used easily to implement import and export functions of DD structures from/to other DD libraries.
A DD specification is defined by deriving it from an appropriate one of the base classes defined in <tdzdd/DdSpec.hpp>.
Every DD specification must have getRoot
and getChild
member functions. getRoot
defines the root node configuration. getChild
defines a mapping from parent node configurations to child node configurations. If the node is not a terminal, the functions update state information and return a positive integer representing the node level. If the node is ⊥ or ⊤, they simply return 0 or -1 respectively for convenience, even though both nodes are level 0. We refer to such a return value as a level code.
is an N-ary DD specification using type T
to store state information. Class S
must implement the following member functions:
int getRoot(T& state)
stores state information of the root node into state
and returns a level code.int getChild(T& state, int level, int value)
receives state information of a non-terminal node via state
, the level of it via level
, and a branch label in the range [0, N-1] via value
; updates state
by state information of the child node and returns a level code.In addition, S
may have to override the following member functions:
bool equalTo(T const& state1, T const& state2)
returns if state1
and state2
are equivalent. The default implementation is state1 == state2
.size_t hashCode(T const& state)
computes a hash value for state
. The default implementation is static_cast<size_t>(state)
.Hash values for any two states must be the same whenever they are equivalent. As shown in Overview, we can use the default implementations and do not need to override them when T
is a fundamental data type such as int
.
is an N-ary DD specification using an array of type T
to store state information. The size of the array must be fixed to some positive integer m by calling predefined function setArraySize(m)
in the constructor of S
. The library handles the state information just as (sizeof(T)
× m)-byte raw data for efficiency; therefore, T
must be a data structure without object-oriented features (user-defined constructor, destructor, copy-assignment, etc.). Class S
must implement the following member functions:
int getRoot(T* array)
stores state information of the root node into array[0]
..array[m-1]
and returns a level code.int getChild(T* array, int level, int value)
receives state information of a non-terminal node via array[0]
..array[m-1]
, the level of it via level
, and a branch label in the range [0, N-1] via value
; updates array[0]
..array[m-1]
by state information of the child node and returns a level code.You can find an example in apps/test/example2.cpp.
is an N-ary DD specification using a combination of type TS
and an array of type TA
to store state information. The size of the array must be fixed to some positive integer m by calling predefined function setArraySize(m)
in the constructor of S
. The library handles the state information of the array just as (sizeof(TA)
× m)-byte raw data for efficiency; therefore, TA
must be a data structure without object-oriented features (user-defined constructor, destructor, copy-assignment, etc.). Class S
must implement the following member functions:
int getRoot(TS& scalar, TA* array)
stores state information of the root node into scalar
as well as array[0]
..array[m-1]
and returns a level code.int getChild(TS& scalar, TA* array, int level, int value)
receives state information of a non-terminal node via scalar
and array[0]
..array[m-1]
, the level of it via level
, and a branch label in the range [0, N-1] via value
; updates scalar
and array[0]
..array[m-1]
by state information of the child node and returns a level code. is an N-ary DD specification using no state information, which means that the DD does not have more than one node at any non-terminal level. Class S
must implement the following member functions:
int getRoot()
returns a level code of the root node.int getChild(int level, int value)
receives level of a non-terminal node via level
and a branch label in the range [0, N-1] via value
; returns a level code of the child node.The next example is a specification of a ZDD for a family of all singletons out of n items.
Every DD specification inherits from tdzdd::DdSpecBase<S,N>
, which defines common member functions including the one to generate a "dot" file for Graphviz.
Each DD specification may have to define its own printState
member function that prints text on each DD nodes.
Text of each level can also be customized by overriding printLevel
member function.
The default implementation prints the level
itself.
Operations on DD specifications are defined as global functions in <tdzdd/DdSpecOp.hpp>. Note that they are also applicable to DD structures.
returns a BDD specification for logical AND of two BDD specifications.
returns a BDD specification for logical AND of two or more BDD specifications. (since C++11)
returns a BDD specification for logical OR of two BDD specifications.
returns a BDD specification for logical OR of two or more BDD specifications. (since C++11)
returns a ZDD specification for set intersection of two ZDD specifications.
returns a ZDD specification for set intersection of two or more ZDD specifications. (since C++11)
returns a ZDD specification for set union of two ZDD specifications.
returns a ZDD specification for set union of two or more ZDD specifications. (since C++11)
optimizes a BDD specification in terms of the BDD node deletion rule.
optimizes a ZDD specification in terms of the ZDD node deletion rule.
creates a QDD specification from a BDD specification by complementing skipped nodes in terms of the BDD node deletion rule.
creates a QDD specification from a ZDD specification by complementing skipped nodes in terms of the ZDD node deletion rule.
The template class of DD structures is defined in <tdzdd/DdStructure.hpp>.
Note that DdStructure<N>
works also as the DD specification that represent itself.
A DD structure can be constructed from a DD specification using the following templated constructor.
The optional argument useMP
sets the attribute value of the object that enables OpenMP parallel processing. Note that the parallel algorithms are tuned for fairly large DDs and may not be very effective on small DDs.
The default constructor of tdzdd::DdStructure<N>
creates a new DD representing ⊥.
The next one constructs a new DD with n non-terminal nodes at levels n to 1, of which each one has N edges pointing to the same node at the next lower level.
When N = 2, it is a ZDD for the power set of a set of n items.
TdZdd provides an efficient method, called ZDD subsetting, to refine an existing ZDD by adding a constraint given as a DD specification.
This templated member function of tdzdd::DdStructure<N>
updates the current DD by a new DD for ZDD intersection of itself and the given DD specification. The original DD should be reduced as a ZDD in advance for this function to work efficiently.
The following member functions of tdzdd::DdStructure<N>
apply reduction rules to the current DD structure.
qddReduce()
applies the node sharing rule only. bddReduce()
applies the node sharing rule and the BDD node deletion rule, which deletes a node when all its outgoing edges point to the same child. zddReduce()
applies the node sharing rule and the ZDD node deletion rule, which deletes a node when all of its non-zero-labeled outgoing edges point to ⊥.
A DD evaluator can be defined by deriving it from tdzdd::DdEval<E,T>
defined in <tdzdd/DdSpec.hpp>.
defines the DD evaluator E that computes a value of type T.
A tdzdd::DDStructure<N>
object can be evaluated by E as follows.
Every DD evaluator must define the following functions:
void evalTerminal(T& v, int id)
receives a terminal node identifier (0 or 1) via id
and writes the value for it into v
.void evalNode(T& v, int level, tdzdd::DdValues<T,N> const& values)
receives the level
of the node to be evaluated and evaluation results for its child nodes via values
; writes the result value into v
.In evalNode
, the value and level of the b-th child node (b = 0..*N*-1) can be obtained through values.get(b)
and values.getLevel(b)
respectively.
The following member functions of tdzdd::DdStructure<N>
might be also useful.
gets the level of the root node.
gets the number of nonterminal nodes.
checks structural equivalence with another DD. Compare after reduction if you want to check logical equivalence.
checks structural inequivalence with another DD. Compare after reduction if you want to check logical inequivalence.
transforms a BDD into a ZDD.
transforms a ZDD into a BDD.
counts the number of minterms of the function represented by this BDD.
counts the number of itemsets in the family of itemsets represented by this ZDD.
returns an iterator to the first element of the family of itemsets represented by this ZDD. Each itemset is represented by std::set<int>
of levels of selected items.
returns an iterator to the element following the last element of the family of itemsets represented by this ZDD.