2

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.

  • 1
    You do have the boolean function, just in a different format. The function that's defined by your example data is `(!x0&!x1&!x2&!x3&!x4)|(!x0&!x1&!x2&x3&!x4)|(x0&x1&x2&x3&!x4)|...`. – Paul Hankin Apr 22 '20 at 23:44
  • Okay thanks! Can I use this boolean function to construct BDD? May I ask which software I should look for and what is their mode of input? –  Apr 23 '20 at 19:50
  • I'm not sure. You said you couldn't use the answers to the other question because you didn't have a boolean function. What's stopping you use those answers now? – Paul Hankin Apr 24 '20 at 07:11
  • Nothing really! –  Apr 24 '20 at 19:26

1 Answers1

4

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.

0 _
  • 10,524
  • 11
  • 77
  • 109
  • Thank you for the detailed answer. If I want to implement this: https://stackoverflow.com/questions/59815531/intersection-of-bdd-zdd-using-cudd using this python package where I want to build the two BDDs corresponding to "1100" and "0000" first and then plot a BDD of their intersected elements as in AND; is there any way to do it? I don't see any AND function here. –  May 27 '20 at 05:53
  • 1
    Logical conjunction ("AND") can be computed with `w = u & v` for two BDD `Function` instances `u` and `v`, or with `w = bdd.apply('and', u, v)` where `bdd` the BDD manager of `u` and `v`. Plotting is possible with `bdd.dump('foo.pdf', [w])` or `bdd.dump('foo.png', [w])` (an example of plotting is https://github.com/tulip-control/dd/blob/master/examples/np.py#L38). – 0 _ May 27 '20 at 11:29
  • Thank you again; from your very first example code the image I receive for BDD is: https://ibb.co/8DSX2CZ whereas what I wanted is this: https://ibb.co/NyhM88k I can extend your example to what I want but just to ask, why is this graph so big? It doesn't look like a typical BDD. I wanted a BDD that would show only the data = {'0 0 0 0 0', '0 0 0 1 0', '1 1 1 1 0'} pointing to 1 and otherwise 0. –  Jun 01 '20 at 22:00
  • 1
    The first image includes also intermediate BDDs constructed during computations, because it includes all the BDDs in the BDD manager. One possibility is `del` references other than the desired one and call the method `bdd.collect_garbage()`. Another option is to plot the BDD nodes reachable from only selected root nodes. If `w` is the root node of interest, then this can be done with `bdd.dump('foo.pdf', [w])` or `bdd.dump('foo.pdf', roots=[w])`. There can be multiple roots when plotting using `dd.autoref`. – 0 _ Jun 02 '20 at 08:59
  • I want to "AND" a lot of BDD Function instances just like:https://stackoverflow.com/questions/59815531/intersection-of-bdd-zdd-using-cudd, where an example of just one "AND" is shown. Also, I don't want any intermediate BDDs in the BDD functions.I am assuming I have to initiate multiple managers. Here is what I came up with for 4 BDD instances where 3 ANDs will be needed: a = _bdd.BDD() b = _bdd.BDD() c = _bdd.BDD() d = _bdd.BDD() w = a & b & c & d; is it the correct way? –  Jun 10 '20 at 02:21
  • 1
    Working within one BDD manager, with intermediate results (it is impossible to not construct intermediate results) the conjunction of multiple BDDs can be computed by successive conjunction of pairs of BDDs, as for example `bdd = _bdd.BDD(); bdd.declare('x', 'y', 'z'); a = bdd.add_expr('x'); b = bdd.add_expr('y'); bdd.add_expr('z'); w = a & b & c`. Plotting the individual BDDs is possible with, for example, `bdd.dump('foo_a.pdf', [a])` or all in one plot with `bdd.dump('foo.pdf', [a, b, c, w])`. – 0 _ Jun 10 '20 at 07:46
  • Is it possible to please list the download steps for the dd package from its GitHub repository? I installed the Cython module extensions but like you said the cudd_zdd is missing from there. How do I install both versions (pure python and cython bindings) of dd including the cudd_zdd? –  Jun 14 '20 at 01:11
  • 1
    Using [`git`](https://git-scm.com/) the repository can be obtained with `git clone https://github.com/tulip-control/dd.git`. Then `cd dd/` and `python setup.py install --fetch --cudd --cudd_zdd`. Alternatively, a zip can be downloaded from https://github.com/tulip-control/dd/archive/master.zip, then unzipped and `dd` built from the sources inside the zip archive with `python setup.py install --fetch --cudd --cudd_zdd`. When `dd` version 0.5.6 will be released, it will include the module `dd.cudd_zdd` so the download steps with `pip` from PyPI above will then install also `dd.cudd_zdd`. – 0 _ Jun 14 '20 at 09:37
  • I followed your instructions and this is what I get at the end for git clone method (only the end is shown): https://ibb.co/FD2qjKp And this is for the zip method(only the end is shown): https://ibb.co/smKXKv8 --cudd_zdd is said to be not recognized at the end for the first method. Is this normal? From my understanding if the above methods are followed it should also include --cudd_zdd..right? In that case the second method works? –  Jun 17 '20 at 20:45
  • There is a "d" missing in `--cudd_zdd` in the error message. – 0 _ Jun 18 '20 at 03:10
  • @loannis With the dd package is there any way to declare boolean don't care states? –  Nov 01 '21 at 21:43
  • For example, if I want to see how many combinations of xx00 to xx11 would be possible, where x represents either '1' or '0'? I assume there would be total of 16 possibilities... –  Nov 01 '21 at 21:54
  • 1
    One way to compute this particular result (number of assignments over more variables than those variables that the BDD depends on, i.e., than the BDD's support) is to `import dd.autoref as _bdd; bdd = _bdd.BDD(); bdd.declare(*(f'x{i}' for i in range(4))); u = bdd.add_expr('~ x2 /\ ~ x3'); v = bdd.add_expr('x2 /\ x3'); n1 = bdd.count(u, nvars=4); n2 = bdd.count(v, nvars=4); print(n1 * n2)`. Relevant: `list(bdd.pick_iter(u, care_vars=[f'x{i}' for i in range(4)]))`. Regarding a "care set", the method `omega.symbolic.fol.Context.to_expr` takes a care set (as BDD) as optional argument. – 0 _ Nov 01 '21 at 22:13
  • @loannis Filippidis Sorry. I wasn't able to explain properly. By "A= XX00 to B=XX11", I meant all possible ways to go from state "A=XX00" to "B=XX11". ${XX}={00, 01, 10, 11}$. So, $A={0000, 0100, 1000, 1100}$ and $B={0011, 0111, 1011, 1111}$. Finally, as there are 4 unique candidates of A, and B, there are 16 possible ways $A \rightarrow B$ can happen, e.g., $0000 \rightarrow 0011, 0000 \rightarrow 0111$,....$1100 \rightarrow 1111$. –  Nov 02 '21 at 16:49
  • Another example can be A={X001} to B={X11X}. There are 8 possible ways, e.g., 0001 ->0110, 0001 ->0111... ... 1001->1111. Please let me know if dd package can handle examples like this. –  Nov 02 '21 at 23:25
  • Hi, I got a question, after constructing my BDD, how can I test an expression whether its true or not?. I used bdd.exists(test_expr, root_node) ==bdd.true, however the function return always true, not a single false which is odd. – hatahetahmad Nov 26 '22 at 18:36