MiniZinc - Constraint to enforce two arrays be equal

Question

I'm trying to model a satisfaction problem with MiniZinc but I'm stuck at coding this constraint:

Given two arrays A and B of equal length, enforce that A is a permutation of B

In other words, I'm looking for a constraint that enforces [1,2,2]=[1,2,2] and also [1,2,2]=[2,2,1]. Informally, A and B have to be equal. The arrays are both defined on the same set of integers, in particular the set 1..n-1, for some n. Values in both A and B can be repeated (see example).

Is there such a global constraint in MiniZinc? Thank you.

Answer 1

In addition to the predicate shown by hakank, here are two other ways to express the same predicate

include "globals.mzn";

%
% Ensure that a and b are perumutations of each other by 
% counting the number of occurences of each value in the 
% domains of a and b, 
%
predicate permutation_count(array[int] of var int: a,
                            array[int] of var int: b) =
    let {
        set of int: I = index_set(a),
        constraint assert(I = index_set(b), "Index sets of a and b must match"),
        set of int: domain = dom_array(a) intersect dom_array(b),
        set of int: NValues = 1..card(domain),
        array[NValues] of int: values = [ v | v in domain ],
        array[NValues] of var 0..card(I): counts,
    } in
    global_cardinality_closed(a, values, counts) /\
    global_cardinality_closed(b, values, counts);

%
% Ensure that a and b are permutations of each other by
% sorting each and constraining that to be the same.
% 
predicate permutation_sort(array[int] of var int: a,
                           array[int] of var int: b) =
    let {
        set of int: I = index_set(a),
        constraint assert(I = index_set(b), "Index sets of a and b must match"),
        set of int: domain = dom_array(a) intersect dom_array(b),
        array[I] of var domain: sorted_values,
    } in
    sorted_values = sort(a) /\
    sorted_values = sort(b);

int: n = 3;

array[1..n] of var 1..2: x;
array[1..n] of var 1..2: y;

constraint permutation_count(x, y);

solve satisfy;

The first one counts the values in both input arrays, since in permutations the counts must be the same. The second variant uses the sorting constraint to sort both a and b to check that they are the same.

Which variant works best can vary between solvers, problems, and problem isntances. The counting solution may be problematic if the domains of the inputs are large, which is worth remembering.

Answer 2

Here is the predicate I tend to use for these cases. It requires an extra array (p) which contains the permutations from array a to array b.

/*
  Enforce that a is a permutation of b with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

A simple model using this:

include "globals.mzn"; 

int: n = 3;

array[1..n] of var 1..2: x;
array[1..n] of var 1..2: y;
array[1..n] of var 1..n: p;

/*
  Enforce that array b is a permutation of array a with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

                   
solve satisfy;

constraint
  x = [2,2,1] /\
  permutation3(x,p,y)
;

output [
  "x: \(x)\ny: \(y)\np: \(p)\n"
];

Output:

x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 2, 1]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [2, 3, 1]
----------
x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 1, 2]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [1, 3, 2]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [2, 1, 3]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [1, 2, 3]
----------
==========

There is an alternative formulation of this which don't requires the extra permutation p (it's defined inside the predicate):

predicate permutation3b(array[int] of var int: a,
                       array[int] of var int: b) =
  let {
    array[index_set(a)] of var index_set(a): p;
  } in
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

For the same problem, this will only output these 3 different solutions (the first model has more solutions since the the permutations differs).

x: [2, 2, 1]
y: [2, 2, 1]

----------
x: [2, 2, 1]
y: [2, 1, 2]

----------
x: [2, 2, 1]
y: [1, 2, 2]

----------
==========

Personally I tend to use the first version since I tend to want to output the permutation and like to have control over the variables.