Solving Knight's Tour Problem using SV Constraints

SystemVerilog
, , ,
1

Knight’s tour is a sequence of moves of a knight on a chessboard such that the knight visits every square only once, for more info please check Wikipedia.

So assuming we have N*N chessboard, say N=5 for simplicity, whose squares are numbered from 0 to 24, as shown:

944×398 53.6 KB

I wrote the code below to get random array tour_indices for possible indices of the movements, i.e.

tour_indices[0] is the square index of the first move (e.g. 6).
tour_indices[1] is the square index of the second move (e.g. 13).
tour_indices[2] is the square index of the third move (e.g. 22).
tour_indices[24] is the square index of the last move.

But I got solver timeout from 3 out of 4 commercial simulator :-) (EDA playground: Edit code - EDA Playground)

So I do appreciate your reply if you have a better solution that doesn’t disturb the solver :-)

`define size 5

class knightTour #(int N = 5);
  rand byte tour_indices[N*N];
  rand byte curr_row_idx[N*N];
  rand byte curr_col_idx[N*N];
  rand byte next_row_diff[N*N];
  rand byte next_col_diff[N*N];

  constraint c_next_diff {
    foreach(next_row_diff[i]){
      next_row_diff[i]  inside {-2, -1, 1, 2};
      curr_row_idx[i] == 0    ->  next_row_diff[i]  inside {1, 2};
      curr_row_idx[i] == 1    ->  next_row_diff[i]  inside {-1, 1, 2};
      curr_row_idx[i] == N-2  ->  next_row_diff[i]  inside {-2, -1, 1};
      curr_row_idx[i] == N-1  ->  next_row_diff[i]  inside {-2, -1};
    }
    foreach(next_col_diff[i]){
      next_col_diff[i]  inside {-2, -1, 1, 2};
      curr_col_idx[i] == 0    ->  next_col_diff[i]  inside {1, 2};
      curr_col_idx[i] == 1    ->  next_col_diff[i]  inside {-1, 1, 2};
      curr_col_idx[i] == N-2  ->  next_col_diff[i]  inside {-2, -1, 1};
      curr_col_idx[i] == N-1  ->  next_col_diff[i]  inside {-2, -1};
    }
    foreach(next_col_diff[i]){
      next_row_diff[i] inside {-2, 2} -> next_col_diff[i] inside {-1, 1};
      next_row_diff[i] inside {-1, 1} -> next_col_diff[i] inside {-2, 2};
    }
  }
  constraint c_row_indices { 
    foreach(curr_row_idx[i]){
      curr_row_idx[i]  inside {[0:N-1]};
      (i>0)  ->  curr_row_idx[i] == curr_row_idx[i-1]+next_row_diff[i-1];
    }
  }
  constraint c_col_indices {    
    foreach(curr_col_idx[i]){
      curr_col_idx[i]  inside {[0:N-1]};
      (i>0)  ->  curr_col_idx[i] == curr_col_idx[i-1]+next_col_diff[i-1];
    }
  }
      
  constraint c_tour_indices {
    unique {tour_indices};
    
    foreach(tour_indices[i]){
      tour_indices[i] inside {[0:N*N-1]};
      tour_indices[i] == N*curr_row_idx[i]+curr_col_idx[i];
    }
  }
endclass

module testbench;
  knightTour #(`size) m_knightTour;
  
  initial begin
    m_knightTour = new();

    repeat(3) begin
      if(m_knightTour.randomize()) begin
        $write("tour_indices ");
        for (int i = 0; i < `size*`size; i++) $write( "%d ", m_knightTour.tour_indices[i]);
        $display("\n=====================================\n");
      end
      else
        $error("ERROR");
    end
  end
endmodule
2

In reply to Wafa:
Hi Wafa,

I’ve tried the following, but it’s only fully working with one simulator :), though I managed to get a repetition or 2 from other simulators before getting a solver timeout
I’ve done other trials, but I always get the solver timeout with other simulators.

I’ve checked the outcome manually, so I’d appreciate it if you double-check it.
EDA playground: Edit code - EDA Playground

//----------------------------------//
class knight#(SSIZE=5);
    
  const int XMOVES_1 [2] = {1,-1};  
  const int XMOVES_2 [2] = {2,-2};
  const int YMOVES_1 [2] = {1,-1}; 
  const int YMOVES_2 [2] = {2,-2};
  
  localparam SIZE = SSIZE*SSIZE;
  rand int xstep_1[SIZE];
  rand int ystep_1[SIZE];
  rand int xstep_2[SIZE];
  rand int ystep_2[SIZE];
  
  rand int x_next_moves[SIZE];
  rand int y_next_moves[SIZE];
  rand int tour[SIZE];

    constraint c0 {
      
       foreach(x_next_moves[i]) {
          
          x_next_moves[i] inside {[0:SSIZE-1]};
          y_next_moves[i] inside {[0:SSIZE-1]};
          tour[i] inside {[0:SIZE-1]};
          
          xstep_1[i] inside {XMOVES_1};
          xstep_2[i] inside {XMOVES_2};
          ystep_1[i] inside {YMOVES_1};
          ystep_2[i] inside {YMOVES_2};

          if(i != 0) {
            ((x_next_moves[i-1] + xstep_1[i]) == x_next_moves[i]) -> ((y_next_moves[i-1] + ystep_2[i]) == y_next_moves[i]);
            ((x_next_moves[i-1] + xstep_2[i]) == x_next_moves[i]) -> ((y_next_moves[i-1] + ystep_1[i]) == y_next_moves[i]);
            ((x_next_moves[i-1] + xstep_1[i]) == x_next_moves[i]) ^ ((x_next_moves[i-1] + xstep_2[i]) == x_next_moves[i]);
            solve x_next_moves[i] before y_next_moves[i];
          }
         tour[i] == ((x_next_moves[i]*SSIZE) + y_next_moves[i]);
         solve x_next_moves[i], y_next_moves[i] before tour[i];       
       }  
       unique {tour};
    }
endclass

//-------------------------------------------------------//
module test;
  localparam TEST_SSIZE = 5;
    initial begin
      knight#(TEST_SSIZE) k;
      k = new ();
      repeat(5) begin
        void'(k.randomize());
        foreach(k.tour[i]) begin $write("%3d", k.tour[i]); end  
        $display("\n=============================================================================\n");
        end
    end
endmodule
3

//Write a constraint to solve knight’s tour.Code your testbench here

class myC#(N=5);
  rand int Row[N*N];
  rand int Col[N*N];
  rand int helper_arr[N*N];
  
  constraint c0{
    foreach(Row[i]){
      Row[i] inside {[0:N-1]};
      Col[i] inside {[0:N-1]};
    }
      Row[0] == 0; Col[0] == 0;
  }
      
      constraint c1{
        foreach(helper_arr[i]) {
          helper_arr[i] == Row[i]+N*Col[i];
          helper_arr[i] inside {[0:N*N-1]};
        }
          unique{helper_arr};
      }
  
  constraint c2{
    solve Row before Col;
    solve helper_arr before Row;
    
    foreach(Row[i])
      if(i>0) {      
        (Row[i] - Row[i-1]) inside {-2,-1,1,2};
        (Col[i] - Col[i-1]) inside {-2,-1,1,2};
        (Row[i] - Row[i-1]) inside{ -2, 2} -> (Col[i] - Col[i-1]) inside {-1,1};
        (Row[i] - Row[i-1]) inside {-1,1} -> (Col[i] - Col[i-1]) inside {-2,2};
        
      }
  }
        
  constraint c3{
    //closing game
    Row[N*N-1] inside {1,2};
    Col[N*N-1] inside {1,2};
    Row[N*N-1] + Col[N*N-1] == 3;
  }
  
  function void post_randomize();
    $display("The Coordinates Are: \n");
    
    
                    $display("==========================================================================================");

    for (int i = 0; i < N*N; i++) begin
      $write("%d", helper_arr[i]);
    end
                $display("==========================================================================================\n");


    foreach(Row[i])
      $display("(%d, %d)", Row[i],Col[i]);
  endfunction
  
endclass
    
module  test;
  myC C =new;
  
  initial begin
    repeat(3)
      C.randomize();
  end
endmodule
1 Like