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?