Also, the algorithms around using Reduced Order Binary Decision Diagrams (ROBDD) to represent sets efficiently. They are used in verification algorithms with very large state spaces, such as "Symbolic Model Checking: 10^20 states and beyond" by Burch, Clarke, and McMillan <http://www.cse.chalmers.se/edu/year/2012/course/TDA956/Paper...>