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.

score 6 · Accepted Answer · edited May 21 '19 at 03:01

6

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.

edited May 21 '19 at 03:01

colelemonz

1,229
1
15
27

answered Nov 16 '17 at 18:21

Zayenz

1,914
12
11

Thanks for your hints. I am mostly dealing with Boolean variables rather than integers. Your links refer to integer constraints. – Axel Kemper Nov 16 '17 at 19:58
4

@AxelKemper MiniZinc makes use of automatic coercion. This means that Booleans can be used as integers and integers as floats, if required by a predicate or function. When in your case the predicate would consist of only Boolean arguments, we generally trust the compiler to simplify the constraint back to Boolean logical form. Note that in Gecode global constraints might perform better because of specialised propagators, while constructed predicates would consist of a (large) number of propagators. – Dekker1 Nov 16 '17 at 22:04

Cardinality constraints in MiniZinc

1 Answers1