Binary Decision Diagrams (Bdds)

Binary Decision Diagrams (BDDs): Binary Decision Diagrams (BDDs) are bit-serial DFA for satisfying instances of Boolean formulas.5 To better understand this characterization, consider the finite language
L1 = {abcd | d ∨ (a ∧ b ∧ c)}.
Since all finite languages (a finite number of finite strings in this case) are regular, a regular expression describing this language can be obtained by spelling out all the satisfying instances of d∨(a∧b∧c). This finite regular language is denoted by the following regular expression:
(1110 1111 0001 0011 0101 0111 1001 1011 1101)
By putting this regular expression in a file called a.b.c d, we can use the following grail command sequence to obtain a minimal DFA for it, as shown in Figure 11.1(a):

cat a.b.c d | retofm | fmdeterm | fmmin | perl grail2ps.perl -> a.b.c d.ps
Now consider the language that merely changes the bit-serial order in which the variables are examined from abcd to dabc:
L2 = {dabc | d ∨ (a ∧ b ∧ c)}.
Using the regular expression
(0111 1000 1001 1010 1011 1100 1101 1110 1111)
as before, we obtain the minimal DFA shown in Figure 11.1(b). The two minimal DFAs seem to be of the same size. Should we expect this in general? The minimal DFAs in Figure 11.1 and Figure 11.2, are suboptimal as far as their role in decoding the binary decision goes, as they contain redundant decodings. For instance, in Figure 11.1(a),

after abc = 111 has been seen, there is no need to decode d; however, this diagram redundantly considers 0 and 1 both going to the accepting state 0. In Figure 11.1(b), we can make node 6 point directly to node 0. Eliminating such redundant decodings, Figures 11.1(a) and (b) will, essentially, become BDDs; the only difference from a BDD at that point would be that BDDs explicitly include a 0 node to which all falsifying assignments lead to. Let us now experiment with the following two languages where we shall discuss these issues even more, and actually present the drawing of a BDD.
Linterleaved = {abcdef | a = b ∧ c = d ∧ e = f}
has a regular expression of satisfying assignments
(000000 001100 000011 110000 001111 110011 111100 111111)
and
Lnoninterleaved = {acebdf | a = b ∧ c = d ∧ e = f}