MiniZinc

Question

我正在尝试使用 MiniZinc 模拟满意度问题，但我一直坚持编写此约束：

给定两个长度相等的数组 A 和 B，强制 A 是 B[ 的排列=22=]

换句话说，我正在寻找强制执行 [1,2,2]=[1,2,2] 和 [1,2,2]=[2,2,1] 的约束。非正式地，A 和 B 必须相等。这两个数组都是在同一组整数上定义的，特别是 1..n-1 组，某些 n。 A 和 B 中的值可以重复（参见示例）。

MiniZinc有这样的全局约束吗？谢谢。

Answer 1

这是我倾向于在这些情况下使用的谓词。它需要一个额外的数组 (p)，其中包含从数组 a 到数组 b.

的排列

/*
  Enforce that a is a permutation of b with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

使用这个的简单模型：

include "globals.mzn"; 

int: n = 3;

array[1..n] of var 1..2: x;
array[1..n] of var 1..2: y;
array[1..n] of var 1..n: p;

/*
  Enforce that array b is a permutation of array a with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

                   
solve satisfy;

constraint
  x = [2,2,1] /\
  permutation3(x,p,y)
;

output [
  "x: \(x)\ny: \(y)\np: \(p)\n"
];

输出：

x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 2, 1]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [2, 3, 1]
----------
x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 1, 2]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [1, 3, 2]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [2, 1, 3]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [1, 2, 3]
----------
==========

有一个替代公式不需要额外的排列 p（它在谓词中定义）：

predicate permutation3b(array[int] of var int: a,
                       array[int] of var int: b) =
  let {
    array[index_set(a)] of var index_set(a): p;
  } in
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

对于同一个问题，这只会输出这 3 个不同的解决方案（第一个模型有更多的解决方案，因为排列不同）。

x: [2, 2, 1]
y: [2, 2, 1]

----------
x: [2, 2, 1]
y: [2, 1, 2]

----------
x: [2, 2, 1]
y: [1, 2, 2]

----------
==========

我个人倾向于使用第一个版本，因为我倾向于输出排列并喜欢控制变量。

Answer 2

除了hakank所示的谓词，这里还有另外两种表达相同谓词的方式

include "globals.mzn";

%
% Ensure that a and b are perumutations of each other by 
% counting the number of occurences of each value in the 
% domains of a and b, 
%
predicate permutation_count(array[int] of var int: a,
                            array[int] of var int: b) =
    let {
        set of int: I = index_set(a),
        constraint assert(I = index_set(b), "Index sets of a and b must match"),
        set of int: domain = dom_array(a) intersect dom_array(b),
        set of int: NValues = 1..card(domain),
        array[NValues] of int: values = [ v | v in domain ],
        array[NValues] of var 0..card(I): counts,
    } in
    global_cardinality_closed(a, values, counts) /\
    global_cardinality_closed(b, values, counts);

%
% Ensure that a and b are permutations of each other by
% sorting each and constraining that to be the same.
% 
predicate permutation_sort(array[int] of var int: a,
                           array[int] of var int: b) =
    let {
        set of int: I = index_set(a),
        constraint assert(I = index_set(b), "Index sets of a and b must match"),
        set of int: domain = dom_array(a) intersect dom_array(b),
        array[I] of var domain: sorted_values,
    } in
    sorted_values = sort(a) /\
    sorted_values = sort(b);

int: n = 3;

array[1..n] of var 1..2: x;
array[1..n] of var 1..2: y;

constraint permutation_count(x, y);

solve satisfy;

第一个计算两个输入数组中的值，因为在排列中计数必须相同。第二个变体使用排序约束对 a 和 b 进行排序以检查它们是否相同。

哪种变体效果最好可能因求解器、问题和问题实例而异。如果输入的域很大，计数解决方案可能会有问题，这一点值得记住。

MiniZinc - 强制两个数组相等的约束

MiniZinc - Constraint to enforce two arrays be equal

constraint-programming