Boolector #6 Sudoku
This time we’ll discuss how to solve Sudoku with Boolector.
Algorithm:
Let’s consider 9x9 Sudoku (a grid) with some values filled, and needs to be completed keeping some constraints in mind. Constraints!
SAT solver can assign random values to the whole grid but these constraints should be followed.
Every element of grid should be between 1 and 9 (for 9x9) both inclusive.
Every row should have distinct element.
Every column should have distinct element.
Every sub-grid (3x3) should have distinct element.
Here you got your Sudoku solution.
Let’s dive deep in code.
- Let’s create a Btor instance and enable model generation for whole code until deletion of Btor instance. We are setting the output number format to be in decimal, whenever we are going to print the output.
Btor *btor=boolector_new();
boolector_set_opt(btor,BTOR_OPT_MODEL_GEN,1);
boolector_set_opt(btor,BTOR_OPT_OUTPUT_NUMBER_FORMAT,2);2. Let’s create custom data types for index, element each of 8 bits. Another data type representing a 1D array having index of type sort_index and elements of type sort_elem.
BoolectorSort sort_index=boolector_bitvec_sort(btor,8);
BoolectorSort sort_elem=boolector_bitvec_sort(btor,8);
BoolectorSort sort_d1_array=boolector_array_sort(btor,sort_index,
sort_elem);3. Now create a BoolectorNode grid representing a array of data type sort_d1_array with symbol “grid” here. Symbol is just a identification for array used during boolector_print_model().
boolector_print_model() prints all the inputs in the whole device (instance Btor) in a specified format (btor or smt2).
BoolectorNode *grid=boolector_array(btor,sort_d1_array,”grid”);4. Sudoku, that we are building, is a 9x9, but the array we built is 1D array. So what we did is represent 2D array as a 1D array with indexes in a sequential basis.
e.g. 9x9 indexes are
Row1: 0–8
Row2: 9–17
Row3: 18–26
till: 80
BoolectorNode *index[9][9];
for(int i=0;i<9;i++)
{
for(int j=0;j<9;j++)
{
index[i][j]=boolector_int(btor,i*9+j,sort_elem);
}
}5. Numbers for assignment to each cell in grid. Each index i is mapped with number i+1. (1–9)
BoolectorNode *assign[9];for(int i=0;i<9;i++)
{
assign[i]=boolector_int(btor,i+1,sort_elem);
}
6. Now some of the elements needs to be prefixed just like we get to solve.
Any boolector node is just like a vessel that needs to be emptied (released) before new assignment.
BoolectorNode *grid2;
grid2=boolector_write(btor,grid,index[0][6],assign[7]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[1][1],assign[3]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[1][2],assign[5]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[1][3],assign[0]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[2][2],assign[4]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[2][3],assign[2]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[2][5],assign[7]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[3][0],assign[8]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[3][3],assign[3]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[3][6],assign[6]);
boolector_release(btor,grid2);
grid2=boolector_write(btor,grid,index[3][8],assign[2]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[4][1],assign[1]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[4][7],assign[8]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[4][8],assign[3]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[5][0],assign[2]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[5][6],assign[5]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[6][3],assign[4]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[7][2],assign[7]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[7][6],assign[2]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[7][8],assign[0]);
boolector_release(btor,grid2);grid2=boolector_write(btor,grid,index[8][4],assign[1]);
boolector_release(btor,grid);grid=boolector_write(btor,grid2,index[8][5],assign[6]);
boolector_release(btor,grid2);
7. The constraints u1 (reused 1 time) checks that each element of grid array is between 1 and 9, both included.
BoolectorNode *readj,*readk,*u1;BoolectorNode *_1=boolector_int(btor,1,sort_elem);
BoolectorNode *_9=boolector_int(btor,9,sort_elem);for(int i=0;i<9;i++)
{
for(int j=0;j<9;j++)
{
readj=boolector_read(btor,grid,index[i][j]);
u1=boolector_ugte(btor,readj,_1); //readj<=1
boolector_assert(btor,u1); //constraint specified
boolector_release(btor,u1); //released for reuse
u1=boolector_ulte(btor,readj,_9); //readj<=9
boolector_assert(btor,u1); //constraint specified
boolector_release(btor,u1); //released for reuse
boolector_release(btor,readj); //released for reuse
}
}
8. This logic here sets up the constraint that no two elements in each row are equal.
readj is element in grid at index[i][j]
readk is element in grid at index[i][k]
for(int i=0;i<9;i++)
{
for(int j=0;j<9;j++)
{
readj=boolector_read(btor,grid,index[i][j]);
for(int k=0;k<9 && j!=k;k++)
{
readk=boolector_read(btor,grid,index[i][k]);
u1=boolector_ne(btor,readj,readk);
boolector_assert(btor,u1);
boolector_release(btor,readk);
boolector_release(btor,u1);
}
boolector_release(btor,readj);
}
}9. This logic here sets up the constraint that no two elements in each column are equal.
readj is element in grid at index[j][i]
readk is element in grid at index[k][i]
for(int i=0;i<9;i++)
{
for(int j=0;j<9;j++)
{
readj=boolector_read(btor,grid,index[j][i]);
for(int k=0;k<9 && j!=k;k++)
{
readk=boolector_read(btor,grid,index[k][i]);
u1=boolector_ne(btor,readj,readk);
boolector_assert(btor,u1);
boolector_release(btor,readk);
boolector_release(btor,u1);
}
boolector_release(btor,readj);
}
}10. This logic here sets up the constraint that no two elements in each subgrid are equal.
Each element in a 3x3 subgrid has same i/3 and j/3 among their indexes.
readij is element in grid at index[i][j]
readwk is element in grid at index[w][k]
BoolectorNode *readij,*readwk;
for(int i=0;i<9;i++)
{
for(int j=0;j<9;j++)
{
readij=boolector_read(btor,grid,index[i][j]);
for(int w=0;w<9;w++)
{
for(int k=0;k<9;k++)
{
if(i!=w && j!=k && i/3==w/3 && j/3==k/3)
{
readwk=boolector_read(btor,grid,index[w][k]);
u1=boolector_ne(btor,readij,readwk);
boolector_assert(btor,u1);
boolector_release(btor,readwk);
boolector_release(btor,u1);
}
}
}
boolector_release(btor,readij);
}
}11. boolector_sat will return BOOLECTOR_SAT if above constraints (assertions) are possible for any random values, othervise BOOLECTOR_UNSAT. OTHER, if there is any other error.
int result=boolector_sat(btor);
if(result==BOOLECTOR_SAT)
cout<<”SAT”<<endl;
else if(result==BOOLECTOR_UNSAT)
cout<<”UNSAT”<<endl;
else
cout<<”OTHER”<<endl;12. If BOOLECTOR_UNSAT, just release all connections in device and delete the device itself.
if(result==BOOLECTOR_UNSAT)
{
boolector_release_all(btor);
boolector_delete(btor);
return;
}13. Othervise, print the grid and then release the connections and then device itself.
int counti=0;
for(int i=0;i<9;i++)
{
++counti;
int countj=0;
for(int j=0;j<9;j++)
{
countj++;
readij=boolector_read(btor,grid,index[i][j]);
const char *s=boolector_bv_assignment(btor,readij);
cout<<s<<” “;
if(countj==3)
{
cout<<” | “;
countj=0;
}
boolector_free_bv_assignment(btor,s);
boolector_release(btor,readij);
}
cout<<endl;
if(counti==3)
{
for(int i=0;i<12;i++)
{
cout<<” — “;
}
cout<<endl;
counti=0;
}
}
boolector_release_all(btor);
boolector_delete(btor);
return;Complete code can be found here.
