Difference between similar MiniZinc constraints

Question

In the solution of the Zebra puzzle (http://rosettacode.org/wiki/Zebra_puzzle#MiniZinc) there's a constraint stating that one of the pets must be a zebra:

var 1..5: n;
constraint Gz[n]=Zebra; 

Has the expression below a different meaning? They yield different results.

constraint exists(n in 1..5)(Gz[n]=Zebra);

Answer 1

These constraints are indeed equivalent. There is however a different in the way MiniZinc will translate these constraint for the solver.

The first option will be translated as a element constraint:

var 1..5: n;
constraint array_int_element(n, Gz, Zebra);

While the second one will result in an big clause constraint:

constraint bool_clause([Gz[1]=Zebra, Gz[2]=Zebra, Gz[3]=Zebra, Gz[3]=Zebra, Gz[5]=Zebra], [])

Although the constraints are equivalent it might depend on the solver which form will be more efficient during solving.

A better approach is to use the global count_leq(array [int] of var int: x, int: y, int: c) which enforces c to be less or equal to the number of occurences of y in x. Expressing the constraint as:

include "count_leq.mzn";
constraint count_leq(Gz, Zebra, 1);

directly conveys the meaning of the constraint and allows the solver used to use whichever form of the constraint would be best suited for its solving mechanism