Minimality

In order to show (at some point) that our algorithm returns a minimal solution we come up with the following definition of minimality.

A solution is minimal if there is no other solution with a smaller number of leafs. Within the set of solutions of the same number of leafs the minimal solution is the one with the smallest number of dimensions.

From this definition one theorem emerged:

Min(#leafs) ∧ Min(#dims) ⇒ Min(#choices)

Sketch for a proof

By PBC.

¬(Min(#leafs) ∧ Min(#dims) ⇒ Min(#choices)) = Min(#leafs) ∧ Min(#dims) ∧ ¬Min(#choices)

If #choices is not minimal it can be improved. How this?

1. Deleting a redundant choice (i.e A<A<1,2>,2> = A<1,2>). This leads to a smaller number of leafs and thus a contradiction.
2. Merging multiple choices in a larger one (i.e. A<B<1,2>,3> = C<1,2,3>). This variation preserving operation can only be performed if either

• A and B are not constrained by other usages, or
• A and B are used the same all over and thus this transformation can be applied globally

Both cases of (2) lead to a smaller size of dimensions and thus a contradiction.