针对递归函数的 Minizinc 约束

Question

我想使用这样的函数：

function int: nextr(var int: n)
if n <= 1
  2
elseif n <= 8
  n + 5
elseif n <= 68
  n + 13
elseif n <= 509
  n + 34
elseif n <= 3611
  n + 89
else n + 233

在变量必须满足 nextr(n)、nextr(nextr(n))、nextr(next(nextr(n))) 等中的任何值的约束中。

有没有办法在 minizinc 中指定这样的约束？如果一般不可能，我可以接受显式递归限制，但不需要对所有步骤进行繁琐的枚举？

Answer 1

示例：

y 的值被限制为等于

next(x) \/ next(next(x)) \/ ...

最多 K 层嵌套。

function var int: nextr(var int: n) =
  if n <= 1 then
    2
  elseif n <= 8 then
    n + 5
  elseif n <= 68 then
    n + 13
  elseif n <= 509 then
    n + 34
  elseif n <= 3611 then
    n + 89
  else
    n + 233
  endif;

int: K = 10;

var int: x;
var int: y;
array[1..K] of var int: rec_up_to_k;

constraint forall (i in 1..K) (
  if i == 1 then
    rec_up_to_k[i] = nextr(x)
  else
    rec_up_to_k[i] = nextr(rec_up_to_k[i-1])
  endif
);

constraint exists (i in 1..K) (
  y = rec_up_to_k[i]
);

constraint x >= 0;

solve satisfy;

输出：

x = 3612;
y = 3845;
rec_up_to_k = array1d(1..10, [3845, 4078, 4311, 4544, 4777, 5010, 5243, 5476, 5709, 5942]);
----------

针对递归函数的 Minizinc 约束

Minizinc constraint against recursive function

minizinc