Minizinc basic understanding of arrays and booleans

Question

After running through the tutorials, thinking I got the concepts, I set about creating my own model and immediately ran into problems. Better to get stuck in asap to realise just how little you actually know, imo.

In this example I would simply like to get an output where classes consist of students that want them, i.e. true, as represented by my array (not every student is able to attend on every day).

There could be all sorts of badness in the way the model was written...

Needless to say, I get the error WARNING: model inconsistency detected

enum Students = { Mark, Bart, Mary, Anne, Sue };

enum Classes = { Mon, Tue, Wed};

array[Students, Classes] of bool: pref =  
              [| true, true, false,
              | false, true, true,
              | true, false, true,
              | true, false, false,
              | false, false, true |];

constraint forall (i in Students, j in Classes)(pref[i,j]=true);

solve satisfy;

output [ " \(pref[Students,Classes]);\n"  ]

Bonus would be limiting it so each Student only appears once...

Perfect outcome would be something like a list of all the combinations where students preferences are satisfied and they are in 1 class.

[Mark, Anne | Bart | Mary, Sue]

Thank you for helping me along my way!

Answer 1

The vital part that you might not understand is that MiniZinc is a declarative language. You do not tell it how to solve a problem, but merely specify the problem and let the language do the rest.

A MiniZinc model is specified in terms of

• variables: decisions that need to be made / things you want to know
• parameters: things you already know
• constraints: the rules that are enforced between any or all variables and parameters.

In your model you didn't specify any variables, merely parameters and constraints. It is said to be inconsistent because you give it an array pref that contains both true and false, but then your constraint enforces that every element in the array must be true.

Likely you meant to make pref your set of variables and meant that your constraint should force one preference for every student:

enum Students = { Mark, Bart, Mary, Anne, Sue };
enum Classes = { Mon, Tue, Wed};

array[Students, Classes] of var bool: pref;
constraint forall (i in Students)(
  count(j in Classes) (pref[i, j]) = 1
);

solve satisfy;
output [ "pref = ", show2d(pref), ";"  ];

If you only want each student to have at least one preference you can use exists instead:

enum Students = { Mark, Bart, Mary, Anne, Sue };
enum Classes = { Mon, Tue, Wed};

array[Students, Classes] of var bool: pref;
constraint forall (i in Students)(
  exists(j in Classes) (pref[i, j])
);

solve satisfy;
output [ "pref = ", show2d(pref), ";"  ];

This would work, but if you know, as is the case in the first solution, that the students only make one preference, then it is better to just enforce this as part of the variable type:

enum Students = { Mark, Bart, Mary, Anne, Sue };
enum Classes = { Mon, Tue, Wed};

array[Students] of var Classes: pref;

solve satisfy;
output [ "pref = ", show(pref), ";"  ];

Then no constraint is required to ensure a student has exactly one preference.