數(shù)獨是一種非常流行的游戲，數(shù)獨本質(zhì)上也是一個約束問題，所以我們可以讓SystemVerilog的約束求解器來幫助我們解決。 約束求解器的精妙之處就是，我們只描述約束限制，繁重的數(shù)值生成工作由工具來幫我們完成。 你只需“既要...又要...”，其他的讓下人干吧～

我們將數(shù)獨網(wǎng)格表示為9x9整數(shù)數(shù)組，在名為sudoku_solver_base的類中定義所有屬性字段和約束。

class sudoku_solver_base;          
  rand int grid[9][9];          
            
  // ...          
endclass

我們的第一個約束是數(shù)組中的所有元素都必須是 1 到 9 之間的數(shù)字，這很容易：

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

每行中的元素必須是唯一的，可以使用SystemVerilog中的unique語法結(jié)構(gòu)來描述：

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

另外，每列上的所有元素也必須是唯一的。此時我們就需要構(gòu)建一個輔助數(shù)組，將網(wǎng)格轉(zhuǎn)置。

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

然后再加上類似的unique約束：

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

要解決一個數(shù)獨問題，僅有這3個約束遠遠是不夠的，因為還需要9 個子網(wǎng)格（3x3）都滿足相同的約束。 我們將9x9網(wǎng)格保存在四維數(shù)組中：

local  rand  int  sub_grids [ 3 ][ 3 ][ 3 ][ 3 ];
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 ];           
}

在我們已經(jīng)拿到所有對應(yīng)的3x3網(wǎng)格后，我們類似地可以使用unique語法結(jié)構(gòu)進行約束。 注意，這里需要將3x3的網(wǎng)格轉(zhuǎn)換成一個一維數(shù)組再約束。

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 ];           
}

????

審核編輯：湯梓紅