Exploring a shipping puzzle, part 3

← Back to Kevin's homepagePublished: 2018 November 25

Solving 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:

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

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:


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”.


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


Running1 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 datasets2 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:

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.

  1. 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
  2. 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)) "];")]))