lederhosen: (Default)
[personal profile] lederhosen
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.

Date: 2015-10-20 01:55 pm (UTC)
From: (Anonymous)
That sounds interesting, but how do you know it's not just iteratively guessing random numbers until it finds a solution that matches the constraints?

Don't get me wrong; A programmable Monte Carlo solver is still useful, just not as cool.

-- Pat Scaramuzza


lederhosen: (Default)

April 2017

2345 678

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Apr. 30th, 2017 10:32 pm
Powered by Dreamwidth Studios