Fun and Games with CRV: Sudoku

This week let's mix it up a bit and do something less work-related. Everybody probably knows what Sudoku is, but just in case you don't here's a link to the Wikipedia page.

Sudoku is a pretty popular game that many people play to pass the time. I've played it as well, but I'm not really good at it so I turned to my computer for help. Now, programming a Sudoku solver is probably really difficult, plus I would have no idea where to start. This is why we'll cheat and have the SystemVerilog random number generator solve it for us.

This is the beauty of constraint programming; we don't have to solve problems, we just have to describe them and let our constraint solver do the heavy lifting. While we want to express our problem in the form of constraints, we also want to express everything in an as short and abstract a way as possible. Let's get started!

We'll represent our Sudoku grid as a 9 x 9 array of integers. We'll define all properties (fields and constraints) in a class called sudoku_solver_base. This class will hold all of the rules needed to solve any game of Sudoku, while an actual game will be represented by a sub-class of this class that defines the initial starting point (for example also via constraints or by reading it from a file).

class sudoku_solver_base;
rand int grid[9][9];

// ...
endclass

The first constraint we have is that all elements inside our array must be numbers between 1 and 9, which is pretty easy to express (also note the syntax of a multi-dimensional foreach as this is common gotcha):

constraint all_elements_1_to_9_c {
foreach (grid[i, j])
grid[i][j] inside { [1:9] };
}

The elements on each row must also be unique. This is very easily expressed using SystemVerilog 2012's unique construct:

constraint unique_on_row_c {
foreach (grid[i])
unique { grid[i] };
}

Using unique has saved us from doing double foreach and has made the constraint much more readable.

The complementary of the last constraint is that all elements on a column must also be unique. This is a bit trickier as SystemVerilog doesn't have any way of slicing an array into columns. While we could do some double foreach looping, that wouldn't be as clean as using unique. What we first have to do is construct an auxiliary array that is the transpose of our grid. This requires extra memory but it will help keep our constraints more readable.

local rand int grid_transposed[9][9];

constraint create_transposed_c {
foreach (grid[i, j])
grid_transposed[i][j] == grid[j][i];
}

grid_transposed's rows will contain grid's columns. It's now easy to constrain these to have all unique elements:

constraint unique_on_column_c {
foreach (grid_transposed[i])
unique { grid_transposed[i] };
}

We may not have gained very much because we've anyway used a double foreach just to construct the transposed grid, but this is a pretty nifty trick if you need to apply complex constraints on 2D arrays. The idea isn't mine, I "borrowed" it from one of Team Specman's blog posts.

Now we have to concentrate on the 9 sub-grids that make up our Sudoku grid. Like we did with the transposed grid, we want to construct these and use unique on their elements. We can think of these sub-grids as being the elements of a 3x3 matrix. This is how we'll index them:

+-------+-------+-------+
| | | |
| (0,0) | (0,1) | (0,2) |
| | | |
+-------+-------+-------+
| | | |
| (1,0) | (1,1) | (1,2) |
| | | |
+-------+-------+-------+
| | | |
| (2,0) | (2,1) | (2,2) |
| | | |
+-------+-------+-------+

These we will keep in a 2D array of 3x3 arrays (which is basically a 4D array):

local rand int sub_grids[3][3][3][3];

Keeping with my goal of writing short and sweet constraints, the first thing I tried was directly slicing in two dimensions:

constraint create_sub_grids_c {
foreach (sub_grids[i, j])
sub_grids[i][j] == grid[3*i +: 3][3*j +: 3];
}

This unfortunately wasn't supported. "This is probably because of the range operator", I thought. "No big deal, I'll just slice row-wise", I then said to myself. I tried it out first for one row:

constraint create_sub_grids_c {
foreach (sub_grids[i, j])
sub_grids[i][j][1] == grid[3*i + 1][3*j + 1];
}

This was however also not supported as equality constraints cannot be defined on entire arrays, only on individual array elements. This means we have to use brute force and explicitly assign each element (something I would have hoped to avoid):

constraint create_sub_grids_c {
foreach (sub_grids[i, j, k, l])
sub_grids[i][j][k][l] == grid[i*3 + k][j*3 + l];
}

This was another double foreach I would have hoped to avoid. We'll, we've worked so much for our sub-grids, we might as well just use unique on them and set our final constraint:

constraint unique_in_sub_grid_c {
foreach (sub_grids[i, j])
unique { sub_grids[i][j] };
}

Here is where the harsh reality of simulator bugs hit me and even though uniqueness constraints on entire arrays are allowed by the LRM, the simulator was encountering an internal error during randomization. While annoying, I thought I could maybe work around it by first storing each sub-grid in a one dimensional array:

local rand int sub_grids_lin[3][3][9];

constraint create_sub_grids_lin_c {
foreach (sub_grids_lin[i, j, k])
sub_grids_lin[i][j][k] == sub_grids[i][j][k/3][k%3];
}

Magically, after inserting this constraint, the internal error was gone, even though I hadn't yet removed the array uniqueness constraint. I left this line inside the sample code just to have it working, but be aware that it shouldn't be necessary.

For testing I used the same puzzle as on Wikipedia:

class sudoku_solver extends sudoku_solver_base;
constraint puzzle_c {
grid[0][0] == 5;
grid[0][1] == 3;
grid[0][4] == 7;

// ...

grid[8][4] == 8;
grid[8][7] == 7;
grid[8][8] == 9;
}
endclass

The result I got was also the same as there on the first run. That's right, I got first time right Sudoku!

As always, you can find the full code on the blog's SourceForge repository. If you want to play with it a little more you could also create a file reader for it to read in the starting point of the puzzle.

I hope you enjoyed this little exercise! In a future post I do intend to implement the same thing in e and see if I end up with less code (or more). If you don't want to miss it, feel free to hit the subscribe button.

Comments