Is there a way to know what are the total number of solutions to randomization.
Lets say there is a class with some data members and constraints around them. Is it possible to know the size of solution space?
In reply to sharatk:
Not really. Although we conceptually think of the constraint solver of building a complete solution space and then randomly picking one of the solutions, that’s not how it’s usually implemented. For performance, tools perform optimizations that might prevent certain solutions from every being found.
There are tools beginning to provide some information on charataristics of the solution space. I would check with your tool vendor as this is a relatively new field.
In reply to dave_59:
Thanks Dave. Always helpful.
The problem I am trying to solve is, lets say we solve Sudoku using constraints. How am I sure that it is the only solution, there is? I can randomize it say 10k times and see if any solution was different from the first one I got. I can still not be completely sure.
Is there any other way way?
In reply to sharatk:
I was thinking of solving this exact example problem, but never made it past the mental exercise phase.
Assuming you have a class that models your sudoku puzzle, you’ll need an encapsulating class that contains two sudoku instances. In both instances you set the values of the fixed cells and turn rand_mode off on those cells. Then randomize one instance, which should generate a solution.
Then the encapsulating class provides a constraint to enforce the 2 instances are not identical. i.e.
class unique_solution;
sodoku a = new;
rand sodoku b = new;
constraint {
a.cell != b.cell;
}
function set( int x, y, val );
a.cell[x][y] == val; a.cell[x][y].rand_mode(0);
b.cell[x][y] == val; b.cell[x][y].rand_mode(0);
endfunction
function void solve();
// set fixed cells
set( 1, 4, 3 );
set( 6, 8, 2 );
...
// find a solution
if ( a.randomize() ) begin
$display(" found a solution ");
if ( this.randomize() ) begin
$display(" found another solution, first was not unique ");
end
else begin
$display(" no other solution found, the first one was unique ");
end
end
else begin
$display(" your puzzle has no solution ");
end
endclass
Now, how well solvers handle this could be another issue.
*edited
In reply to sharatk:
I think this has to be left as an academic exercise as so far the only way to prove the number of solutions for a Sudoku puzzle is exhaustive simulation with a supercomputer.
In reply to dave_59:
in which case that becomes…
if ( this.randomize() ) begin
$display(" found another solution, first was not unique ");
end
else begin
$display(" ¯\_(ツ)_/¯ ");
end
@dave
I think Warner’s solution is smart, which can be extrapolated to see if this is a unique solution
Warner,
Awesome job there. Though I must point out
a.cell[0][0] != b.cell[0][0]
… Is unncessary in SV. You can just do a.cell != b.cell and it should just work.
In reply to sharatk:
Though I must point out
a.cell[0][0] != b.cell[0][0]
… Is unncessary in SV. You can just do a.cell != b.cell and it should just work.
I don’t know what you’re talking about? ;)
In reply to dave_59:
Hai, dave
I thought of a method like this:-
Randomize the array with given constraint, and then store the result into a queue of such arrays;
So the constraint is like the present array should not resemble the previous array (means at least if one element is different from previous arrays, make it as a valid one)
For that I want to compare the stored arrays with present arrays but I cannot do a direct compare ( double equal to ) of arrays;
Is there any way I can do to help me solve that array comparison please…
Thank you.
If you want to, here is a look of my sudoku_class part with constraints:-
`define SUD_DIMENSION 9 // The parameter user needs to provide
//the dimension of the total sudoku
// for a 4x4 one, it is 4
// for a 9x9 one, it is 9
// for a 16x16 one, it is 16, and so on..
`define SUB_SQUARE_SIZE 3
typedef int generic_arr[1:`SUD_DIMENSION][1:`SUD_DIMENSION];
//-------------------------Class Definition-----------------------
class solve_sudoku;
rand generic_arr sud_arr;
generic_arr tmp_arr ;
generic_arr stored_q[$];
bit counting_arr[`SUB_SQUARE_SIZE][`SUB_SQUARE_SIZE]; //used for framing uniqueness of sub-sqaures
function new();
foreach(tmp_arr[i,j]) begin
tmp_arr[i][j]=0;
end
endfunction
function void add_elem(int row,col,val);
tmp_arr[row][col]=val;
endfunction
//all entries of array should be in between in given range
constraint range_values {
foreach(sud_arr[i,j]) {
sud_arr[i][j]>=1;sud_arr[i][j]<=`SUD_DIMENSION;
}
}
//unique , rows
constraint unique_row {foreach(sud_arr[i]) {unique {sud_arr[i]};}}
//make columns unique:
constraint unique_col {
foreach (sud_arr[r1,c1]) foreach(sud_arr[r2,c2]) {
c1 == c2 && r1 != r2 -> sud_arr[r1][c1] != sud_arr[r2][c2]; // unique col
}}
//take starting point of a sub-square, and then loop
// to ensure every element in the sub-square is not equal to others
constraint sub_square_unique{ //subset squares constraint
foreach(sud_arr[r,c]) { //foreach1
r%`SUB_SQUARE_SIZE==1 && c%`SUB_SQUARE_SIZE==1 ->
foreach(counting_arr[r1,c1]) { //foreach2
foreach(counting_arr[r2,c2]) { //foreach3
(r1!=r2) && (c1!=c2) -> sud_arr[r+r1][c+c1] != sud_arr[r+r2][c+c2];
} // closing of foreach1
} //closing of foreach2
}// closing of foreach3
} // end of subset squares constraint
constraint pre_def_elemts { //pre-defined elements are fixed here
foreach(tmp_arr[r,c]) {
if(tmp_arr[r][c] != 0)
sud_arr[r][c]==tmp_arr[r][c];
}
}
constraint no_repetitions_please {
if(stored_q.size() > 0)
foreach(stored_q[i]) {
sud_arr != stored_q[i]; //this is not working..
}
}
endclass