alt Hacker NewsYou are right, poor phrasing on my side. Instead of focusing on C appearing twice, I should rather focus on how complex the expansion is, meaning that everytime we have to expand the BDD (which we need to do during subtyping or emptiness for example), we end-up doing a lot of repeated operations. I will push an update, thank you for commenting.
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!