MiniZinc 中的通道是什么？你能提供一个简单的例子来解释通灵吗？最后，什么是逆？

Question

MiniZinc 中的通道是什么？你能提供一个简单的例子来解释通灵吗？最后，什么是逆？

Answer 1

两者都用于在两个数组之间建立双向关系。

让f成为一个index_set(f)等于1..10和 值的数组81..90。然后f可以看作是一个映射——也就是一个函数——从值1..10集到值集81..90。

逆.

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

此约束说，如果f是映射的索引的函数i的值j，然后invf是映射的索引的函数j的值i（反之亦然）。换句话说，数组invf以 in 中的值进行索引，f并生成 中f包含的每个值的位置in f。

int_set_channel。

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

约束表示如果x是一个将索引映射i到给定 set的函数j，则该值i包含在 index jin处的集合中y（反之亦然）。这与逆约束完全相同，只是它y是一组集合而不是一组值。

根据我的经验，转换约束对于从一个问题视图移动到另一个问题很有用，以便以最自然和最有效的方式表达其他约束。这种类型的约束可以使用上述的全局约束，或者使用基本的语言结构来表达。参见，例如，carseq.mzn。

有关更多有用信息和具体示例，请参阅文档的第 2.6.6.1 节。

示例：

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]

在这里，通道约束将模型中包含的n-queens问题的两个视图联系起来。第一个视图q是一维的，并告诉每列中皇后的行位置。第二个视图qb是二维的，它告诉棋盘的哪一块棋盘被某个皇后占据。第一个视图非常适合解决问题的放置部分。第二个视图非常适合应用对称破坏约束。