Introduction to MiniZinc
A couple weeks ago, my son Gavin challenged me with an alphametic puzzle:
T W O
+ T W O
--------
F O U R
It reminds me the course I took three years ago in coursera, Basic Modeling for
Discrete Optimization. The course introduced MiniZinc, a
constraint modeling language to describe the constraints and objective function.
The minizinc
toolchain then invoke specialized solvers, such as
Gecode, to find the solution. The course embodies the
story plot of Romance of the Three Kingdoms to demonstrate the discrete
optimization in the real world, :-).
Back to our problem, we can describe the problem as two-four.mzn:
include "alldifferent.mzn";
var 1..9: T; var 0..9: W; var 0..9: O; var 1..9: F; var 0..9: U; var 0..9: R;
constraint alldifferent([T, W, O, F, U, R]);
constraint 100 * T + 10 * W + O
+ 100 * T + 10 * W + O
= 1000 * F + 100 * O + 10 * U + R;
solve satisfy;
and solve the problem as:
minizinc --solver Gecode two-four.mzn
T = 7;
W = 3;
O = 4;
F = 1;
U = 6;
R = 8;
----------
Game solver
I find minizinc is quite handy to solve some board games.
There exists a Sudoku solver in the minizinc tutorial. I would showcase how to solve Flow Free game with minizinc.
The game starts with color dots in pairs scattered in the board. We need to connect matching colors with pipes to fill all blank spaces without crossing.
Thus for each cell, except the ends, MUST connect to two adjacent cells, one for input, the other for output. The ends connect to only one adjacent cell. So the constraints can be described as:
- If the cell is an end, it MUST have only one neighbor with the same color.
- Otherwise, it MUST have exactly two neighbors with the same color.
More concretely, we use the n_neighbor
predicate to lookup the init
, and
enforce number of neighbors as one if the color is pre-populated or two
otherwise.
enum COLOR;
int: width; int: height;
set of int: WIDTH = 1..width;
set of int: HEIGHT = 1..height;
array[HEIGHT, WIDTH] of COLOR: init;
array[HEIGHT, WIDTH] of var COLOR: board;
predicate n_neighbor(var int: i, var int: j, int: count) =
let { var COLOR: c = board[i, j] } in
sum([
if i > 1 then c == board[i-1, j] else false endif,
if i < height then c == board[i+1, j] else false endif,
if j > 1 then c == board[i, j-1] else false endif,
if j < width then c == board[i, j+1] else false endif
]) == count;
constraint forall(i in HEIGHT, j in WIDTH)(
if init[i, j] != X then
% X is blank
board[i, j] = init[i, j] /\ n_neighbor(i, j, 1)
else
n_neighbor(i, j, 2)
endif
);
solve satisfy;
We also separate the model.and data to make the model more generic:
minizinc --solver Gecode flow-free.mzn flow-free-hard.mzn
board = array2d(1..7, 1..7, [B, B, B, B, G, G, G, B, Y, Y, B, G, C, G, O, B, Y, B, G, C, R, O, B, Y, B, G, C, R, O, B, B, B, G, C, R, O, O, O, O, G, G, R, R, R, R, R, R, R, R]);
We can rearrange the 2d array for better readability:
B, B, B, B, G, G, G,
B, Y, Y, B, G, C, G,
O, B, Y, B, G, C, R,
O, B, Y, B, G, C, R,
O, B, B, B, G, C, R,
O, O, O, O, G, G, R,
R, R, R, R, R, R, R
Close thoughts
I highly recommend you to take the Basic Modeling for Discrete Optimization and the succeeding Advanced Modeling for Discrete Optimization courses to learn a little bit of MiniZinc. As most of us are not specialized in this domain, it is really powerful to simply describe the problem, then leverage the optimized solvers to solve the problems.