k个连续整数约束

Question

如何在约束编程中陈述以下约束？ （最好在 Gurobi 或 Comet 中）。

S 是一个大小为 n 的整数数组。我可以用来填充数组的整数集在 1-k 范围内。对于每个可以使用的整数，都有一个约束 ci。 ci表示连续整数的最小个数i。

例如，如果 c1 = 3，c2 = 2，则 1112211112111 不是有效序列，因为必须有两个连续的 2，而 1112211122111 是有效序列。

Answer 1

也许使用常规约束（Comet 中的自动机）是最好的方法。

然而，这是 MiniZinc 中一个简单的解决方案，它使用了很多具体化。至少应该可以将它翻译成彗星（我认为 Gurobi 不支持具体化）。

决策变量（序列）在数组“x”中。它还使用一个辅助数组（“starts”），其中包含每个序列的起始位置；这使得推理“x”中的序列变得更容易。序列数以“z”为单位（例如，用于优化问题）。

根据 x 的大小和其他约束，可能会添加更多（冗余）约束，例如可以有多少序列。不过，这里没有这样做。

这是型号：http://www.hakank.org/minizinc/k_consecutive_integers.mzn

如下图所示。

int: n;
int: k;

% number of consecutive integers for each integer 1..k
array[1..k] of int: c;

% decision variables
array[1..n] of var 1..k: x;

% starts[i] = 1 ->  x[i] starts a new sequence
% starts[i] = 0 ->  x[i] is in a sequence
array[1..n] of var 0..k: starts;
% sum of sequences
var 1..n: z = sum([bool2int(starts[i] > 0) | i in 1..n]);

solve :: int_search(x, first_fail, indomain_min, complete) satisfy;

constraint
   forall(a in 1..n, b in 1..k) (
      (starts[a] = b ) -> 
         (
             forall(d in 0..c[b]-1) (x[a+d] = b )
             /\
             forall(d in 1..c[b]-1) (starts[a+d] = 0 )
             /\
             (if a > 1 then x[a-1] != b else true endif)    % before 
             /\
             (if a <= n-c[b] then x[a+c[b]] != b else true endif) % after
         )
  )
  /\
  % more on starts
  starts[1] > 0 /\
  forall(i in 2..n) (
     starts[i] > 0 <-> ( x[i]!=x[i-1] )
  )
  /\
  forall(i in 1..n) (
     starts[i] > 0 -> x[i] = starts[i]
  )
;

output [ 
     "z     : " ++ show(z) ++ "\n" ++
     "starts: " ++ show(starts) ++ "\n" ++
     "x     : " ++ show(x)  ++ "\n"
];


%
% data
%

%% From the question above:
%% It's a unique solution.
n = 13;
k = 2;
c = [3,2];