Not an expert, and not sure how but lazy BDD's fit in specifically, but I thought BDD's are already the gold-standard data structures in most model checkers and assumed they were at the limit of possibilities for performance. Can anyone comment whether that's true, whether it means this kind of implementation is already standard in other programming languages for sets/bools? What about infrastructure with fast set operations like redis?