In a recent episode of the excellent Art of Mathematics podcast (specifically the one called A beautiful theorem with an ugly proof), the host Dr. Carol Jacoby offers the listener the following puzzle to solve:

Can you find a list of numbers such that they can be listed in an array with the properties that:

- The 0th cell contains how many zeroes are in the array,
- The 1st cell contains how many ones,
- The 2nd cell contains how many twos,
- …,
- The
*n*th cell contains how many*n*s

While going through the solution to the puzzle in the next episode, Dr. Jacoby mentioned that it was not incredibly hard to solve, but it was difficult to find an elegant proof that there was only one solution.

I spent some time noodling with this problem in my notebook, trying to discover (1) one or more solutions (obviously), and (2) properties of the problem that might lead to a proof. However I am no mathematician, so although I did find some solutions for various (small) values of *n*, I did not figure out how to prove anything about them.

It occurred to me that it could be fun to write a program to solve this problem. Lately, I have been working through the online course Basic Modeling for Discrete Optimization, which uses a declarative constraint programming language called MiniZinc. MiniZinc is developed by a team that includes one of the course instructors, Dr. Peter Stuckey, who also wrote an interesting book on constraint programming called Programming with Constraints, which is on my to-read list.

As I was working through the discrete optimization course, I thought: why not take a crack at this problem with MiniZinc? Although my MiniZinc programming capabilities are still at the “baby talk” level, that’s still enough to do useful work.

Before we share the actual MiniZinc program below, let’s restate the problem slightly differently so that it’s closer to the form MiniZinc will need:

- Give me an integer
`n=10`

that represents the maximum value of the array`0..9`

- Give me a set of integers we can use for indexing into the above array
- Create the actual array (let’s call it
`xs`

) based on the above specification - Constraint:
`xs`

element 0 contains how many zeroes are in the array - Constraint:
`xs`

element 1 contains how many ones are in the array - … and so on for 2 through 9, until we reach the end of the array (in this case it has ten elements)
- Find a solution that satisfies the above constraints

The complete program listing is below. I won’t try to explain the syntax here (for that see the MiniZinc tutorial), but you should be able to puzzle it out if you’ve done much programming.

Invoke it like so:

$ minizinc -a aom.mzn

This should result in the following output. The double line at the bottom means that this is the best/optimal solution.

10 = [6, 2, 1, 0, 0, 0, 1, 0, 0, 0] ---------- ==========

## Program Listing

% aom.mzn -- Puzzle from an episode of the podcast "The Art of Mathematics" int: n = 10; set of int: INDEX = 1 .. n; array[INDEX] of var 0..9: x; % The 0th cell contains how many zeroes are in the array. % The 1st cell contains how many ones. % The 2nd cell contains how many twos. % ... % The 9th cell contains how many nines. constraint forall(i in INDEX)(x[i] = sum(j in INDEX)(x[j] = i-1)); % I wrote the "unrolled loop" below first, then combined them into the % 'forall' expression you see above. % constraint x[1] = sum(i in INDEX)(x[i] = 0); % constraint x[2] = sum(i in INDEX)(x[i] = 1); % constraint x[3] = sum(i in INDEX)(x[i] = 2); % constraint x[4] = sum(i in INDEX)(x[i] = 3); % constraint x[5] = sum(i in INDEX)(x[i] = 4); % constraint x[6] = sum(i in INDEX)(x[i] = 5); % constraint x[7] = sum(i in INDEX)(x[i] = 6); % constraint x[8] = sum(i in INDEX)(x[i] = 7); % constraint x[9] = sum(i in INDEX)(x[i] = 8); % constraint x[10] = sum(i in INDEX)(x[i] = 9); solve satisfy; output ["\(sum(x)) = \(x)\n"]; % eof