Minizinc 阵列排序

Question

假设我有一个如下所示的数组声明

array[1..5] of int: temp = [1,0,5,0,3];

有没有办法启动一个看起来与 temp 相同但没有 0 的新数组？结果如下所示

[1,5,3]

或以 0 位于数组开头或结尾的方式对数组进行排序，即

[0,0,1,5,3]

或

[1,5,3,0,0]

谢谢

Answer 1

使用MiniZinc 2，可以按如下方式完成：

array[1..5] of int: temp = [1,0,5,0,3];
%  calculate upper bound of temp index
int: i_max = max(index_set(temp));
%  use array comprehension to count non-zero elements
int: temp_non_zero = sum([1 | i in 1..i_max where temp[i] != 0]);
%  copy non-zero elements to new array
array[1..temp_non_zero] of int: temp2 = [temp[i] | i in 1..i_max where temp[i] != 0];
%  calculate upper bound for temp2 index
int: i2_max = max(index_set(temp2));

solve satisfy;

%  show our variables
output 
["\ni_max=" ++ show(i_max)] 
++ ["\ni2_max=" ++ show(i2_max)] 
++ ["\n" ++ show(temp2[i]) | i in 1..i2_max] 
;

Answer 2

尽管 Axel 已经回答了这个问题，但我将展示另一种方法——在我的书中更简洁一些。

情况一：数组("temp")是常量数组。然后可以简单地写

数组[int] of int: temp2 = [temp[i] |我在 index_set(temp) where temp[i] != 0];

MiniZinc 2（对比版本1.*）如果可以计算则不需要声明大小；只需使用 "array[int]" 就足够了。此外，"index_set" 用于更通用一点，例如处理索引从 0..4 开始的情况（参见注释行）。

情况 2：数组 ("s") 是一个决策变量数组

如果要处理的数组是决策变量，我们不知道（根据定义）有多少个 0，必须依赖替代变体，即对数组进行排序。然后可以使用 "sort" 函数，如模型所示。

 include "globals.mzn";

 % constant
 array[1..5] of int: temp = [1,0,5,0,3];
 % array[0..4] of int: temp = array1d(0..4, [1,0,5,0,3]);
 array[int] of int: temp2 = [temp[i] | i in index_set(temp) where temp[i] != 0];

 % decision variables
 array[1..5] of var int: s;
 array[1..5] of var int: s2 = sort(s); % NOT CORRECT, see model below

 solve satisfy;

 constraint
    s = [1,0,5,0,3]
 ;

 %  show our variables
 output 
 [
    "temp: \(temp)\n",
    "temp2: \(temp2)\n",

    "s: \(s)\n",
    "s2: \(s2)\n",
 ];

更新

对于决策变量的稳定版本，这在我看来是有效的。它根据 "s[i]" 是否为 0 来计算放置此数字的位置。虽然不是很漂亮。

 int: n = 5;
 array[1..n] of var 0..5: s;
 array[1..n] of var lb_array(s)..ub_array(s): s2;

 solve satisfy;

 constraint
   s = [1,0,5,0,3] /\
   forall(i in 1..n) (
      if s[i] != 0 then
        s2[sum([s[j]!=0 | j in 1..i-1])+1] = s[i]
      else 
        s2[sum([s[j]!=0 | j in 1..n]) + sum([s[j]=0 | j in 1..i-1])+1 ] = 0
      endif
   )
;

output 
[ 
  "s: \(s)\n",
  "s2: \(s2)\n",
]
;

输出为

s: [1, 0, 5, 0, 3]
s2: [1, 5, 3, 0, 0]

Answer 3

另一种选择：

两个数组之间的1:1映射被建立为唯一索引值（=数组位置）的数组。然后对这些索引进行排序。如果元素指向零，则比较对元素的权重更高。因此，零值被移到后面，同时保持非零元素的顺序不变。

int: n = 5;
int: INF = 99999;    %  infinity
array[1..n] of var 0..5: s;
array[1..n] of var 1..n: map;
array[1..n] of var 0..5: s2;

solve satisfy;

%  set s[]
constraint
   s = [1,0,5,0,3]
;
%  1:1 mapping between s[] and s2[]
constraint 
  forall (i in 1..n) (
    exists(j in 1..n) (
      map[j] = i
    )
  )
;
constraint
   forall(i in 1..n) (
      s2[i] = s[map[i]]
   )
;
%  sort the map and move zero values to the back
constraint
   forall(i in 1..n-1) (
     (if s2[i] != 0 then map[i] else INF endif) <= 
     (if s2[i+1] != 0 then map[i+1] else INF endif)
   )
;

output 
[ 
  "s: \(s)\n",
  "map: \(map)\n",
  "s2: \(s2)\n",
]
;

输出：

s: [1, 0, 5, 0, 3]
map: [1, 3, 5, 4, 2]
s2: [1, 5, 3, 0, 0]

Minizinc 阵列排序

Minizinc array sorting

sorting

minizinc