Cardinality constraints in MiniZinc

Question

The MiniZinc constraint solver allows to express cardinality constraints very easily using the built-in sum() function:

%  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);

The cardinality constraint is met, if and only if the number if true elements in the array of Boolean variables is as specified. Booleans are automatically mapped to integer values 0 and 1 to compute the sum.

I implemented my own cardinality constraint predicate as set of counter slices:

%  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 implementation is using a parallel encoding with fewer lines/variables between the slices:

%  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;

Question:

Does it make sense to use home-grown cardinality predicates? Or is the MiniZinc implementation of sum() beyond all doubts in terms of solution speed?

Update:
I am using Gecode as solver back-end.

Answer 1

Linear sums is typically one of the most significant constraints to implement well in a constraint solver, so for your case the initial version using a simple sum is much better. In particular, the propagator in Gecode that implements the Boolean sum is heavily optimized to be as efficient as possible.

As a general rule, it is typically a good idea to use the constraints that are available. In particular, if what one is doing maps well to a global constraint that is typically a good idea. A related example would be if you want to count the occurrences of several different numbers in an array of integers, in which case the global cardinality constraint is very useful.

For completeness: When using lazy clause generation solvers (Chuffed for example), (novel) decompositions may sometimes be surprisingly useful. But that is a much more advanced topic.