使用SystemVerilog解決數(shù)組問(wèn)題

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

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

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

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

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

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

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

另外，每列上的所有元素也必須是唯一的。此時(shí)我們就需要構(gòu)建一個(gè)輔助數(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] };          
}

要解決一個(gè)數(shù)獨(dú)問(wèn)題，僅有這3個(gè)約束遠(yuǎn)遠(yuǎn)是不夠的，因?yàn)?strong>還需要9 個(gè)子網(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)拿到所有對(duì)應(yīng)的3x3網(wǎng)格后，我們類似地可以使用unique語(yǔ)法結(jié)構(gòu)進(jìn)行約束。 注意，這里需要將3x3的網(wǎng)格轉(zhuǎn)換成一個(gè)一維數(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 ];           
}

????

審核編輯：湯梓紅