# 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: The benchmarks used in the paper Symmetries for MiniZinc are given here: