CODEWITHSUNDEEP
minizinc
Attila Karoly
Attila Karoly

Reputation: 1021

Difference between similar MiniZinc constraints

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

Upvotes: 3

Views: 189

Answers (2)

Dekker1
Dekker1

Reputation: 5786

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

Upvotes: 3

hakank
hakank

Reputation: 6854

If the declaration var 1..5: n is removed, then there is no global n that can be used in the output section, and this will yield an error: MiniZinc: type error: undefined identifier n'`.

It you keep var 1..5: n then the variable n in the exists loop don't have any effect of the global defined variable n, with the result that (the global) n will take any of the values 1..5 (which is shown if all solutions are printed).

Upvotes: 2

Related Questions