nqueens/nqueens.cc

   1 #include <vector>
   2 #include <stack>
   3 #include <sstream>
   4 #include <iostream>
   5 #include <fstream>
   6 #include <cstdio>
   7 #include <cstdlib>
   8 #include "inc_solver.h"
   9 #include "solver_interface.h"
  10 #include "csolver.h"
  11 #include "common.h"
  12 #include <algorithm>
  13 #include <ctime>
  14
  15 using namespace std;
  16
  17 void EqualOneToCNF(vector<int> literals, vector< vector<int> > & cnf){
  18         int N = literals.size();
  19         cnf.push_back(literals);
  20
  21         vector<int> dnf;
  22         // this one is a->~b, a->~c, ...
  23         for (int j=0; j<N-1; j++){
  24                 for (int k=j+1; k<N; k++){
  25                         dnf.push_back(-literals[j]);
  26                         dnf.push_back(-literals[k]);
  27                         cnf.push_back(dnf);
  28                         dnf.clear();
  29                 }
  30         }
  31 }
  32
  33 void verticalSymmetryBreaking(vector<int> col1, vector<int> colN, vector<vector<int> > &cnf){
  34         vector<int> dnf;
  35         for(int i=0; i<col1.size(); i++){
  36                 dnf.push_back(-col1[i]);
  37                 for(int j=i+1; j<colN.size(); j++){
  38                         dnf.push_back(colN[j]);
  39                 }
  40                 cnf.push_back(dnf);
  41                 dnf.clear();
  42         }
  43
  44
  45 }
  46
  47 void Or( vector<int> literals, vector<vector<int> > & cnf){
  48         int N= literals.size();
  49         vector<int> dnf;
  50         for( int i=0; i<N; i++){
  51                 dnf.push_back(literals[i]);
  52         }
  53         cnf.push_back(dnf);
  54 }
  55
  56 void LessEqualOneToCNF(vector<int> literals, vector< vector<int> > & cnf){
  57         int N = literals.size();
  58         vector<int> dnf;
  59         // this one is a->~b, a->~c, ...
  60         for (int j=0; j<N-1; j++){
  61                 for (int k=j+1; k<N; k++){
  62                         dnf.push_back(-literals[j]);
  63                         dnf.push_back(-literals[k]);
  64                         cnf.push_back(dnf);
  65                         dnf.clear();
  66                 }
  67         }
  68 }
  69
  70 bool validateSolution(int N, int *table, int size){
  71         for(int k=0; k<size; k++){
  72                 if(table[k]>0){
  73                         int row = k/N;
  74                         int col = k%N;
  75                         for (int j= row*N; j<(row+1)*N; j++)
  76                                 if(j!=k && table[j] >0){
  77                                         return false;
  78                                 }
  79                         for(int j=0; j<N; j++){
  80                                 int indx = j*N+col;
  81                                 if(indx !=k && table[indx]>0){
  82                                         return false;
  83                                 }
  84                         }
  85
  86                         int i=row;
  87                         int j = col;
  88                         while( i>0 && j>0){
  89                                 int indx = i--*N+j--;
  90                                 if(k!=indx && table[indx]>0){
  91                                         return false;
  92                                 }
  93                         }
  94                         i=row;
  95                         j=col;
  96                         while(i>0 && j<N){
  97                                 int indx=i--*N+j++;
  98                                 if(k!=indx && table[indx]>0){
  99                                         return false;
 100                                 }
 101                         }
 102                         i=row;
 103                         j=col;
 104                         while(i<N && j>0){
 105                                 int indx = i++*N+j--;
 106                                 if(k!=indx && table[indx]>0){
 107                                         return false;
 108                                 }
 109                         }
 110                         i=row;
 111                         j=col;
 112                         while(i<N && j<N){
 113                                 int indx = i++*N+j++;
 114                                 if(k!=indx && table[indx]>0){
 115                                         return false;
 116                                 }
 117                         }
 118
 119                 }
 120         }
 121         return true;
 122 }
 123
 124 void printValidationStatus(int N, int *table, int size){
 125         if(validateSolution(N, table, size)){
 126                 printf("***CORRECT****\n");
 127         }else{
 128                 printf("***WRONG******\n");
 129         }
 130
 131 }
 132
 133 void printSolution(int N, int *table, int size){
 134         for(int i=0; i<size; i++){
 135                 if(table[i] > 0){
 136                         printf("Q");
 137                 }else{
 138                         printf("*");
 139                 }
 140                 if((i+1)%N==0){
 141                         printf("\n");
 142                 }
 143         }
 144         printf("\n");
 145 }
 146
 147 void originalNqueensEncoding(int N){
 148         int numVars = N*N;
 149         int kk=1;
 150         int ** VarName = new int * [N];
 151         for (int i=0; i<N; i++){
 152                 VarName[i] = new int [N];
 153                 for (int j=0; j<N; j++){
 154                         VarName[i][j] = kk++;
 155                 }
 156         }
 157
 158         int numFormula = 0;
 159         vector< vector<int> > cnf;
 160
 161         vector<int> vars;
 162
 163         // generator formula per row
 164         // v1 + v2 + v3 + v4 + ... = 1r
 165         for (int i=0; i<N; i++){
 166                 for (int j=0; j<N; j++){
 167                         vars.push_back(VarName[i][j]);
 168                 }
 169                 EqualOneToCNF(vars, cnf);
 170                 vars.clear();
 171         }
 172
 173         // generator formula per col
 174         // v1 + v2 + v3 + v4 + ... = 1r
 175         for (int i=0; i<N; i++){
 176                 for (int j=0; j<N; j++){
 177                         vars.push_back(VarName[j][i]);
 178                 }
 179                 EqualOneToCNF(vars, cnf);
 180                 vars.clear();
 181         }
 182
 183         // diagonal
 184         for (int i=0; i<N-1; i++){
 185                 for (int j=0; j<N-i; j++){
 186                         vars.push_back(VarName[j][i+j]);
 187                 }
 188                 LessEqualOneToCNF(vars, cnf);
 189                 vars.clear();
 190         }
 191         for (int i=1; i<N-1; i++){
 192                 for (int j=0; j<N-i; j++){
 193                         vars.push_back(VarName[j+i][j]);
 194                 }
 195                 LessEqualOneToCNF(vars, cnf);
 196                 vars.clear();
 197         }
 198         for (int i=0; i<N-1; i++){
 199                 for (int j=0; j<N-i; j++){
 200                         vars.push_back(VarName[j][N-1 - (i+j)]);
 201                 }
 202                 LessEqualOneToCNF(vars, cnf);
 203                 vars.clear();
 204         }
 205         for (int i=1; i<N-1; i++){
 206                 for (int j=0; j<N-i; j++){
 207                         vars.push_back(VarName[j+i][N-1-j]);
 208                 }
 209                 LessEqualOneToCNF(vars, cnf);
 210                 vars.clear();
 211         }
 212
 213         //Symmetry breaking constraint
 214         int mid = 1+ ((N-1)/2);
 215         for (int i=0; i<mid; i++){
 216                 vars.push_back(VarName[0][i]);
 217         }
 218         Or(vars, cnf);
 219         vector<int> lastCol;
 220         for(int i=0; i<N; i++){
 221                 lastCol.push_back(VarName[N-1][i]);
 222         }
 223         verticalSymmetryBreaking(vars, lastCol, cnf);
 224         vars.clear();
 225         //That's it ... Let's solve the problem ...
 226         IncrementalSolver *solver =allocIncrementalSolver();
 227
 228         for (int i=0; i<cnf.size(); i++){
 229                 addArrayClauseLiteral(solver, cnf[i].size(), cnf[i].data());
 230         }
 231         finishedClauses(solver);
 232         int start_s=clock();
 233         int result = solve(solver);
 234         int stop_s=clock();
 235         cout << "SAT Solving time: " << (stop_s-start_s)/double(CLOCKS_PER_SEC)*1000 << " ms" << endl;
 236         switch(result){
 237                 case IS_UNSAT:
 238                         printf("Problem is unsat\n");
 239                         break;
 240                 case IS_SAT:{
 241                         printSolution(N, &solver->solution[1], solver->solutionsize);
 242                         printValidationStatus(N, &solver->solution[1], solver->solutionsize);
 243                         break;
 244                 }
 245                 default:
 246                         printf("Unknown results from SAT Solver...\n");
 247
 248         }
 249         deleteIncrementalSolver(solver);
 250 }
 251
 252
 253 void csolverNQueensSub(int N, bool serialize=false){
 254         CSolver *solver = new CSolver();
 255         uint64_t domain[N];
 256         for(int i=0; i<N; i++){
 257                 domain[i] = i;
 258         }
 259         uint64_t range[2*N-1];
 260         for(int i=0; i<2*N-1; i++){
 261                 range[i] = i-N+1;
 262         }
 263         Set *domainSet = solver->createSet(1, domain, N);
 264         Set *rangeSet = solver->createSet(1, range, 2*N-1);
 265         vector<Element *> Xs;
 266         vector<Element *> Ys;
 267         for(int i=0; i<N; i++){
 268                 Xs.push_back(solver->getElementVar(domainSet));
 269                 Ys.push_back(solver->getElementVar(domainSet));
 270         }
 271         Set *d1[] = {domainSet, domainSet};
 272         Function *sub = solver->createFunctionOperator(SATC_SUB, rangeSet, SATC_NOOVERFLOW);
 273         //X shouldn't be equal
 274         for(int i=0; i<N-1; i++){
 275                 for(int j=i+1; j<N; j++ ){
 276                         Element *e1x = Xs[i];
 277                         Element *e2x = Xs[j];
 278                         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 279                         Element *inputs2 [] = {e1x, e2x};
 280                         BooleanEdge equals = solver->applyPredicate(eq, inputs2, 2);
 281                         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, equals));
 282                 }
 283         }
 284         //Y shouldn't be equal
 285         for(int i=0; i<N-1; i++){
 286                 for(int j=i+1; j<N; j++ ){
 287                         Element *e1y = Ys[i];
 288                         Element *e2y = Ys[j];
 289                         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 290                         Element *inputs2 [] = {e1y, e2y};
 291                         BooleanEdge equals = solver->applyPredicate(eq, inputs2, 2);
 292                         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, equals));
 293                 }
 294         }
 295         //vertical difference and horizontal difference shouldn't be equal  shouldn't be equal
 296         BooleanEdge overflow = solver->getBooleanVar(2);
 297         Set *d2[] = {rangeSet, rangeSet};
 298         for(int i=0; i<N-1; i++){
 299                 for(int j=i+1; j<N; j++ ){
 300                         Element *e1y = Ys[i];
 301                         Element *e2y = Ys[j];
 302                         Element *e1x = Xs[i];
 303                         Element *e2x = Xs[j];
 304                         Function *f1 = solver->createFunctionOperator(SATC_SUB, rangeSet, SATC_IGNORE);
 305                         Element *in1[] = {e1x, e2x};
 306                         Element *subx = solver->applyFunction(f1, in1, 2, overflow);
 307                         Element *in2[] = {e1y, e2y};
 308                         Element *suby = solver->applyFunction(f1, in2, 2, overflow);
 309                         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 310                         Element *inputs2 [] = {subx, suby};
 311                         BooleanEdge equals = solver->applyPredicate(eq, inputs2, 2);
 312                         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, equals));
 313                 }
 314         }
 315         if (serialize){
 316                 solver->serialize();
 317         }
 318         if (solver->solve() != 1){
 319                 printf("Problem is Unsolvable ...\n");
 320         }else {
 321                 int table[N*N];
 322                 memset( table, 0, N*N*sizeof(int) );
 323                 for(int i=0; i<N; i++){
 324                         uint x = solver->getElementValue(Xs[i]);
 325                         uint y = solver->getElementValue(Ys[i]);
 326 //                      printf("X=%d, Y=%d\n", x, y);
 327                         ASSERT(N*x+y < N*N);
 328                         table[N*x+y] = 1;
 329                 }
 330                 printSolution(N, table, N*N);
 331                 printValidationStatus(N, table, N*N);
 332         }
 333         delete solver;
 334 }
 335
 336 void atmostOneConstraint(CSolver *solver, vector<BooleanEdge> &constraints){
 337         int size = constraints.size();
 338         if(size <1){
 339                 return;
 340         } else if(size ==1){
 341                 solver->addConstraint(constraints[0]);
 342         }else{
 343 //              solver->addConstraint(solver->applyLogicalOperation(SATC_OR, &constraints[0], size))
 344                 for(int i=0; i<size-1; i++){
 345                         for(int j=i+1; j<size; j++){
 346                                 BooleanEdge const1 = solver->applyLogicalOperation(SATC_NOT, constraints[i]);
 347                                 BooleanEdge const2 = solver->applyLogicalOperation(SATC_NOT, constraints[j]);
 348                                 BooleanEdge array[] = {const1, const2};
 349                                 solver->addConstraint( solver->applyLogicalOperation(SATC_OR, (BooleanEdge *)array, 2));
 350                         }
 351                 }
 352
 353         }
 354 }
 355
 356 void mustHaveValueConstraint(CSolver* solver, vector<Element*> &elems){
 357         for(int i=0; i<elems.size(); i++){
 358                 solver->mustHaveValue(elems[i]);
 359         }
 360 }
 361
 362 void differentInEachRow(CSolver* solver, int N, vector<Element*> &elems){
 363         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 364         for(int i=0; i<N-1; i++){
 365                 for(int j=i+1; j<N; j++ ){
 366                         Element *e1x = elems[i];
 367                         Element *e2x = elems[j];
 368                         Element *inputs2 [] = {e1x, e2x};
 369                         BooleanEdge equals = solver->applyPredicate(eq, inputs2, 2);
 370                         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, equals));
 371                 }
 372         }
 373
 374
 375 }
 376
 377 void oneQueenInEachRow(CSolver* solver, vector<Element*> &elems){
 378         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 379         int N = elems.size();
 380         for(int i=0; i<N; i++){
 381                 vector<BooleanEdge> rowConstr;
 382                 for(int j=0; j<N; j++){
 383                         Element* e1 = elems[j];
 384                         Element* e2 = solver->getElementConst(3, (uint64_t) i);
 385                         Element* in[] = {e1, e2};
 386                         BooleanEdge equals = solver->applyPredicate(eq, in, 2);
 387                         rowConstr.push_back(equals);
 388                 }
 389                 if(rowConstr.size()>0){
 390                         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, &rowConstr[0], rowConstr.size()) );
 391                 }
 392         }
 393 }
 394
 395 void generateRowConstraints(CSolver* solver, int N, vector<Element*> &elems){
 396         oneQueenInEachRow(solver, elems);
 397         differentInEachRow(solver, N, elems);
 398 }
 399
 400 void diagonallyDifferentConstraint(CSolver *solver, int N, vector<Element*> &elems){
 401         Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 402         for(int i=N-1; i>0; i--){
 403 //              cout << "i:" << i << "\t";
 404                 vector<BooleanEdge> diagonals;
 405                 for(int j=i; j>=0; j--){
 406                         int index = i-j;
 407                         Element* e1 = elems[index];
 408 //                      cout << "e" << e1 <<"=" << j << ", ";
 409                         Element* e2 = solver->getElementConst(2, (uint64_t) j);
 410                         Element* in[] = {e1, e2};
 411                         BooleanEdge equals = solver->applyPredicate(eq, in, 2);
 412                         diagonals.push_back(equals);
 413
 414                 }
 415 //              cout << endl;
 416                 atmostOneConstraint(solver, diagonals);
 417         }
 418         for(int i=1; i< N-1; i++){
 419 //              cout << "i:" << i << "\t";
 420                 vector<BooleanEdge> diagonals;
 421                 for(int j=i; j<N; j++){
 422                         int index =N-1- (j-i);
 423                         Element* e1 = elems[index];
 424 //                      cout << "e" << e1 <<"=" << j << ", ";
 425                         Element* e2 = solver->getElementConst(2, (uint64_t) j);
 426                         Element* in[] = {e1, e2};
 427                         BooleanEdge equals = solver->applyPredicate(eq, in, 2);
 428                         diagonals.push_back(equals);
 429
 430                 }
 431 //              cout << endl;
 432                 atmostOneConstraint(solver, diagonals);
 433
 434         }
 435
 436 }
 437
 438 void diagonallyDifferentConstraintBothDir(CSolver *solver, int N, vector<Element*> &elems){
 439         diagonallyDifferentConstraint(solver, N, elems);
 440         reverse(elems.begin(), elems.end());
 441 //      cout << "Other Diagonal:" << endl;
 442         diagonallyDifferentConstraint(solver, N, elems);
 443 }
 444
 445 void symmetryBreakingConstraint(CSolver *solver, int N, vector<Element*>& elems){
 446         Predicate *lt = solver->createPredicateOperator(SATC_LT);
 447         int mid = N/2 + N%2;
 448         Element *e1x = elems[0];
 449         Element *e2x = solver->getElementConst(2, mid);
 450         Element *inputs [] = {e1x, e2x};
 451         solver->addConstraint(solver->applyPredicate(lt, inputs, 2));
 452
 453         e2x = elems[N-1];
 454         Element *inputs2 [] = {e1x, e2x};
 455         BooleanEdge equals = solver->applyPredicate(lt, inputs2, 2);
 456         solver->addConstraint(equals);
 457
 458 }
 459
 460 void csolverNQueens(int N, bool serialize=false){
 461         if(N <=1){
 462                 cout<<"Q" << endl;
 463                 return;
 464         }
 465         CSolver *solver = new CSolver();
 466         uint64_t domain[N];
 467         for(int i=0; i<N; i++){
 468                 domain[i] = i;
 469         }
 470         Set *domainSet = solver->createSet(1, domain, N);
 471         vector<Element *> elems;
 472         for(int i=0; i<N; i++){
 473                 elems.push_back(solver->getElementVar(domainSet));
 474         }
 475         mustHaveValueConstraint(solver, elems);
 476         generateRowConstraints(solver, N, elems);
 477         diagonallyDifferentConstraintBothDir(solver, N, elems);
 478         symmetryBreakingConstraint(solver, N, elems);
 479 //      solver->printConstraints();
 480         if(serialize){
 481                 solver->serialize();
 482         }
 483         if (solver->solve() != 1){
 484                 printf("Problem is Unsolvable ...\n");
 485         }else {
 486                 int table[N*N];
 487                 memset( table, 0, N*N*sizeof(int) );
 488                 for(int i=0; i<N; i++){
 489                         uint x = solver->getElementValue(elems[i]);
 490 //                      printf("X=%d, Y=%d\n", x, i);
 491                         ASSERT(N*x+i < N*N);
 492                         table[N*x+i] = 1;
 493                 }
 494                 printSolution(N, table, N*N);
 495                 printValidationStatus(N, table, N*N);
 496         }
 497         delete solver;
 498 }
 499
 500
 501
 502 int main(int argc, char * argv[]){
 503         if(argc < 2){
 504                 printf("Two arguments are needed\n./nqueen <size> [--csolver]\n");
 505                 exit(-1);
 506         }
 507         int N = atoi(argv[1]);
 508         if(argc <3){
 509                 printf("Running the original encoding ...\n");
 510                 originalNqueensEncoding(N);
 511         }else if( strcmp( argv[2], "--csolver") == 0){
 512                 printf("Running the CSolver encoding ...\n");
 513                 csolverNQueens(N);
 514         }else if (strcmp( argv[2], "--dump") == 0){
 515                 printf("Running the CSolver encoding ...\n");
 516                 csolverNQueens(N, true);
 517         }else {
 518                 printf("Unknown argument %s", argv[2]);
 519         }
 520         return 0;
 521 }