Brain puzzle solver

2016-09-01

Brain puzzles are generally of the form of an area of numbers, letters, or icons and you must fill in the blanks using logical deduction. The rules are basically a set of constraints though the puzzles may vary. Currently one of the most common of these puzzles is the Sudoku. One might say hyped but I'm pretty sure the hype is over. It's fairly mainstream nowadays anyways.

TL;DR here is the shiny

A Sudoku has fairly simple constraints; in a grid of 9x9 cells each row and colum of the grid must contain all numbers from 1 to 9, once. Additionally the grid is divided in nine 3x3 mini grids and each of these must also get all numbers 1 to 9 once. Thassit.

I've been doing these brain puzzles for nearly twenty years. That doesn't make me smart or anything, I just like doing them. Now, Sudoku's are a little boring to my taste. I'll do one every now and then but definitely favor others.

It so happens that the past few months I've been hard at work on a finitedomain solver for a client. A finite domain solver is an piece of code that accepts some vars with possible values, some constraints like this var must be less than that var, and will try to assign a value to each variable without breaking any of the constraints. A fairly straightforward concept but deceptively difficult.

Combine that with puzzles and you get something beautiful ;)

Let's take a look at Sudoku's for example. There are 81 variables (each cell in the 9x9 grid). Each variable can have a value ranging from 1 through 9. There are also the two general constraints; each row and column must contain the values 1 through 9 exactly once. Each designated 3x3 must contain each number 1 through 9 exactly once.

The way we'd code that in the solver is something like this (untested, just from the top of my head okay quickly tested):

Code:
let solver = new Solver;
// add the cells for a blank puzzle
// an actual puzzle will want to explicitly init some of these vars
for (let y = 0; y < 9; ++y) {
for (let x = 0; x < 9; ++x) {
solver.addVar('cell' + (x+1) + (y+1), [1, 9]);
}
}
// nine rows
solver.distinct(['cell11', 'cell12', 'cell13', 'cell14', 'cell15', 'cell16', 'cell17', 'cell18', 'cell19']);
solver.distinct(['cell21', 'cell22', 'cell23', 'cell24', 'cell25', 'cell26', 'cell27', 'cell28', 'cell29']);
solver.distinct(['cell31', 'cell32', 'cell33', 'cell34', 'cell35', 'cell36', 'cell37', 'cell38', 'cell39']);
solver.distinct(['cell41', 'cell42', 'cell43', 'cell44', 'cell45', 'cell46', 'cell47', 'cell48', 'cell49']);
solver.distinct(['cell51', 'cell52', 'cell53', 'cell54', 'cell55', 'cell56', 'cell57', 'cell58', 'cell59']);
solver.distinct(['cell61', 'cell62', 'cell63', 'cell64', 'cell65', 'cell66', 'cell67', 'cell68', 'cell69']);
solver.distinct(['cell71', 'cell72', 'cell73', 'cell74', 'cell75', 'cell76', 'cell77', 'cell78', 'cell79']);
solver.distinct(['cell81', 'cell82', 'cell83', 'cell84', 'cell85', 'cell86', 'cell87', 'cell88', 'cell89']);
solver.distinct(['cell91', 'cell92', 'cell93', 'cell94', 'cell95', 'cell96', 'cell97', 'cell98', 'cell99']);
// nine columns
solver.distinct(['cell11', 'cell21', 'cell31', 'cell41', 'cell51', 'cell61', 'cell71', 'cell81', 'cell91']);
solver.distinct(['cell12', 'cell22', 'cell32', 'cell42', 'cell52', 'cell62', 'cell72', 'cell82', 'cell92']);
solver.distinct(['cell13', 'cell23', 'cell33', 'cell43', 'cell53', 'cell63', 'cell73', 'cell83', 'cell93']);
solver.distinct(['cell14', 'cell24', 'cell34', 'cell44', 'cell54', 'cell64', 'cell74', 'cell84', 'cell94']);
solver.distinct(['cell15', 'cell25', 'cell35', 'cell45', 'cell55', 'cell65', 'cell75', 'cell85', 'cell95']);
solver.distinct(['cell16', 'cell26', 'cell36', 'cell46', 'cell56', 'cell66', 'cell76', 'cell86', 'cell96']);
solver.distinct(['cell17', 'cell27', 'cell37', 'cell47', 'cell57', 'cell67', 'cell77', 'cell87', 'cell97']);
solver.distinct(['cell18', 'cell28', 'cell38', 'cell48', 'cell58', 'cell68', 'cell78', 'cell88', 'cell98']);
solver.distinct(['cell19', 'cell29', 'cell39', 'cell49', 'cell59', 'cell69', 'cell79', 'cell89', 'cell99']);
// nine 3x3
solver.distinct(['cell11', 'cell12', 'cell13', 'cell21', 'cell22', 'cell23', 'cell31', 'cell32', 'cell33']);
solver.distinct(['cell41', 'cell42', 'cell43', 'cell51', 'cell52', 'cell53', 'cell61', 'cell62', 'cell63']);
solver.distinct(['cell71', 'cell72', 'cell73', 'cell81', 'cell82', 'cell83', 'cell91', 'cell92', 'cell93']);
solver.distinct(['cell14', 'cell15', 'cell16', 'cell24', 'cell25', 'cell26', 'cell34', 'cell35', 'cell36']);
solver.distinct(['cell44', 'cell45', 'cell46', 'cell54', 'cell55', 'cell56', 'cell64', 'cell65', 'cell66']);
solver.distinct(['cell74', 'cell75', 'cell76', 'cell84', 'cell85', 'cell86', 'cell94', 'cell95', 'cell96']);
solver.distinct(['cell17', 'cell18', 'cell19', 'cell27', 'cell28', 'cell29', 'cell37', 'cell38', 'cell39']);
solver.distinct(['cell47', 'cell48', 'cell49', 'cell57', 'cell58', 'cell59', 'cell67', 'cell68', 'cell69']);
solver.distinct(['cell77', 'cell78', 'cell79', 'cell87', 'cell88', 'cell89', 'cell97', 'cell98', 'cell99']);
// go!
solver.solve({max: 1});
// ->
[{
cell11: 1, cell21: 2, cell31: 3, cell41: 4, cell51: 5, cell61: 6, cell71: 7, cell81: 8, cell91: 9,
cell12: 4, cell22: 5, cell32: 6, cell42: 7, cell52: 8, cell62: 9, cell72: 1, cell82: 2, cell92: 3,
cell13: 7, cell23: 8, cell33: 9, cell43: 1, cell53: 2, cell63: 3, cell73: 4, cell83: 5, cell93: 6,
cell14: 2, cell24: 1, cell34: 4, cell44: 3, cell54: 6, cell64: 5, cell74: 8, cell84: 9, cell94: 7,
cell15: 3, cell25: 6, cell35: 5, cell45: 8, cell55: 9, cell65: 7, cell75: 2, cell85: 1, cell95: 4,
cell16: 8, cell26: 9, cell36: 7, cell46: 2, cell56: 1, cell66: 4, cell76: 3, cell86: 6, cell96: 5,
cell17: 5, cell27: 3, cell37: 1, cell47: 6, cell57: 4, cell67: 2, cell77: 9, cell87: 7, cell97: 8,
cell18: 6, cell28: 4, cell38: 2, cell48: 9, cell58: 7, cell68: 8, cell78: 5, cell88: 3, cell98: 1,
cell19: 9, cell29: 7, cell39: 8, cell49: 5, cell59: 3, cell69: 1, cell79: 6, cell89: 4, cell99: 2,
}]

We can see that the solution is correct. You can obviously setup the constraints a little conciser with loops. But for something as simple as Sudoku's I think this is a very legible code.

Now I didn't want to bother with Sudoku's so I've started on a gimmicky tool to solve so called "Tectonics" (English). In this variation of a Sudoku you have an n x m matrix of numbers. The matrix is cut up in clusters of p cells. Each cluster must contain each number from 1 to p, one number per cell. No cell can have a neighbor with the same value as itself, not even diagonally.

The constraints to this puzzle area also quite simple. Outlined above. The variables are a little more variable for Tectonic since they must range from 1 to the size of a cluster. Most of the simple puzzles have clusters of at most 5 cells so the domains are quite small. The constraints must check to make sure each neighboring cell contains a unique value (and preferably only check each neighbor once). Each cluster must also contain the required values 1 through p, once for each value in that range.

The solution is a little bit more work because we first must work out the clusters so we can apply a constraint on the cells in each cluster. Once we have those clusters it's a matter of

Code:
solver.sum([cell1, cell2, cell3, cell4], 10);

Where 10 is the sum of each number 1 through p. This will make sure the solver will require cell1 through cell4 to sum 10, regardless of their actual value. This still leaves a bunch of invalid possibilities (1+1+1+7=10) so we must make them unique as well

Code:
solver.distinct([cell1, cell2, cell3, cell4]);

And we must make sure each cell has no neighbor with the same value. This constraint is independent of the clusters. We could simply do a solver.neq ("not equal") for each neighbor of each cell but that will lead to every neighbor being checked twice. So instead we just check the left, top-left, top, and top-right neighbors of each cell. This has the added benefit of easily skipping over the x=0, y=0 cases (instead of checking x==width-1.

Code:
let n = x + y * width;
if (x || y) {
if (x) {
solver.neq(v, cellVars[ n - 1 ]); // w
if (y) {
solver.neq(v, cellVars[ n - 1 - width ]); // nw
}
}
if (y) {
solver.neq(v, cellVars[ n - width ]); // n
if (x < width - 1) { // var may not exist so ugly bound check
solver.neq(v, cellVars[ n + 1 - width ]); // ne
}
}
}

And that's it really.

I've coded a UI to build puzzles and solve them. You can see the code on github and a live demo of the toy on github pages.

The solve is rather fast, but that's no surprise to me. A 4x5 puzzle has 37 vars and 38 constraints (causing 104 propagators). A 9x11 has 177 vars and 269 constraints (into 637 propagators). While the potential search space is huge, a lot is chiseled away from it very quickly. This isn't that much different from doing them in your head, actually. Just ... automated and faster. Hurray for AI ;)

I intend to make solvers for other types of brain puzzles. I just need to find the time :) Although this didn't take me that long so who knows...

Have fun. I know I did.