The general steps to follow are to recursively apply the Shannon decomposition that will quickly reduce the formula to smaller ones that can then be dealt with as a whole. The example above is however again a case that can be understood at the level of the formula: It says that an even number of variables must be true because of ¬(a XOR b XOR c XOR d), that this number is not zero because of a | b | c | d and that this number is not four because of ¬a | ¬b | ¬c | ¬d. Hence, exactly two of the four variables must be true which again leads to a symmetric BDD with a simple structure.