Also, the algorithms around using Reduced Order Binary Decision Diagrams (ROBDD) to represent sets efficiently. They are used in verification algorithms with ve

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/Papers/SMC.pdf http://www.cse.chalmers.se/edu/year/2012/course/TDA956/Paper...>