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
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.
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]].
If there are just five variables, the BDD looks like this
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.