Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

How to directly manipulate binary decision diagrams? #162

Open
RPrudden opened this issue Jan 9, 2021 · 0 comments
Open

How to directly manipulate binary decision diagrams? #162

RPrudden opened this issue Jan 9, 2021 · 0 comments

Comments

@RPrudden
Copy link

RPrudden commented Jan 9, 2021

I am trying to generate BDDs with a very predictable structure. I have a method that works for very small problems, but is too expensive to generate the BDD for even a modest number of variables. Because there is so much structure, I suspect it should be possible to do this more efficiently by manipulating the BDD directly, but I haven't been able to find a way to do this. Any guidance would be much appreciated!

Details

I have a 1D sequence of boolean variables x_i, e.g. [x_1, x_2, x_3, x_4, x_5], and I want to constrain it so that there are no isolated ones or zeros (except possibly at the edges).

I have implemented this in pyeda by 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]].

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)

If there are just five variables, the BDD looks like this
image

This works fine for five or so variables, but beyond about 25 variables generating the BDD is too expensive. I'm looking for an approach that can scale to larger problems.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant