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.
My current interpretation of
o IN { l1; l2; l3 }isassign(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 foro.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 allidifferent from 1, 2, and 3.