Improve Bdd export to BooleanExpression

[daemontus]

Currently, export to BooleanExpression from Bdd is a trivial graph traversal algorithm. There is a lot of extra techniques that can improve this algorithm:

• If we know all valid paths have x set to true, we can start the formula with x & ... and later skip x completely (this can be also done for each smaller Bdd in each expansion step). Technically, we are looking for a variable ordering that minimises the number of nodes in this specific Bdd.
• We can try to find implication/equivalence pairs. That is, if a <=> b on all paths, we can put this as a condition at the beginning and then skip b completely.