MiniZinc 中的基数约束

Question

MiniZinc 约束求解器允许使用内置的sum() 函数非常轻松地表达cardinality constraints：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_sum(array[int] of var bool: x) =
    (sum(x) == 2);

满足基数约束，当且仅当布尔变量数组中的真元素数量符合指定时。布尔值会自动映射到整数值 0 和 1 以计算总和。

我将自己的基数约束谓词实现为一组计数器切片：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_serial(array[int] of var bool: x) =
    let 
    {
      int: lb = min(index_set(x));
      int: ub = max(index_set(x));
      int: len = length(x);
    }
    in
    if len < 2 then
      false
    else if len == 2 then
      x[lb] /\ x[ub]
    else
      (
        let 
        {
          %  1-of-3 counter is modelled as a set of slices
          %  with 3 outputs each
          array[lb+1..ub-1] of var bool: t0;
          array[lb+1..ub-1] of var bool: t1;
          array[lb+1..ub-1] of var bool: t2;
        }
        in
        %  first two slices are hard-coded
        (t0[lb+1] == not(x[lb] \/ x[lb+1])) /\
        (t1[lb+1] == (x[lb] != x[lb+1])) /\
        (t2[lb+1] == (x[lb] /\ x[lb+1])) /\
        %   remaining slices are regular
        forall(i in lb+2..ub-1)
        (
          (t0[i] == t0[i-1] /\ not x[i]) /\
          (t1[i] == (t0[i-1] /\ x[i]) \/ (t1[i-1] /\ not x[i])) /\
          (t2[i] == (t1[i-1] /\ x[i]) \/ (t2[i-1] /\ not x[i])) 
        ) /\
        %  output 2 of final slice must be true to fulfil predicate
        ((t1[ub-1] /\ x[ub]) \/ (t2[ub-1] /\ not x[ub]))
      )
    endif endif;

此实现使用切片之间的行/变量更少的并行编码：

%  This predicate is true, iff 2 of the array
%  elements are true
predicate exactly_two_parallel(array[int] of var bool: x) =
    let 
    {
      int: lb = min(index_set(x));
      int: ub = max(index_set(x));
      int: len = length(x);
    }
    in
    if len < 2 then
      false
    else if len == 2 then
      x[lb] /\ x[ub]
    else
      (
        let 
        {
          %  counter is modelled as a set of slices
          %  with 2 outputs each
          %  Encoding:
          %  0 0 : 0 x true
          %  0 1 : 1 x true
          %  1 0 : 2 x true
          %  1 1 : more than 2 x true
          array[lb+1..ub] of var bool: t0;
          array[lb+1..ub] of var bool: t1;
        }
        in
        %  first two slices are hard-coded
        (t1[lb+1] == (x[lb] /\ x[lb+1])) /\
        (t0[lb+1] == not t1[lb+1]) /\
        %   remaining slices are regular
        forall(i in lb+2..ub)
        (
          (t0[i] == (t0[i-1] != x[i]) \/ (t0[i-1] /\ t1[i-1])) /\
          (t1[i] == t1[i-1] \/ (t0[i-1] /\ x[i])) 
        ) /\
        %  output of final slice must be  1 0 to fulfil predicate
        (t1[ub] /\ not t0[ub])
      )
    endif endif;

问题：

使用本土基数谓词有意义吗？还是sum()的MiniZinc实现在解决速度方面毫无疑问？

更新：
我使用Gecode 作为求解器后端。

Answer 1

线性求和通常是在约束求解器中实现良好的最重要的约束之一，因此对于您的情况，使用简单求和的初始版本要好得多。特别是，Gecode 中实现布尔求和的传播器经过大量优化以尽可能高效。

作为一般规则，使用可用的约束通常是一个好主意。特别是，如果一个人正在做的事情很好地映射到global constraint，这通常是一个好主意。一个相关的例子是，如果您想计算一个整数数组中几个不同数字的出现次数，在这种情况下，global cardinality constraint 非常有用。

为了完整性：当使用惰性子句生成求解器（例如 Chuffed）时，（新颖的）分解有时可能会非常有用。但这是一个更高级的话题。