Feature request: associating constraints with arrays

[dan1221]

Many combinatorial objects involve an array with one or more associated constraints. For example, a permutation can be represented as a one-dimensional array with an alldifferent constraint, and a latin square can be represented as a two-dimensional square array with each row and column being a permutation. But MiniZinc apparently doesn't have a way to define a permutation such that later variables can be defined as permutations, perhaps adding additional constraints if applicable.

[Dekker1]

I'm not sure what you mean. Can you give an example of what you would want to be able to do?

[dan1221]

I think MiniZinc is missing the notion of user-defined types that incorporate a data structure such as an array, and one or more constraints. For example, a permutation type that incorporates a one-dimensional array and an alldifferent constraint. Once you've defined a permutation type, you should be able to declare variables of that type, without repeating that the permutation type includes an array. You should also be able to declare a new type that is an array of permutations, again without repeating anything about the permutation being based on an array. You should be able to declare a new type that is a restricted permutation, such as an involution or derangement, and then use that new type to declare variables, etc.

You should be able to use any such type to generate and/or count all instances that satisfy the constraints. And you should be able to generate and/or count instances of a type regardless of whether it was declared in a global scope or not.

Instead, we have the notion of an alldifferent predicate. But you can't declare a variable to be of type alldifferent, because alldifferent isn't a type, and alldifferent doesn't inherit the property of being an array. Instead you have to declare a permutation variable to be an array type and then apply the alldifferent predicate. Then if you want to declare an involution type, you can't declare it to be a permutation type with the added constraint that it equals its inverse.

[zayenz]

Note: the below comment is wrong, see the follow-up by @Dekker1.

~~You can do some things with functions to get a library of pre-defined types. It is not a full type-system with associated constraints, but it might be enough for some use-cases.~~

~~For example, the following declares a function permutation that creates an array that models a permutation of a supplied size (with the caveat that I'm not sure about the generics).~~

include "globals.mzn";

int: n = 6;
set of int: Domain = 1..n;

function array[$$X] of var $$X: permutation(set of $$X: size) =
    let {
        array[size of var size result;
        constraint all_different(result);
    } in
    result;
    
array[Domain] of var Domain: x = permutation(Domain);

solve satisfy;

output [show(x)];

[Dekker1]

I think having something like "constructors" is an interesting notion. I think the function that @zayenz wrote expresses how I would see these constructors working.

However, currently this function does not yet work because of the common sub-expression elimination in MiniZinc. When you define another permutation y:

array[Domain] of var Domain: y = permutation(Domain);

MiniZinc will return the exact same result array (because the arguments of the function are the same), and x and y will always take the same values.

We need a minor extension to the language to make something like this work. However, I'm not sure how common the need is some these constructors. You would already always be able to write the constraints that you would post on your variables as an additional predicate, so constructors would not reduce the "code size" of the models much (although I love that they are more expressive), and I'm wondering how many of these data+constraint variants are used dynamically enough to make them worth an extra language feature. Maybe the introduction of tuples and records will make this more worthwhile, but I still need to see some more examples to be convinced.

[guidotack]

This is a feature that is (was) available in the full Zinc language in a restricted form, which supports constrained types like this:

type NonNegFloat = (float: x where x >= 0);

To be fully flexible, this would have to be extended to allow for type-inst variables (i.e., generic user defined types), e.g. like this (just mocking up some syntax, not sure this is the best way to do it):

type permutation of $A = array[$A] of var $A: x where all_different(x);

That would allow you to write e.g.

permutation of 1..3: x;

This could be an interesting addition to the language, we'll have to think about whether that's something that could be added.

[zayenz]

@Dekker1 Interesting, I would intuitively have expected that the function-approach would work. Thanks for the information. I would not have expected that a variable that is returned from a function would be a candidate for CSE, but I can see that it would. I think that the discussion at the end of the local variables description in the documentation could be improved to warn about this more clearly. For me it "feels" like the function I wrote is functionally defined, but when you point it out I realize it isn't.

I think that a way to encode such sub-models would be useful, and for example an annotation of some sort that would enable this could be interesting. Especially with records and tuples, as the returned information could have more structure than a homogeneous array.