I made a video about bex, a crate for working with and solving giant boolean expressions (and also an ongoing exercise in optimization).
Fair warning: this is mostly a math video, so I don't really dive into the rust code, and most of the exposition is done through a different math-centric programming language called J.
Anyway, here it is!