decide what `full` and `care_bits` mean

`dd` enumeration API

In dd.bdd.BDD.sat_iter and dd.cudd.BDD.sat_iter the meaning is:

if not full, then return assignments as they result from traversing the BDD. Depending on the variable order, this can yield varying results
if full, then:
- if care_bits is None, then return assignments to all the variables of the BDD manager (usually this isn't what we want)
- else assert care_bits \subseteq support

So, full says whether full assignments are desired. care_bits matters only if full is given, and is explicit, in that it specifies exactly over which variables to enumerate.

However, there is little point in providing fewer care_bits than support, because that is guaranteed to raise an AssertionError about missing variables.

In particular, care_bits = set() is useless, because why would you enumerate a non-constant BDD over no variables?

Another point is whether care_bits should be used as an upper or lower bound. Upper bound means "at most these bits". Lower bound means "at least these bits".

Perhaps a more reasonable alternative would be to enumerate over the union support \cup care_bits, and so avoid both checking whether support \subseteq care_bits, as well as the need to raise any exceptions. (We could consider allowing even variables that are not in the symbol table, though that would work only in BDDs, not for variables that take integer values.)

The exception case leaves that case free for a new meaning to be chosen. It may be worth considering letting full=False, care_bits={...} mean that care_bits should be assigned always, and any missing vars in support assigned only along BDD paths that they appear on.

Another problem is that support \subseteq care_bits is checked whenever care_vars is not None. Even when full = False. Consider changing this behavior in dd.

tulip-control / dd