What is Channeling in MiniZinc? Can you provide an simple example to explain Channeling? Finally, What is Inverse?

Solution

Both are used to establish a bidirectional relationship between two arrays.

Let f be an array with index_set(f) equal to 1..10 and values in 81..90. Then f can be seen as a mapping --a.k.a. a function-- from the set of values 1..10 to the set of values 81..90.

Inverse.

predicate inverse(array [int] of var int: f,
                  array [int] of var int: invf)

This constraint says that if f is a function mapping an index i to a value j, then invf is a function mapping an index j to a value i (and vice-versa). In other words, the array invf is indexed with the values in f and it yields the position in f of the each value contained in f.

int_set_channel.

predicate int_set_channel(array [int] of var int: x,
                          array [int] of var set of int: y)

The constraint says that if x is a function mapping an index i to a given set j, then the value i is contained in the set at index j in y (and vice-versa). This is the exact same thing as the inverse constraint, only that y is an array of sets rather than an array of values.

In my experience, chanelling constraints are useful to move from one problem view to another, so as to express other constraints in the most natural --and efficient-- way. This type of constraints may use the global constraints described above, or expressed using basic language constructs. See, for instance, carseq.mzn.

For more useful information and a concrete example, see Section 2.6.6.1 of the docs.

Example:

int: n;
array [1..n] of var 1..n: q; % queen is column i is in row q[i]

include "alldifferent.mzn";

constraint alldifferent(q);                       % distinct rows
constraint alldifferent([ q[i] + i | i in 1..n]); % distinct diagonals
constraint alldifferent([ q[i] - i | i in 1..n]); % upwards+downwards

include "lex_lesseq.mzn";

% Alternative Boolean model:
% Map each position i,j to a Boolean telling us whether there is a queen at i,j
array[1..n,1..n] of var bool: qb;

% Channeling constraint
constraint forall (i,j in 1..n) ( qb[i,j] <-> (q[i]=j) );

% Lexicographic symmetry breaking constraints
constraint
    lex_lesseq(array1d(qb), [ qb[j,i] | i,j in 1..n ])
/\  lex_lesseq(array1d(qb), [ qb[i,j] | i in reverse(1..n), j in 1..n ])
/\  lex_lesseq(array1d(qb), [ qb[j,i] | i in 1..n, j in reverse(1..n) ])
/\  lex_lesseq(array1d(qb), [ qb[i,j] | i in 1..n, j in reverse(1..n) ])
/\  lex_lesseq(array1d(qb), [ qb[j,i] | i in reverse(1..n), j in 1..n ])
/\  lex_lesseq(array1d(qb), [ qb[i,j] | i,j in reverse(1..n) ])
/\  lex_lesseq(array1d(qb), [ qb[j,i] | i,j in reverse(1..n) ])
;

% search
solve :: int_search(q, first_fail, indomain_min)
      satisfy;
output [ if fix(q[j]) == i then "Q" else "." endif ++
         if j == n then "\n" else "" endif | i,j in 1..n]

Here, the channeling constraints put in relation the two views of the n-queens problem contained in the model. The first view q is uni-dimensional, and tells the row position of the queen within each column. The second view qb is bi-dimensional, and tells which tile of the chessboard is occupied by some queen. The first view is great for solving the placement part of the problem. the second view is great for applying symmetry breaking constraints.