Exploring a shipping puzzle, part 3

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:

• 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 only vars are the values of the routes 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 of leg_ids.

  The lowest leg_id starts at 1, and we’re using 0 to mean “no leg assigned”. So a row containing 0 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¹ 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² 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 two-character disjunction operator gives me TLA+ and undergrad LaTeX flashbacks, and there are land mines in the form of occasional, inexplicably non-symbolic infix operators like diff. I just wish I could write something like

  (constraint
   (forall [rid route
            d (diff day {F})]
           (let [l1 (routes r d)
                 l2 (routes r (enum-next 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 type var 0..card(leg_id). But I did it because I couldn’t get var 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 off-by-one 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.