Kudos on the article! My understanding on BDDs is sadly not as strong as I would prefer it to be, so I'm guessing I am not quite caught up on how they are being used here.

I think I was expecting to see the algorithm for merging multiple BDDs that I saw in Knuth's work. Though, in that regard, I would expect a ZDD approach would be a lot easier to start with. That or you would have to make the BDD to merge be a big chain of every variable before the stuff to be merged where true goes to BOTTOM, and false goes to the next variable before new first to merge.

Again, kudos on this. I do look forward to trying to understand it more!