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: