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

Question

我试图用MiniZinc建模一个满意度问题，但我一直在编码这个约束：

给定两个长度相等的数组A和B，强制A是B的置换

换句话说，我正在寻找一个强制执行[1,2,2]=[1,2,2]和[1,2,2]=[2,2,1]的约束。非正式地说，A和B必须相等。对于某些n，这两个数组都定义在同一组整数上，特别是集合1..n-1上。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进行排序，以检查它们是否相同。

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