SKEDSOFT

has
(000000 010010 001001 100100 011011 101101 110110 111111).
When converted to minimized DFAs, these regular expressions yield Figures 11.2(a) and (b), where the size difference due to the variable orderings is very apparent. The BDD for Figure 11.2(b) created using the BED tool appears in Figure 11.3. The commands used to create this BDD were:
bed> var a c e b d f % declares six variables
bed> let exp4 = (a=b) and (c=d) and (e=f) % defines the desired expn.
bed> upall exp4 % builds the BDD -
bed> view exp4 % displays the BDD
By comparing Figure 11.3 against Figure 11.2(b), one can see how, in general, BDDs eliminate redundant decodings.

BDDs are efficient data structures for representing Boolean functions and computing the reachable states of state transition systems. In these applications, they are very often ‘robust,’ i.e., their sizes remain modest as the computation advances. As many of these state transition systems have well over 2150 states (just to pick a large number!), this task cannot be accomplished in practice by explicitly enumerating the states. However, BDDs can often very easily represent such large state-spaces by capitalizing on an implicit representation of states as described in Section 11.3. However, BDDs can deliver this ‘magic’ only if a “good” variable ordering is chosen.

One also has to be aware of the following realities when it comes to using BDDs:

• The problem of determining an optimal variable ordering is NPcomplete (see Chapter 20 for a definition of NP-completeness). [42]; this means that the best known algorithms for this task run in exponential worst-case time.
• In many problems, as the computation proceeds and new BDDs are built, variable orderings must be recomputed through dynamic variable re ordering algorithms, which are never ideal and add to the overhead.
• For certain functions (e.g., the middle bits of the result of multiplying two N-bit numbers), the BDD is provably exponentially sized, no matter which variable ordering is chosen.

Even so, BDDs find extensive application in representing as well as manipulating state transition systems realized in hardware and software. We now proceed to discuss how BDDs can be used to represent state transition relations and also how to perform reachability analysis.