Alldifferent and optional types

[Ties Westendorp]

I'm considering building a model and gathering instances from real life data for this years MiniZinc challenge, but I'm a bit disheartened in doing so after an attempt at refactoring a previous model I made by using option types in combination with global constraints.

Using option types seems like the way to go over constructing this pattern yourself using dummy values, but it just doesn't play nicely with predicates like `alldifferent`. I've tried several ways to circumvent the issue (using `deopt` and `... where occurs(..)`), but it just doesn't seem possible; using `deopt` necessitates an `occurs` check in my list comprehension, but adding `occurs` seems to change the return type to `array[int] of var opt int` despite the `deopt` call...

I've found an old GH issue (https://github.com/MiniZinc/libminizinc/issues/56) about this exact issue, but that dates back to 2015 and was closed in 2019 with the remark: just don't use option types - which is not a very satisfying answer in my opinion. Is there any progress on this/is this still a feature that's on the roadmap?

[Ties Westendorp]

I should add that I'm currently using the very hacky looking: `alldifferent_except_0([ 0+A[i] | i in B ])` (variable names minimized) to achieve what I need. Adding 0 to the option type ensures that <> maps to 0, and other values remain the same.

[Jip J. Dekker]

Hi Ties,

Since the issue that you link to was closed, there has been a big push to improve the support for "opt" type, and the quality of the solver models that these variables generate. Many globals now do have support for "opt" variables. This includes the "all_different" constraint as documented: https://www.minizinc.org/doc-2.6.1/en/lib-globals-alldifferent.html#mzn-ref-globals-alldifferent-all-different

The problem you might be having is that you use the older "alldifferent" call, which seems to have not been updated. (This name should probably be deprecated as it does not match the naming conventions, but some find it hard to let go).

As a comment, although your solution might look "hacky", this is essentially how the standard decomposition of all_different for optional integer variables works: https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fzn_all_different_int_opt.mzn (Note that we have to be a bit careful with optional variables where 0 appears in the domain).

Cheers,

Jip

[Jip J. Dekker]

Just a note that even using the name "alldifferent" should work if you are using the current version of MiniZinc: https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/all_different.mzn

[Mikael Zayenz Lagerkvist]

On Fri, Mar 25, 2022 at 12:36 AM Jip J. Dekker <j...@dekker.li> wrote:
> Since the issue that you link to was closed, there has been a big push to improve the support for "opt" type, and the quality of the solver models that these variables generate. Many globals now do have support for "opt" variables. This includes the "all_different" constraint as documented: https://www.minizinc.org/doc-2.6.1/en/lib-globals-alldifferent.html#mzn-ref-globals-alldifferent-all-different

As a note, when I saw the question by Tias yesterday, I briefly looked
at the documentation for all_different. I had assumed that there would
be a version that accepted optional variables, but my reading of the
documentation led me astray. The text

"Constrain the elements in the array x to be pairwise different or absent."

reads to me as if only one absent value is allowed (which I found an
odd constraint to have, but did not question). It might not be the
right reading of the text, but I think it might be a good idea to
expand it a bit further to clarify that multiple absent values are
allowed.

On a related note, I was surprised to find that the all_different
family does not support variables with enumerated values, just var int
variables. I would have thought that both all_different (with and
without optionality) and all_different_except would have enum-handling
versions.

Cheers,
Mikael

--
Mikael Zayenz Lagerkvist

[Ties Westendorp]

I tried using all_different first, but got all sorts of errors. I'm probably using an outdated version of MiniZinc, though I haven't installed very long ago.. Every Google search result leads with the documentation of version 2.5.3, while 2.6.0 already exists apparently, this was probably the source of my confusion. *facepalm*

[Ties Westendorp]

Just updated, this fixed the issue I was having with all_different. I still have one other issue with regards to opt types, though. The following snippet ought to work, but doesn't:

`list of var A: foo = [ a | a in B where bar[a] = 1]`

Because `bar` is of type `list of var opt ...` the type of `foo` becomes `list of var opt A` rather than the declared type. How can I coerce it? I would expect that using an opt type variable in a comparison like this would be fine, furthermore, replacing the check by `occurs(bar[a])` doesn't fix the error either. I'm a bit at a loss on how to solve this issue.

[guido.tack]

Hi,

Any array with a variable `where` clause has an option type in MiniZinc. The reason is that MiniZinc does not support arrays of variable size (i.e., where the solver has to determine the size of the array as a decision variable). So in your example above, the type of the array has to be `list of var opt A`. The problem isn't so much that `bar` has an option type, it's that it has a `var` type.

Perhaps let us know how you want to use `foo`, and why it's a problem if `foo` has type `var opt A`.

Cheers,

Guido

[guido.tack]

Hi Mikael,

good point, we should make the documentation for all_different a bit less ambiguous.

The all_different family of constraints does support enumerated types, since those simply automatically coerce to `int`. We could define the predicates using `$$E` instead of `int` as the types, but the behaviour would be the same and it would not introduce any additional type safety. That's not true for `all_different_except`, though, where we could enforce that the array and the set have the same enum type. I'll have to check whether that leads to any issues with backwards compatibility.

Cheers,

Guido

[Ties Westendorp]

Hi Guido, thanks for your response. I can see why using opt types in this case is required by the restrictions of a fixed size array, and I can indeed get the model through the type checker by propagating `opt` through the necessary type signatures, but my model fails to run after these changes. The error I get is: `MiniZinc: evaluation error: internal error: missing builtin 'forall'`. I don't get this error when omitting the `where` clause, and removing all the opt types from the function calls, and I'm unsure why this error is occurring - the error message isn't really descriptive. I'm not sure if I can distill a MWE from my model, but if you want to have a look, I can share the two versions of the model (with and without the opt types).