To convert a formula into a ZDD or vice versa, you have to consider the set representation of the minterms, where only the positive variables are listed in the sets, and variables not listed are considered false. These minterms can also be written as a DNF, which is then the maximal DNF that lists a corresponding minterm for each satisfying assignment.
SNFs are essentially formula representations of BDDs. Therefore, we can also get DNFs or CNFs from them. An if-then-else operator (p → f0 | f1) with a variable p and formulas f0 and f1 can be written as
- (p → f1 | f0) = (!p|f1) & (p|f0)
- (p → f1 | f0) = (!p&f0) | (p&f1)
By repeating this, you can create a DNF or CNF from any SNF. For example, consider the following example:
a → (c → 0 | 1) | (b → (c → 0 | 1) | 1)
= a → !c | (b → !c | 1)
= a → !c | (b&!c | !b)
= !a&b&!c | !a&!b | a&!c
However, this is only a DNF and not a full DNF, which means that the minterms do not contain ALL variables, and we need a full DNF for the ZDD representation. Therefore, a minterm m that does not list a variable p must be expanded as follows
m = !p&m | p&m
This way, we obtain the following for the above example:
= !a&b&!c | !a&!b | a&!c
= !a&b&!c | !a&!b&!c | !a&!b&c | a&!c
= !a&b&!c | !a&!b&!c | !a&!b&c | a&!b&!c | a&b&!c
and this corresponds to the set representation that is then listed in the solution to generate the ZDD:
{{b}, {}, {c}, {a}, {a,b}}
