Fun and Games with CRV: The N-Queens Problem

Blog Comments
1

It's been quite a while since we've solved the zebra puzzle using SystemVerilog. In this post we'll look at another oldie, but a goldie called the n-queens problem. This problem first appeared in a more specific form as the eight queens puzzle, first published in 1848. In this puzzle, the player is asked to place eight queens on a chessboard in such a way that they don't threaten each other. It has fascinated mathematicians (including the great Carl Friedrich Gauss) ever since to find solutions to it. Edsger Dijkstra used it to illustrate the power of backtracking. More recently, Team Specman also solved this problem using constraint programming and published it in this post. The e code they employed is short and sweet, but it's not so easy to digest, though.

This is a companion discussion topic for the original entry at https://verificationgentleman.netlify.app/2015/02/26/fun-and-games-with-crv-n-queens-problem.html
2

Very prettily done - thanks.

I’ve used $onehot constraints but I’m not 100% sure that all the main tools support that.

Did you, at any point in your experiments, try using an auxiliary variable (one for each column, and possibly another for each row) that contains the location of the queen? That might make some of the constraints easier to write, but perhaps would give the solver a harder time.

When doing “interesting” things with SV constraints - whether for intellectual pastime like this, or for the day job - I’ve often found myself hitting incomprehensible performance problems, simply because I have no idea how the tools’ solvers are doing their job. Each tool seems to have its own “no go areas”, constraint idioms that cause solver performance to drop horribly - but it’s really hard to get any kind of grip on why that happens, and what you can do to avoid it. That’s a slightly simpler problem for Specman users because they have only one implementation to worry about (two, I suppose, if you count both Intelligen and pgen?) and the Specman documentation says quite a lot about how things work behind the curtain. Constraint solver performance in SV, and how to avoid hobbling it, would be a good topic for a future post or series of posts, if anyone has any expertise in that area.

4

That’s a pity. Only 1 of 3 simulators I tried supports $onehot in constraints. Using an auxiliary “which bit should be set” variable works fine, and does not seem to cause any trouble when combined with other constraints on the vector:

rand bit [N-1:0] v;
rand int position;
constraint v_onequeen {
position inside {[0:N-1]};
v == (1 << position);
}

5

I didn’t want to use the method you describe (with the auxiliary variable per row/column) because that’s how Vitaly did it in his Specman post and I didn’t want my post to just be a simple translation from e to SV. I also wanted to experiment with the array reduction method in constraints (as that’s something new in the 2012 standard).

With respect to solver performance, I’ve tried it out in 2 simulators and I have noticed considerably worse performance on one vs. the other. It’s as you say, pretty much impossible to know why. I usually try to stay away from such topics as simulator performance as I don’t want to get slapped with a lawsuit. Even ignoring that, I would have no idea where to start, since what applies to one simulator won’t apply to another.

6

class n_queen_puzzle#(int n=8);
rand bit board[n][n];
rand bit board_tx[n][n];

constraint unique_row_c {
foreach(board[i,])
board[i].sum() with (int’(item)) == 1;
}

constraint board_tx_c {
foreach (board[i,j])
board_tx[j][i] == board[i][j];

solve board before board\_tx;

}

constraint unique_col_c {
foreach(board_tx[i,])
board_tx[i].sum() with (int’(item)) == 1;

}

constraint board_c2 {
foreach(board[i, j]) {
if(board[i][j]) {
foreach(board[k, l]) {
if(i != k && k+l == i+j) board[k][l] != 1;
if(i != k && l-k == j-i) board[k][l] != 1;
}
}
}
}
endclass

7

class array;
rand bit a[8][8];
constraint c_c{
foreach(a[i,])
{
a.sum() with ( item.index(1) == i ? 4’(item) : 0) == 1;
a.sum() with ( item.index(2) == i ? 4’(item) : 0) == 1;
a.sum() with ( item.index(1) - item.index(2) == -i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) - item.index(2) == i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) + item.index(2) == i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) + item.index(2) == i*2 ? int’(item) : 0) <= 1;
}
}

function display();
foreach(a[i]) begin
foreach(a[,j])
$write("%3d",a[i][j]);
$display;
end
endfunction
endclass