Что такое ченнелинг в MiniZinc? Можете ли вы привести простой пример для объяснения ченнелинга? Наконец, что такое обратное? - PullRequest
Новая
       38

Что такое ченнелинг в MiniZinc? Можете ли вы привести простой пример для объяснения ченнелинга? Наконец, что такое обратное?

2 голосов
/ 08 октября 2019

Что такое ченнелинг в MiniZinc? Можете ли вы привести простой пример для объяснения ченнелинга? Наконец, что такое обратное?

1 Ответ

3 голосов
/ 08 октября 2019

Оба используются для установления двунаправленной связи между двумя массивами.

Пусть f будет массивом с index_set(f), равным 1..10 и значениями в 81..90. Тогда f можно рассматривать как отображение - то есть функцию - из набора значений 1..10 в набор значений 81..90.

Inverse. 

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 содержится в наборе по индексу jв 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 является двумерным и показывает, какая плитка на шахматной доске занята какой-то королевой. Первый вид отлично подходит для решения размещения часть проблемы. второй вид отлично подходит для применения ограничений симметрии .

...