Efficiently create structured binary decision diagram

Question

I'm trying to create a BDD with a particular structure. I have a 1D sequence of boolean variables x_i, e.g. x_1, x_2, x_3, x_4, x_5. My condition is satisfied if there are no isolated ones or zeros (except possibly at the edges).

I have implemented this using pyeda as follows. The condition is equivalent to examining consecutive triples ([x_1, x_2, x_3]; [x_2, x_3, x_4]; ...) and checking that their truth values are one of [[1,1,1], [0,0,0], [1,1,0], [0,1,1], [1,0,0], [0,0,1]].

from functools import reduce
from pyeda.inter import bddvars

def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1,1,1], [0,0,0], [1,1,0], [0,1,1], [1,0,0], [0,0,1]]
    truths = [[farr[i] if p[i] else ~farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])

X = bddvars('x', k)
Xc = [X[i-1:i+2] for i in range(1,k-1)]
cont_constraints = [possible_3_grams(c) for c in Xc]
cont_constr = reduce(lambda x, y: x & y, cont_constraints)
print(cont_constr.to_dot())

The final diagram looks like this:

This works well for short sequences, but the last reduction becomes extremely slow when the length gets beyond about 25. I would like something that works for much longer sequences.

I wondered if it would be more efficient in this case to build the BDD directly, since the problem has a lot of structure. However, I can't find any way to directly manipulate BDDs in pyeda.

Does anyone know how I can get this working more efficiently?

Answer 1

This example can be solved for large numbers of variables using the package dd, which can be installed with

pip install dd

For example,

from functools import reduce

from dd.autoref import BDD


def possible_3_grams(farr):
    farr = list(farr)
    poss = [[1, 1, 1], [0, 0, 0], [1, 1, 0], [0, 1, 1], [1, 0, 0], [0, 0, 1]]
    truths = [[farr[i] if p[i] else ~ farr[i] for i in range(3)] for p in poss]
    return reduce(lambda x, y: x | y, [reduce(lambda x, y: x & y, t) for t in truths])


def main():
    k = 100
    xvars = [f'x{i}' for i in range(k)]
    bdd = BDD()
    bdd.declare(*xvars)
    X = [bdd.add_expr(x) for x in xvars]
    Xc = [X[i-1:i+2] for i in range(1, k-1)]
    cont_constraints = [possible_3_grams(c) for c in Xc]
    cont_constr = reduce(lambda x, y: x & y, cont_constraints)
    print(cont_constr)
    bdd.dump('example.png', [cont_constr])

The above uses the pure Python implementation of BDDs in the module dd.autoref. There is a Cython implementation available in the module dd.cudd that interfaces to the CUDD library in C. This implementation can be used by replacing the import statement

from dd.autoref import BDD

with the statement

from dd.cudd import BDD

The above script using the class dd.autoref.BDD works for k = 800 (with the bdd.dump statement commented). The above script using the class dd.cudd.BDD works for k = 10000, provided dynamic reordering is first disabled bdd.configure(reordering=False), and constructs a BDD with 39992 nodes (with the bdd.dump statement commented).

The diagram for k = 100 is the following:

If two-level logic minimization is also of interest, it is implemented in the package omega, an example can be found at: https://github.com/tulip-control/omega/blob/master/examples/minimal_formula_from_bdd.py