Exploring a shipping puzzle, part 3
← Back to Kevin's homepagePublished: 2018 November 25Solving a constraint puzzle…with a constraint solver.
As promised in part 2, I solved the shipping puzzle using MiniZinc. I won’t explain too much about how MiniZinc works in this article. If you’re curious for more, check out:
The awesome MiniZinc Coursera video course (this is how I learned MiniZinc in a few weeks so that I could implement the solution below)
Hillel Wayne’s Constraint Solving with MiniZinc and Optimizing MiniZinc posts
I’ll explain the parts of my solution, then at the end discuss some general thoughts about MiniZinc. Lets dive in!
(Update: See also a reader’s MiniZinc solutions and a differential dataflow solution.)
Types + Data
The first part of my solution defines the data types and a specific problem instance (which should look familiar from part 1):
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types
enum DAY = {M, T, W, R, F};
enum CITY;
set of int: leg_id;
array[leg_id] of CITY: start;
array[leg_id] of CITY: end;
array[leg_id] of DAY: dow;
set of int: route_id;
array[route_id, DAY] of var 0..card(leg_id): routes;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Data
CITY = {PDX, SFO, SEA, DEN, JFK};
leg_id = {1 , 2 , 3 , 4 , 5 , 6 };
start = [PDX, PDX, SEA, DEN, PDX, DEN];
end = [SEA, SFO, DEN, PDX, DEN, JFK];
dow = [M , T , T , W , R , F ];
% We don't know in advance how many routes there might be.
% Worst case bound is when no legs can be connected and each is its own route.
route_id = 1..card(leg_id);
A few things to note here:
Types annotated with
var
are what we’re asking MiniZinc to find for us. In this case, the onlyvar
s are the values of theroutes
array.We’re telling MiniZinc that
routes
should be an array whose rows are routes, columns are days, and values are integers between 0 and the number ofleg_id
s.The lowest
leg_id
starts at 1, and we’re using 0 to mean “no leg assigned”. So a row containing0 0 1 5 0
represents a route which starts with leg 1 on Wednesday and finishes after leg 5 on Thursday.Unlike in the Rust and Clojure solutions, where I represented legs as structs / maps, in MiniZinc they’re all “unrolled” into separate arrays. This is the famous “array of structs” vs. “struct of arrays” representation tradeoff (see Wikipedia).
Constraints
The constraints look pretty similar from the Alloy solution in part 1.
The forall
and sum
syntax is a list comprehension: The first set of parentheses gives the bindings, and the second set gives the body.
The \/
and /\
are infix disjunction and conjunction operators (between friends: “OR” and “AND”).
% Each leg is used exactly once
constraint forall(l in leg_id)
(1 = sum(r in route_id, d in DAY)
(l = routes[r, d]));
% Legs are assigned on the right day
constraint forall(r in route_id, d in DAY where routes[r, d] != 0)
(d = dow[routes[r, d]]);
% Legs must be consecutive and match locations
constraint forall(r in route_id, d in DAY diff {F})
(let { var int: l1 = routes[r, d];
var int: l2 = routes[r, enum_next(DAY, d)]}
in (l1 = 0 \/ l2 = 0 \/ end[l1] = start[l2]));
% Planes cannot stay idle (no empty legs within a route)
constraint forall(r in route_id, d in DAY)
(routes[r, d] = 0 > ( forall(d2 in DAY where d2 > d)(routes[r, d2] = 0)
\/ forall(d2 in DAY where d2 < d)(routes[r, d2] = 0)));
This last constraint took me a minute to come up with.
The >
arrow is implication, and the constraint reads “for a given route, if a day doesn’t have a leg assigned, then all of the following OR all of the preceding days must also be unassigned”.
Objective
Finally, we have the objective of our problem: Find the minimum number of routes:
var int: num_routes;
constraint num_routes = sum(r in route_id)
(0 != sum(d in DAY)(routes[r, d]));
solve minimize num_routes;
output ["num_routes = \(num_routes)\n"];
array[int] of var opt int: non_empty_routes = [r  r in route_id where 0 != sum(d in DAY)(routes[r, d])];
output ["\(r): \(d) \(routes[r, d])\n"  r in non_empty_routes, d in DAY];
Output
Running^{1} MiniZinc gave this correct solution:
num_routes = 2
1: M 1
1: T 3
1: W 4
1: R 5
1: F 6
2: M 0
2: T 2
2: W 0
2: R 0
2: F 0
Unfortunately, when I exported larger datasets^{2} and tried to run this program, MiniZinc failed to complete.
(I tried both the chuffed
and default gecode
solvers, and stopped waiting after 6 minutes for just a 100 leg problem.)
Attempted symmetry breaking
I think one reason that my solution is unable to handle more than 10 legs is because of the growth of degenerate representations.
That’s a fancy way of saying that there are multiple routes
array for each “actual” solution.
In our example, MiniZinc found this routes
array:
1 3 4 5 6
0 2 0 0 0
but the ordering of the rows doesn’t matter.
The routes
array could have just as well been:
0 2 0 0 0
1 3 4 5 6
Without a constraint to “break the symmetry” of these routes
arrays, I think MiniZinc is looking through all of these equivalent representations.
And since the number of these representations grow factorially with the number of legs, things become intractable pretty quickly.
(See Hillel’s Optimizing MiniZinc post for more detail on this.)
I attempted to break the symmetry by forcing an order on the rows: Say, the rows must be ordered by the id of their first leg.
However, I couldn’t figure out how to express this. My first attempt:
predicate nonempty_route(route_id: r) = (0 != sum(d in DAY)(routes[r, d]));
constraint increasing(r in route_id where nonempty_route(r))
([routes[r, d]  d in DAY][0]);
gave me this error:
MiniZinc: type error: no function or predicate with this signature found: `increasing(array[int] of var opt int)'
which I think is because increasing
accepts arrays var int
values rather than var opt int
(opt
meaning optional) — MiniZinc’s type system isn’t convinced that the the array defined by the comprehension [routes[r, d]  d in DAY]
will have a first element.
Trying to order by the maximum leg id:
constraint increasing(r in route_id where nonempty_route(r))
(max(d in DAY)
(routes[r, d]));
returns the same error.
(The return type of max
is var opt int
.)
In both cases, wrapping with deopt
to try and coerce the var opt int
to var int
had no effect.
Other thoughts
I want MiniZinc to do well on this problem, but seem to keep running into roadblocks. I’m about 3 hours into working on this shipping puzzle problem (not counting authoring this post), in addition to the ~14 hours I spent going through the Coursera course.
My thoughts on MiniZinc more broadly:
Syntax: This is a cliche gripe from people who enjoy Lisp, but I kept tripping up on MiniZinc’s syntax. I mean look at this:
constraint forall(r in route_id, d in DAY diff {F}) (let { var int: l1 = routes[r, d]; var int: l2 = routes[r, enum_next(DAY, d)]} in (l1 = 0 \/ l2 = 0 \/ end[l1] = start[l2]));
The
let { ... } in ...
feels awkward, the twocharacter disjunction operator gives me TLA+ and undergrad LaTeX flashbacks, and there are land mines in the form of occasional, inexplicably nonsymbolic infix operators likediff
. I just wish I could write something like(constraint (forall [rid route d (diff day {F})] (let [l1 (routes r d) l2 (routes r (enumnext DAY d))] (or (= l1 0) (= l2 0) (= (end l1) (start l1))))))
Which looks better to me, at least =P
0 is special: It seems to be idiomatic in MiniZinc to use
0
as a special “empty” case, but this just feels a bit dangerous to me. At least, I haven’t internalized the idiom enough to trust myself to easily understand code that relies on it.This includes my own code — I feel gross for saying that the value of the
routes
array is of typevar 0..card(leg_id)
. But I did it because I couldn’t getvar opt leg_id
to run at all.Hard to play with data: The “structure of arrays” input data format makes it difficult to play around with the data — when I mess with sample data manually, I spent most of the time trying to line everything up so I don’t accidentally make an offbyone mistake. The easiest way for me to work with different data representations in MiniZinc was by writing Clojure programs to spit out data in the right shape, rather than try to reshape in MiniZinc.
Ditto when it comes to the output format. I’d love to print a 2D array of the results, or even a table of the city names, but I am terrified of what sort of
output
list comprehensions I’d need to write to do so.(Admittedly, this sort of thing may be out of MiniZinc’s scope as specialized solver software rather than a general purpose language.)
On the whole, though, I’ve enjoyed learning MiniZinc.
I’m impressed that it can handle some numeric optimization problems like this loan calculation that I might struggle to solve algebraically.
MiniZinc seems like a handy tool to keep in my back pocket. I’m secretly hoping to run into a tricky discrete optimization problem that I can’t solve in Clojure or Rust, and I’ll be able to make it shine.

MiniZinc comes with an IDE, but it (version 2.2.2) wouldn’t run on my old OS X (version 10.9.5), so I ran everything via the command line: ↩
/Applications/MiniZincIDE.app/Contents/Resources/minizinc shipping1.mzn

I used the following Clojure program to export legs to a MiniZinc data file: ↩
(spit "../mzn/shipping.dzn" (str/join "\n" [ (str "CITY = {" (str/join "," (distinct (concat (map :start legs) (map :end legs)))) "};") (str "leg_id = {" (str/join "," (range 1 (inc (count legs)))) "};") (str "start = [" (str/join "," (map :start legs)) "];") (str "end = [" (str/join "," (map :end legs)) "];") (str "dow = [" (str/join "," (map :dow legs)) "];")]))