This is part one of a two-part article. Part two is here.

A while back somebody told me to check out MiniZinc. Eventually I did and really enjoyed it, so figured I’d write about it here. This is actually going to be a two part article. Right now we’re talking about what it is and how it works, and in the next post we’ll talk about optimizing models.

MiniZinc is a constraint solving language designed for modeling optimization problems. You represent your problem as some fixed values, some values that may vary, some constraints, and what function you want to minimize/maximize/solve. Constraint solvers are one of those things that are way more obscure than they should be. A lot of people don’t even know constraint solvers exist, much less how useful they are.

As a practice project, I tried to do a scheduling problem. A conference has to schedule all of the accepted talks. Each talk is slotted to a specific day, hour, and conference room. To help with this, it sends a poll out to all attendees: rate every talk on a 5 point scale from “very interested” to “very uninterested”. This helps them find an ideal schedule. For example, if there are two talks that everybody wants to see, they probably shouldn’t be scheduled to the same day and time. Conversely, if there’s two talks with no overlap in the interested parties, then it’s fine to put them at the same time. Let’s model this problem in MiniZinc.

include "globals.mzn";

enum DAYS;
enum ROOMS;
enum TIMES;
constraint assert(card(DAYS) * card(ROOMS) * card(TIMES) == card(talks), "Number of slots must match number of talks");

enum talks;
enum people;

We define a set of days, rooms, times, talks, and attendees. In Minizinc enums are internally implemented as integers. I use them for type-checking. We’ll come back to the constraint later, but for now it’s just enforcing another sanity check for us.

array[people, talks] of 0..4: pref;

MiniZinc has only two complex types: sets and arrays. Multidimensional arrays are first-class constructs, and the values of arrays cannot also be arrays. This is all for optimization purposes: having just a few compact data structures means the search algorithms can be much more efficient.

It also means that the best way to represent what a given person thinks about a given talk is by a large 2D array. pref, like all of our enumerations, is a parameter, or par. The values of all pars are fixed before each run.

array[DAYS, TIMES, ROOMS] of var talks: sched;

This is our first decision variable, or var. While we choose the values of parameters, the solver chooses the values of the decision variables to satisfy the constraints. Interestingly, while vars and pars take on the same values and are directly comparable, they’re considered different types. Some functions will only accept one of the two, and some complex types can only be written as pars. For example, you can have a set of ints, but you can’t have a set of var ints.

constraint alldifferent (d in DAYS, t in TIMES, r in ROOMS) (sched[d, t, r]);

Next, we have a constraint. Any assignment to vars must satisfy all constraints for the model to be valid. If no possible assignment does so, the model is unsatisfiable. In this case, we’re requiring that every value in our sched array must be a different talk. If two values were the same talk then we’d have scheduled it twice. In some conferences this might be totally fine, but for ours, everybody goes once and nobody is left out. So we rule out that schedule with our constraint.

array[people] of var int: score;
constraint forall(p in people) (
  score[p] = sum([if exists (r in ROOMS) (pref[p, sched[d, t, r]] = 4) 
       then 1 else 0 endif | d in DAYS, t in TIMES] 
   )
);

Another var, this representing the “score” of the schedule. The constraint here doesn’t “rule out” any schedules like our previous one did. Instead, effectively assigns the score a value based on the schedule we chose. Most solvers are smart enough to realize that score is completely dependent on sched and will minimize time here.

For the score metric, I chose “number of ‘very interested’ talks a person can see.” I’m assuming that person can’t see two talks that have the same day and time, but different rooms. This means we can represent the score as the number of date-times where at least one room has a talk that person really likes.

solve maximize sum(score);

output 
 ["SCORE: \(sum(score)) \n\n"] ++
 [show(sched[d, t, r]) ++ " " ++ 
   if r == card(ROOMS) then if t == card(TIMES) then "\n\n" else "\n" endif else "" endif | d in DAYS, t in TIMES, r in ROOMS];

Finally, we can choose whether we’re just trying to find a solution that satisfies all constraints or find the optimum such solution by some metric. We want the latter with the sum of each person’s score. The output is just to format our results nicely. That’s the whole model!

Running the Model

To run the model, we need to assign values to our parameters. We can either do this per-run or create a data file to preassign to.

DAYS = anon_enum(2);
ROOMS = {r1, r2};
TIMES = {morning, noon};

people = anon_enum(2);
talks = {t01, t02, t03, t04, t05, t06,
         t07, t08};

pref = [| 4, 1, 4, 4, 1, 4, 1, 1
        | 1, 1, 4, 4, 4, 1, 1, 4
        |]

One nice thing about MiniZinc is it decouples the definition of the problem from the implementation. There are a bunch of different solvers out there, optimized for different kinds of problems, and we’re free to choose the fastest one for our case. For this problem, we’re going to use Chuffed, which comes default with MiniZinc.

SCORE: 8 

t07 t04 
t05 t01 

t08 t06 
t02 t03 

----------
==========
Finished in 569msec

Our naive, completely unoptimized model runs in a fraction of a second.

Adding Complications

Another nice thing about using a constraint language is that it’s optimized for just that, expressing constraints. If the problem gets more complicated, we don’t need to rewrite everything to account for the complication. We can just add another constraint.

Let’s throw on a random complication: while every talk is unique, every presenter is not. t08 and t02 are both by the same person. For the sake of her sanity we won’t schedule both talks for the same day. How can we do to do this?

If we were writing the scheduling algorithm ourself, this would be a huge mess. But in MiniZinc it’s pretty simple:

enum speakers;
array[talks] of speakers: talk_by;
constraint forall (d in DAYS) (
  alldifferent (t in TIMES, r in ROOMS) (talk_by[sched[d, t, r]])
);

If we add the following to our data table

speakers = {s1, s2, s3, s4, s5, s6, s7};
talk_by = [s1, s2, s3, s4, s5, s6, s7, s2];

Then we get a new maximized output:

SCORE: 8 

t01 t05 
t02 t03 

t08 t06 
t04 t07 

----------
==========

Simple.¹

Optimizing

There’s one big problem with everything we’ve done. Our model is tiny. We’re trying to schedule eight talks according to the preferences of two people. You could easily brute force that. Most conferences are much larger than that, and we haven’t show MiniZinc scales to larger problems.

My goal was 24 talks and 20 people. With that there’d be 480 parameters and 24!/(4!)^6 possible conferences, well out of the domain of brute force and simple optimizations. Unfortunately, it’s also out of the domain of our naive model. I tried testing that and MiniZinc was still trying to solve it eight hours later. We need to make things faster. Much faster.

While expressing constraints is easy, optimizing them is a topic of its own. Most of the solvers are really heavily heuristics-based and it’s hard to know, in advance, whether a given optimization will speed things up or slow things down. It’s also not linear, and three optimizations may be ten times faster than any two alone. In the end, I was able to get full model finish in under five seconds. But the process to get there was long and windy with a lot of blind guessing.

One thing that made it harder was how few resources there were on optimizing MiniZinc. The official docs were good for learning how to use it but not for using it well. All the other stuff I could find was basic introductions as opposed to tips on use. This meant I mostly learned through trial and error.

This all means that I think it’d be more useful to everybody if I posted a more comprehensive article on how I optimized my model rather than just give some highlights here. Then it might help other beginners out there. Said article is about 3000 words long and will be going up next week is available here.

Thoughts

MiniZinc is interesting. My main issues were learning how to express specific constraints and making models run fast. I don’t think it’s too applicable to the kind of work I do, but I imagine it would be helpful to a lot of people who don’t know about it. If you’re interested in learning more, you can download it here and read the documentation here. There’s also this Coursera course which I haven’t yet tried.