N Queen Board Problem in SV Constraint

Hi, I have been struggling in solving N queen problem in SV constraint. I know how to constraint the elements for each column and row(credit to the forum). However, diagonals are really a nightmare to me. Can anyone help me out, a detailed explain will be appreciated!!!


class queen_board;
 rand bit queen_b[8][8];
 
 constraint row_c {
    foreach(queen_b[row]) queen_b[row].sum() with (int'(item)) <= 1;
} 
 constraint col_c {
    foreach(queen_b[,col]) queen_b.sum() with (int'(queen_b[item.index(1)][col])) <= 1;
}
 constraint diag_c{
  //??????????????????????????
}
endclass

In reply to qkuang:
A key part of this problem is the diagonals have different lengths. You need to guard

module top;
  parameter N = 8;
  class queen_board;
    rand bit queen_b[N][N];
    constraint c {
      foreach(queen_b[i]) {
        queen_b[i].sum() with (int'(item)) == 1; // row
        queen_b.sum(b) with (int'(queen_b[b.index][i])) == 1; // col
        // descending diagonals
        queen_b.sum(b) with (i+b.index<N? int'(queen_b[b.index][i+b.index]) : 0) <= 1;
        queen_b.sum(b) with (i+b.index<N? int'(queen_b[i+b.index][b.index]) : 0) <= 1;
        // ascending diagonals
        queen_b.sum(b) with (i+b.index<N? int'(queen_b[N-1-i-b.index][N-1-b.index]) : 0) <= 1;
        queen_b.sum(b) with (i+b.index<N? int'(queen_b[N-1-b.index][N-1-i-b.index]) : 0) <= 1;
      }
    }
  endclass
     
  queen_board qb = new;
      initial repeat(5) begin
    assert(qb.randomize());
    foreach(qb.queen_b[i]) $display("%p",qb.queen_b[i]);
    $display;
  end
endmodule

In reply to dave_59:

Thanks Dave! What a elegant solution!
But I think your ascending diagonals constraints are equivalent to descending ones. So there may still has elements on same ascending diagonal.
I updated the constraint and added some comments. If people are interested in this puzzle, hopefully it can help.

if we have a 3X3 board, the coordinates for each location are:
(0,0)(0,1)(0,2)
(1,0)(1,1)(1,2)
(2,0)(2,1)(2,2)


//descending diagonals
 queen_b.sum(b) with (i+b.index<N? int'(queen_b[b.index][i+b.index]) : 0) <= 1;
 // constraint (0,0)+(1,1)+(2,2) <= 1, (0,1)+(1,2) <= 1, (0,2) <= 1;

 queen_b.sum(b) with (i+b.index<N? int'(queen_b[i+b.index][b.index]) : 0) <= 1;
 // constraint (0,0)+(1,1)+(2,2) <= 1, (1,0)+(2,1) <= 1, (2,0) <= 1;

// ascending diagonals
 queen_b.sum(b) with (i+b.index<N? int'(queen_b[b.index][N-1-b.index-i]) : 0) <= 1;
 // constraint (0,2)+(1,1)+(2,0) <= 1, (0,1)+(1,0) <= 1, (0,0) <= 1;

 queen_b.sum(b) with (i+b.index<N? int'(queen_b[i+b.index][N-1-b.index]) : 0) <= 1; 
 // constraint (2,0)+(1,1)+(0,2) <= 1, (2,1)+(1,2) <= 1, (2,2) <= 1;

In reply to dave_59:

Hi Dave ,
Have a question related to unrolling of queen_b.sum(b) :

foreach(queen_b[i]) queen_b[i].sum() with (int'(item)) == 1; 

Here item refers to each element of queen_b[i] i.e queen_b[i][0] to queen_b[i][7]
As i iterates from 0 to 7 , the resultant expression will be sum i.e addition (+) of 8 resultant with_expression i.e :
For queen_b[0].sum() i.e Row 0 :: int’( queen_b[0][0] ) + int’( queen_b[0][1] ) + … + int’( queen_b[0][7] ) == 1 ;
Similarly for queen_b[7].sum() i.e Row 7 :: int’( queen_b[7][0] ) + int’( queen_b[7][1] ) + … + int’( queen_b[7][7] ) == 1 ;

For queen_b.sum(b) , will the resultant expression comprise of sum of 8x8 i.e 64 with expressions ? ( with some elements being 0 due to false condition )

In reply to ABD_91:

Array reduction methods iterates single dimension of an array. For this question, if you didn’t specify with clause in queen_b.sum(b), it will cause a compiling error.

Hello @dave_59 , can you please let me know why the below code is not working for checking diagonal contradiction?

constraint c1 {
      foreach(queen_b[i,j]) {
        foreach(queen_b[m,n])
                {
                  if( i != m && j != n)
                  {
                    i - m != j - n;
                    i - m != n - j;
                  }
                  	
                }
           }
    }

Okay, I had forgotten to add a few additional conditions:

if( i != m && j != n && queen_b[i][j] == 1 && queen[m][n] == 1)

Hi @dave_59 Could you please explain the interpretation of this expression in constraint ? I understood the part where we are trying to identify diagonal elements such that they are below descending diagonal but couldn’t understand queen_b[b.index][i+b.index] . Please provide interpretation.