Binary Decision Diagrams are the state of the art data structures for boolean functions manipulation. They are particularly used in VLSI design, symbolic model checking of digital circuits, in analysis of sequential systems, as well as in many other problems. Due to their strong dependence in size upon the chosen variable order, one of the most important problem in the use of the Binary Decision Diagrams is to construct good orders to minimize (i.e. optimize) their size. This paper presents recent advances in using lower bounds in Binary Decision Diagrams Optimization.
