First of all, <-> is associative, so that it does not matter for its semantics how we parse a sequence of this operator. According to the lecture, we defined this operator however as being left associative, so that we get the following expression with full use of brackets:
((((a&d)<->b)<->c)|((a<->a)&!b))<->!(c<->(a->a))
A CNF obtained by the BDD of this formula is for instance the following one:
(!a|!b|!d) & (b|!c)
Before starting any computation, we first simplify the formula by replacing a<->a with true and propagating the boolean constants so that we get
((((a&d)<->b)<->c)|!b)<->!c
Next, we make a Shannon decomposition: Starting with variable b (it has two occurrences and thus more than variable a), we get the following cofactors:
- b=0: !c
- b=1: (a&d<->c)<->!c
Thus, our formula is equivalent to (b -> (a&d<->c)<->!c) & (!b -> !c) which yields
(!b | ((a&d<->c)<->!c)) & (b|!c)
It remains to convert (a&d<->c)<->!c) to a CNF, so we make a Shannon decomposition with c:
That makes it simple, since the formula (a&d<->c)<->!c) is equivalent to !(a&d). Hence, we get the following formula:
(!b | !(a&d)) & (b|!c)
which has the following CNF:
(!b|!a|!d) & (b|!c)
