Don't force all objects to be assigned

[aspiwack]

My current interpretation of o IN { l1; l2; l3 } is assign(o,l1) \/ assign (o,l2) \/ assign(o,l3).

The good part about this is that this makes sure that all the items are assigned to a location (then you can have extra location to fill up with rubbish items).

But I posit that it is probably inefficient: we want the SAT solver to be able to summarise shuffles. That is to provide incomplete shuffles which are nevertheless solvable. So if I already can solve my shuffle without o, I shouldn't need to generate 3 subshuffles for o.

As always (see for instance #12 ), offloading dense shuffles to a simple shuffling algorithm is better (because it is O(n) rather than exponential…).

So instead the interpetation of a range query should be negative. In this case ~assign(o,li) for all i different from 1, 2, and 3.

[aspiwack]

At time of writing, to do that it suffice to remove the at_least clause in the interpretation of range formulas. But the current example is too fast to reliably observe a difference, so I'm keeping the clause around until I have a longer example to observe the effect (it may even be negative, who knows!).