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

Question

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

Answer 1

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

设 f 是一个数组，index_set(f) 等于 1..10 并且值在 81..90 中。然后 f 可以看作是一个映射 --a.k.a.一个函数 -- 从值集 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 以 f 中的值作为索引，它产生 f 中包含的每个值在 中的位置>f.

int_set_channel。

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

约束表示，如果 x 是一个将索引 i 映射到给定集合 j 的函数，那么值 i 包含在 y 中索引 j 的集合中(反之亦然)。这与 inverse 约束完全相同，只是 y 是集合数组而不是值数组。

---

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

有关更多有用信息和具体示例，请参阅 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]

此处， channel 约束 将模型中包含的 n-queens 问题的两个 View 联系起来。第一个 View q 是一维的，并说明皇后在每一列中的行位置。第二个 View qb 是二维的，它告诉我们棋盘上的哪一 block 棋子被某个皇后占据了。第一个 View 非常适合解决问题的放置 部分。第二个 View 非常适合应用对称破坏约束。