[BUG] Set constraint setLe and setLt do not behave as expected
#936
Comments
dimitri-justeau
changed the title
setLe and setLt do not behave as expectedsetLe and setLt do not behave as expected
|
You are right, I've missed that when I added the decomposition. IntIterableRangeSet union = new IntIterableRangeSet();
for (int v : a.getUB()) {
union.add(v);
}
for (int v : b.getUB()) {
union.add(v);
}
return ref().lexLess(ref().setBoolsView(a, union.size(), union.min()), ref().setBoolsView(b, union.size(), union.min()));a possible correction could be: IntIterableRangeSet union = new IntIterableRangeSet();
for (int v : a.getUB()) {
union.add(v);
}
for (int v : b.getUB()) {
union.add(v);
}
int offset = union.min();
int size = union.size();
BoolVar[] boolA = new BoolVar[size];
BoolVar[] boolB = new BoolVar[size];
for (int i = 0; i < size; i++) {
boolA[size - i - 1] = ref().setBoolView(a, i + offset);
boolB[size - i - 1] = ref().setBoolView(b, i + offset);
}
return ref().lexLess(boolA, boolB);When evaluated on instead of : For comparison: Chuffed: which indicates that some improvements may be done on this decomposition (but also |
|
This is not correct. It accepts 11 solutions: without the correction only 4 of them are found. With the correction, the following solution is missing: Indeed, turned into Boolean variables, the variables are, resp. |
|
You are right, at first glance, I would say that the problem can only happen when there is a "trailing" zero (as it is the only neutral lexicographic element, and as there can be only one zero in a set). The first idea that comes to me now would be omitting the zero from the Boolean representation, do you think it would be correct? |
|
Huum, actually this might also be an issue with the definition of lexicographic order over sets with different cardinalities. There is no ambiguity when the sets have the same cardinality, however when the cardinality is not the same, we can either:
I think that we want the third option, BUT it remains to be clear whether zero is a neutral element or not. Thinking twice, is many cases I would not want the solver to tell me that {0, 1} <= {1}, e.g. if the values of the set depict indices of a cost array. We could also offer different options, to have either a shortlex, a lex, a colex, with or without zero as a neutral element. EDIT: to summarize, I think that MiniZinc is not correct either, or not clear enough about the ordering definition. |
|
Thank you for the insights. |
|
Yep, I think it would definitely be worth it! Do you want me to do it and tag you, or the opposite ? |
|
If you have time to do it now, I'll do it. If not, I'll do it on Thursday |
|
Okay I'm doing it right now ! |
|
Okay, so I was wrong, MiniZinc effectively uses a lexicographic order with trailing zeros at the right, this is why: {0, 1} < {1} is equivalent to 010 < 100 So yep, we need to fix this in Choco, and I do not know what is your opinion on this, but I feel like this lexicographic ordering for sets is not suited for some combinatorial uses of sets. It feels suited when the sorted elements of a set form a word, but I feel like the colexicographic and shortlex could be more suited for some usages. |
|
I don't see why trailing zeros are needed. So, a reverse argmax on the bits could do the job: right? EDIT: that does not work for empty set though |
|
Yes, actually it is not trivial with what is currently available in Choco. Ideally, we could have a channelling constraint (or views) that links a set variable and an array of integers such that the array of integers represents the sorted elements of the set variable. |
|
Here is the decomposition defined in We must compare this decomposition with a one based on views/channeling constraints (and ad hoc prop?). |
|
I just coded and tested a quick channelling constraint, I will try it with your test to see if it solves the problem. |
|
Okay I proposed a PR here: #954 |
|
I integrated your work (with some modifications) in #952 (could you please approve the modifications)? I tested back on Thank you for the fix !
|
|
Nice !! I also think that the new channelling constraint can be useful in some other situations :-) Yes, I thought about doing the reverse filtering too, I guessed that we might be able to filter a bit more that way, but as this was not really useful for First I wanted to do it with views, but actually, an array of views would have been a bit complicated and would involve a lot of events so I think channelling was a better and simpler option. |
Describe the bug
The lexicographic ordering is applied to a boolean representation of the set, in the form: [b0, b1, b2, b3], where b0 is the lexicographically smallest possible number in the set (from UB) and b3 is the largest. For example, if we have a set variable s that takes its values in [ {}, {0, 1, 2, 3, 4} ], the value {1, 2} is represented as 01100.
The problem is that the lexical ordering of this representation is not equivalent to the lexicographic ordering of the sorted set elements. For example (with the same domain [ {}, {0, 1, 2, 3, 4} ]), if s1 = {4} and s2 = {3}, s1 > s2 according to the lexicographic ordering of the sorted set elements. But with the boolean representation we have: s1 = 00001 and s2 = 00010, thus s1 < s2.
Possible solution
One possible solution could be to reverse the boolean representation, with the previous example we would have:
s1 = {4} -> 10000
s2 = {3} -> 01000
The text was updated successfully, but these errors were encountered: