After you found the formula in RMNF (c&b) xor (a&c) xor (c) xor (b) xor true that is represented by the FDD, you want to construct the ZDD. To this end, you perform repeated Shannon decompositions as far as I can see. Shannon decomposition on c yields the following two
- (false&b) xor (a& false) xor (false) xor (b) xor true which is b xor true
- (true&b) xor (a& true) xor (true) xor (b) xor true = b xor a xor true xor b xor true = a
The ZDD for not b is however the one that you can see as the low ZDD of the following correct solution (it shows the desired ZDD), i.e., it is supressing the negation of b (which ZDDs do) but has to make a redundant case distinction on the other variable a.