Boolector #5
Let’s create a program for n_queen problem with help of Boolector solver.
Idea is to randomize nxn grid with provided constraints so that we can reach the final output as expected.
The idea is:
- Take a one dimensional array array_id of size n.
- Each element of array should be inside 0 and n-1 both included.
- Each element should be distinct.
- array_1d[i]-array_1d[j]!=|i-j|
=> array_1d[i]-array_id[j]!=i-j && array_1d[i]-array_id[j]!=j-i
5. Now each element will belong to [0,n-1].
6. To get a grid of 1’s and 0’s, 1 being queen position and 0 being empty, 1 will be logically shifted to left by each element in array_1d.
After algorithm:
array_1d=[2,0,3,1]
Row1: 1<<2
Row2: 1<<0
Row3: 1<< 3
Row4: 1<<1
Now let’s break down the code.
- Get no. of queens to work with.
cout<<”Enter no. of Queens: “;
int n;
cin>>n;2. Get a get instance of Btor. Enable model generation, so that solver can look for assertion (constraints) and enable their working.
Btor *btor=boolector_new();
boolector_set_opt(btor,BTOR_OPT_MODEL_GEN,1);3. Now create custom data types to work with. First is sort_index to specify the the type, wherever they will be used would signify 8 bit vector. Other one is sort_elem to specify type of n bit vector.
Last but not least, is sort_d1_array is a data type for array with index of type sort_index and element of type sort_elem.
BoolectorSort sort_index=boolector_bitvec_sort(btor,8);
BoolectorSort sort_elem=boolector_bitvec_sort(btor,n);
BoolectorSort sort_d1_array=boolector_array_sort
(btor,sort_index,sort_elem);4. array_1d is of type sort_d1_array.
If anybody have experience with any HDL, or packed or unpacked vectors, they would be able to appreciated the mechanism.
array_1d is equivalent to → bit [n] array_1d [8];
BoolectorNode *array_1d=boolector_array(btor,sort_d1_array,0);5. Now array is defined, but how to recognize array elements with index. To recognize any element we need index of type BoolectorNode. Here each element of index is constant with serial values 0 to n-1 of type sort_index (8 bit vector).
BoolectorNode *index[n];for(int i=0;i<n;i++)
index[i]=boolector_int(btor,i,sort_index);
6. I like myself to be prepared for future😜. Let’s create some constants for 1,0,n-1.
BoolectorNode *_1=boolector_int(btor,1,sort_elem);
BoolectorNode *_0=boolector_zero(btor,sort_elem);
BoolectorNode *_n=boolector_int(btor,n-1,sort_elem);7. boolector_read will read from index[i] of array_1d and return the element on it as BoolectorNode i.e. read. u1 will be a 1 bit BoolectorNode containing output of boolector_ugte (unsigned greater than equal to) checking if read≥0. We don’t need to specify is BoolectorNode is 1 bit or 8 bit as it takes care of it itself. If function returning 1bit, left side will be make 1 bit Node, similarly with read, as it will read sort_elem type.
boolector_assert make up a constraint that u1 should be 1 making boolector_ugte return 1 => read≥0 is true.
Why boolector_release in middle of the logic? Well think of it like a box, we can’t just replace what’s in there. First it should be emptied, and then fill it with new value.
boolector_ulte will check that value read from array_1d is less than equal to n-1 (_n=boolector_int(btor,n-1,sort_elem)).
In this code block we have added 2 constraints on each element of array_1d.
read≥0 and read≤n-1
BoolectorNode *read,*u1;
for(int i=0;i<n;i++)
{
read=boolector_read(btor,array_1d,index[i]);
u1=boolector_ugte(btor,read,_0);
boolector_assert(btor,u1);
boolector_release(btor,u1);u1=boolector_ulte(btor,read,_n);
boolector_assert(btor,u1);boolector_release(btor,u1);
boolector_release(btor,read);
}
8. for any element in array_1d readi and any other element of array_1d readj:
readi should be not equal to readj (constraint on each pair of elements)
BoolectorNode *readi,*readj,*distinct;
for(int i=0;i<n;i++)
{
readi=boolector_read(btor,array_1d,index[i]);
for(int j=0;j<n;j++)
{
if(i!=j)
{
readj=boolector_read(btor,array_1d,index[j]);
distinct=boolector_ne(btor,readi,readj);
boolector_assert(btor,distinct);
boolector_release(btor,distinct);
boolector_release(btor,readj);
}
}
boolector_release(btor,readi);
}9. Here will we cover diagonal queens.
for any element in array_1d readi and any other element of array_1d readj:
readi-readj should be not equal to i-j (constraint boolector_assert)
readi-readj should not be equal to j-i (constraint)
for each pair of elements in array_1d:
(readi-readj)!=|i-j|
BoolectorNode *sub,*temp;
for(int i=0;i<n-1;i++)
{
readi=boolector_read(btor,array_1d,index[i]);
for(int j=i+1;j<n;j++)
{
if(i!=j)
{
readj=boolector_read(btor,array_1d,index[j]);
sub=boolector_sub(btor,readi,readj);
u1=boolector_int(btor,i-j,sort_elem);
temp=boolector_ne(btor,sub,u1);
boolector_assert(btor,temp);
boolector_release(btor,temp);
boolector_release(btor,u1); u1=boolector_int(btor,j-i,sort_elem);
temp=boolector_ne(btor,sub,u1);
boolector_assert(btor,temp);
boolector_release(btor,temp);
boolector_release(btor,u1);
}
}
}
10. here boolector_sat will return BOOLECTOR_SAT is above assertion, all of them, are actually possible, otherwise BOOLECTOR_UNSAT.
int result=boolector_sat(btor);
if(result==BOOLECTOR_SAT)
cout<<”SAT”<<endl;
else if(result==BOOLECTOR_UNSAT)
cout<<”UNSAT”<<endl;
else
cout<<”OTHER”<<endl;11. if result is BOOLECTOR_UNSAT, means there is no solution following above assertions (constraints), then release all resources and abort.
Otherwise, we can print the solution. Now each element of array_1d represent where to put the queen and index represents a row.
here boolector_sll is used for logical shift left.
if(result==BOOLECTOR_UNSAT)
{
boolector_release_all(btor);
boolector_delete(btor);
return;
}BoolectorNode *sll;
for(int i=0;i<n;i++)
{
read=boolector_read(btor,array_1d,index[i]);
sll=boolector_sll(btor,_1,read);
const char *s=boolector_bv_assignment(btor,sll);
cout<<”s[“<<i<<”]: “<<s<<endl;
boolector_free_bv_assignment(btor,s);
boolector_release(btor,read);
}
12. Lastly we release the resources and leave.
boolector_release_all(btor);boolector_delete(btor);return;
Here is complete code for N_queen problem.
void n_queen()
{
cout<<”Enter no. of Queens: “;
int n;
cin>>n; Btor *btor=boolector_new();
boolector_set_opt(btor,BTOR_OPT_MODEL_GEN,1);
//boolector_set_opt(btor,BTOR_OPT_OUTPUT_NUMBER_FORMAT,0);
BoolectorSort sort_index=boolector_bitvec_sort(btor,8);
BoolectorSort sort_elem=boolector_bitvec_sort(btor,n);
BoolectorSort sort_d1_array=boolector_array_sort(btor,sort_index,sort_elem);BoolectorNode *index[n];for(int i=0;i<n;i++)
index[i]=boolector_int(btor,i,sort_index);BoolectorNode *array_1d=boolector_array(btor,sort_d1_array,0); BoolectorNode *_1=boolector_int(btor,1,sort_elem);
BoolectorNode *_0=boolector_zero(btor,sort_elem);
BoolectorNode *_n=boolector_int(btor,n-1,sort_elem);//each unique value
BoolectorNode *read,*u1;
for(int i=0;i<n;i++)
{
read=boolector_read(btor,array_1d,index[i]);
u1=boolector_ugte(btor,read,_0);
boolector_assert(btor,u1);
boolector_release(btor,u1); u1=boolector_ulte(btor,read,_n);
boolector_assert(btor,u1); boolector_release(btor,u1);
boolector_release(btor,read);
}
BoolectorNode *readi,*readj,*distinct;
for(int i=0;i<n;i++)
{
readi=boolector_read(btor,array_1d,index[i]);
for(int j=0;j<n;j++)
{
if(i!=j)
{
readj=boolector_read(btor,array_1d,index[j]);
distinct=boolector_ne(btor,readi,readj);
boolector_assert(btor,distinct);
boolector_release(btor,distinct);
boolector_release(btor,readj);
}
}
boolector_release(btor,readi);
}//diagonal queens
BoolectorNode *sub,*usubo,*temp;
for(int i=0;i<n-1;i++)
{
readi=boolector_read(btor,array_1d,index[i]);
for(int j=i+1;j<n;j++)
{
if(i!=j)
{
readj=boolector_read(btor,array_1d,index[j]);
sub=boolector_sub(btor,readi,readj);
u1=boolector_int(btor,i-j,sort_elem);
temp=boolector_ne(btor,sub,u1);
boolector_assert(btor,temp);
boolector_release(btor,temp);
boolector_release(btor,u1); u1=boolector_int(btor,j-i,sort_elem);
temp=boolector_ne(btor,sub,u1);
boolector_assert(btor,temp);
boolector_release(btor,temp);
boolector_release(btor,u1);
}
}
} int result=boolector_sat(btor);
if(result==BOOLECTOR_SAT)
cout<<”SAT”<<endl;
else if(result==BOOLECTOR_UNSAT)
cout<<”UNSAT”<<endl;
else
cout<<”OTHER”<<endl;
if(result==BOOLECTOR_UNSAT)
{
boolector_release_all(btor);
boolector_delete(btor);
return;
} BoolectorNode *sll;
for(int i=0;i<n;i++)
{
read=boolector_read(btor,array_1d,index[i]);
sll=boolector_sll(btor,_1,read);
const char *s=boolector_bv_assignment(btor,sll);
cout<<”s[“<<i<<”]: “<<s<<endl;
boolector_free_bv_assignment(btor,s);
boolector_release(btor,read);
} boolector_release_all(btor); boolector_delete(btor); return;
}
For next part (Sudoku) click here.
