Oct. 19th, 2015

lederhosen: (Default)
I've been doing a course using MiniZinc, which is a specialised language for constraint/optimisation problems. It's a bit different to what I'm used to: it aims to separate the specification of the problem from the solution of the problem. Once you've told it the problem you want it to solve, it translates that into instructions to a solver.

As an example, here's one I wrote on the plane last Friday, to solve the in-flight magazine Sudoku:

include "globals.mzn";
int: box_size=3; % Side length of one of the constraint boxes in a grid
int: grid_size=box_size*box_size; % Total side length of the grid e.g. 3x3=9
set of int: Rows = 1..grid_size; % i.e. rows have index values 1 through grid_size
set of int: Cols = 1..grid_size;
array[Rows,Cols] of var 1..grid_size: grid_solved; % This is the solution we're trying to find
array[Rows,Cols] of 0..grid_size: grid_start; % Clues, with 0 = blank

% Set the standard constraints:
constraint forall(i in Rows)(alldifferent([grid_solved[i,j]|j in Cols]));
constraint forall(j in Cols)(alldifferent([grid_solved[i,j]|i in Rows]));
constraint forall(k,l in 0..box_size-1)(alldifferent([grid_solved[i+k*box_size,j+l*box_size]|i,j in 1..box_size]));
% Require that the solution matches clues
constraint forall(i in Rows, j in Cols)(grid_start[i,j]>0->grid_solved[i,j]=grid_start[i,j]);
% Tell MiniZinc that we just want a solution that satisfies these
% requirements (i.e. we're not trying to optimise anything)
solve satisfy;

% Define the clues - picked this one from
% http://www.telegraph.co.uk/news/science/science-news/9359579/Worlds-hardest-sudoku-can-you-crack-it.html

% And output the solution.
[ show(grid_solved[i,j])++
if j == grid_size then "\n" else " " endif
| i in Rows, j in Cols ]

Using the default solver that came bundled with MiniZinc (Gecode), this finds a solution in about 30-50 milliseconds.

Note that I didn't tell it how to solve the puzzle; I just told it the rules that a successful solution must obey, and MiniZinc/Gecode worked out the rest on their own. I'm sure this is old hat to some of you, but for me this is pretty impressive.

For some more complex problems, it is necessary to give the solver a bit of guidance on what strategy to use, but even there it keeps the focus on defining what the problem is, and it lets me switch from one solver to another without changing my code. I can see this being useful.


lederhosen: (Default)

February 2017


Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Mar. 25th, 2017 12:04 am
Powered by Dreamwidth Studios