Generating Binary decision diagram from an available data structure

Question

This question is a bit long; please bear with me.

I have a data structure with elements like this {x1, x2, x3, x4, x5}:

{0 0 0 0 0, 0 0 0 1 0, 1 1 1 1 0,.....}

They represent all the TRUEs in the truth table. Of course, the 5-bit string elements not present in this set correspond to FALSEs in the truth table. But I don't have the boolean function corresponding to the said set data structure.

I see this question but here all the answers assume the boolean function is given, which is not true.

I need to build a ROBDD and then to ZDD from the given set data structure. Preferably with available python packages like these.

Any advice from experts? I am sure a lot has been done along the line of this.

Answer 1

With the Python package dd, which can be installed using the package manager pip with pip install dd, it is possible to convert the set of variable assignments where the Boolean function is TRUE to a binary decision diagram.

The following example in Python assumes that the assignments where the function is TRUE are given as a set of strings.

from dd import autoref as _bdd


# assignments where the Boolean function is TRUE
data = {'0 0 0 0 0', '0 0 0 1 0', '1 1 1 1 0'}

# variable names
vrs = [f'x{i}' for i in range(1, 6)]
# convert the assignments to dictionaries
assignments = list()
for e in data:
    tpl = e.split()
    assignment = {k: bool(int(v)) for k, v in zip(vrs, tpl)}
    assignments.append(assignment)

# initialize a BDD manager
bdd = _bdd.BDD()
# declare variables
bdd.declare(*vrs)
# create binary decision diagram
u = bdd.false
for assignment in assignments:
    u |= bdd.cube(assignment)

# to confirm
satisfying_assignments = list(bdd.pick_iter(u))
print(satisfying_assignments)

For a faster implementation of BDDs, and for an implementation of ZDDs using the C library CUDD, the Cython module extensions dd.cudd and dd.cudd_zdd can be installed as following:

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd --cudd_zdd

For this (small) example there is no practical speed difference between the pure Python module dd.autoref and the Cython module dd.cudd.

The above binary decision diagram (BDD) can be copied to a zero-suppressed binary decision diagram (ZDD) with the following code:

from dd import _copy
from dd import cudd_zdd


# initialize a ZDD manager
zdd = cudd_zdd.ZDD()
# declare variables
zdd.declare(*vrs)
# copy the BDD to a ZDD
u_zdd = _copy.copy_bdd(u, zdd)

# confirm
satisfying_assignments = list(zdd.pick_iter(u_zdd))
print(satisfying_assignments)

The module dd.cudd_zdd was added in dd == 0.5.6, so the above installation requires downloading the distribution of dd >= 0.5.6, either from PyPI, or from the GitHub repository.