Minizinc Symmetry Declarations
We propose 6 symmetry predicates for MiniZinc defined below. The default decompositions are linked to the predicate names.

predicate var_sym(array[int] of var int: x);
 Requires: All variables in x are distinct.
 Means: Every
variable in the set x is interchangeable, i.e., for any i, j, if we swap
the values of x[i] and x[j], then solutions are preserved.

predicate val_sym(array[int] of var int: x, array[int] of int: s);
 Requires: All variables in x are distinct. All values in s are
distinct.
 Means: We can interchange any pair of values in s over
all the variables in x, i.e., for any i, j, if we take every x[k]
which was set to s[i] and change it to s[j] and take every x[k] which
was set to s[j] and change it to s[i], then solutions are preserved.
 predicate var_seq_sym(array[int,int] of var int: x);
 Requires: All variables in x are distinct.
 Means: We can interchange any pair of variable
sequences in x, i.e., for any i, j, if for every k, we swap x[i,k] with x[j,k], then solutions are preserved.
 predicate val_seq_sym(array[int] of var int: x, array[int,int] of int: s);
 Requires: All variables in x are distinct. All values in s are
distinct.
 Means: We can interchange any pair of value sequences in
x, i.e., for any i, j, if for every m, we take every x[k] which was
set to s[i,m] and change it to s[j,m] and take every x[k] which was
set to s[j,m] and change it to s[i,m], then solutions are preserved.
 predicate var_perm_sym(array[int] of var int:x, array[int,int] of int: p);
 Requires: All variables in x are distinct. Each row of p is a permutation of the integers 1 .. length(x) and the ith row represents the variable sequence [x[p[i,k]]  k in 1..length(x)].
 Means: We can map any variable sequence represented in p to another variable sequence represented in p, i.e., for any i, j, if for every k, we take x[p[i,k]] and set it to the value of x[p[j,k]], then solutions are preserved.
 predicate val_perm_sym(array[int] of var int: x, array[int,int] of int: s);
 Requires: All variables in x are distinct. Each row of s covers the same set of values.
 Means: We can map any value sequence in s to another value sequence in s, i.e., for any i, j, if we take every x[k] which was set to s[i,m] and change its value to s[j,m], then solutions are preserved.
For handling multiple symmetry declarations correctly we need to extend the declarations to take into account a global variable order order as follows:

predicate var_sym_ord(array[int] of var int: x,
array[int] of ver int: order);

predicate val_sym_ord(array[int] of var int: x, array[int] of int: s, array[int] of ver int: order);
 predicate var_seq_sym_ord(array[int,int] of var int: x, array[int] of ver int: order);
 predicate val_seq_sym_ord(array[int] of var int: x, array[int,int] of int: s, array[int] of ver int: order);
 predicate var_perm_sym_ord(array[int] of var int:x, array[int,int] of int: p, array[int] of ver int: order);
 predicate val_perm_sym_ord(array[int] of var int: x, array[int,int] of int: s, array[int] of ver int: order);
The benchmarks used in the paper
Symmetries for MiniZinc are given here: