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:

1. If the cell is an end, it MUST have only one neighbor with the same color.
2. Otherwise, it MUST have exactly two neighbors with the same color.

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;

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

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