This time I will try to solve N-Queen problem using Systemverilog solver constraint. They really need to add systemverilog to leetcode. Kidding! All the cool kids use python these days :).

The Rules are simple:

  • Queens can’t be on the same rows
  • Queens can’t be on the same columns
  • Queens can’t be on diagonal (this really expands to +ve and -ve diagonals)
// square can be 0 or 1 (1 means queen)
constraint a01 {foreach(grid[i][j]) grid[i][j] inside {[0:1]};}

// Each row can have one queen
constraint rows {foreach(grid[i][j]) grid[i].sum() == 1;}

// Each col can have one queen
consraint cols {
    foreach(grid[i][j]) {
        foreach(grid[r]) {
            (r != i) -> (grid[i][j] +grid[r][j] <=1);
        }
    }
}

// Diagnal can have one queen
// +ve diagonal where col+row is constant
// 0123
// 1234
// 2345
// 3456
//
// -ve diagonal where row-col is constant
// 0 -1 -2 -3
// 1  0 -1 -2
// 2  1  0 -1
// -3 2  1  0

consraint pdiag {
    foreach(grid[i][j]) {
        foreach(grid[x][y]) {
            ((i!=x && j!=y) && ((i + j) == (x + y))) -> ((grid[i][j] + grid[x][y])<=1);
        }
    }
}
consraint ndiag {
    foreach(grid[i][j]) {
        foreach(grid[x][y]) {
            ((i!=x && j!=y) && ((i - j) == (x - y))) -> ((grid[i][j] + grid[x][y])<=1);
        }
    }
}

The Output for 4x4 queen problem can be

0010
1000
0001
0100