glucose-syrup/parallel/MultiSolvers.cc

   1 /***************************************************************************************[MultiSolvers.cc]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50 #include <pthread.h>
  51 #include "parallel/MultiSolvers.h"
  52 #include "mtl/Sort.h"
  53 #include "utils/System.h"
  54 #include "simp/SimpSolver.h"
  55 #include <errno.h>
  56 #include <string.h>
  57 #include "parallel/SolverConfiguration.h"
  58
  59 using namespace Glucose;
  60
  61 extern const char* _parallel ;
  62 extern const char* _cunstable;
  63 // Options at the parallel solver level
  64 static IntOption opt_nbsolversmultithreads (_parallel, "nthreads", "Number of core threads for syrup (0 for automatic)", 0);
  65 static IntOption opt_maxnbsolvers (_parallel, "maxnbthreads", "Maximum number of core threads to ask for (when nbthreads=0)", 4);
  66 static IntOption opt_maxmemory    (_parallel, "maxmemory", "Maximum memory to use (in Mb, 0 for no software limit)", 3000);
  67 static IntOption opt_statsInterval (_parallel, "statsinterval", "Seconds (real time) between two stats reports", 5);
  68 //
  69 // Shared with ClausesBuffer.cc
  70 BoolOption opt_whenFullRemoveOlder (_parallel, "removeolder", "When the FIFO for exchanging clauses between threads is full, remove older clauses", false);
  71 IntOption opt_fifoSizeByCore(_parallel, "fifosize", "Size of the FIFO structure for exchanging clauses between threads, by threads", 100000);
  72 //
  73 // Shared options with Solver.cc
  74 BoolOption    opt_dontExportDirectReusedClauses (_cunstable, "reusedClauses",    "Don't export directly reused clauses", false);
  75 BoolOption    opt_plingeling (_cunstable, "plingeling",    "plingeling strategy for sharing clauses (exploratory feature)", false);
  76
  77 #include <sys/time.h>
  78 #include <sys/resource.h>
  79 #include <unistd.h>
  80
  81 static inline double cpuTime(void) {
  82     struct rusage ru;
  83     getrusage(RUSAGE_SELF, &ru);
  84 return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
  85
  86
  87 void MultiSolvers::informEnd(lbool res) {
  88   result = res;
  89   pthread_cond_broadcast(&cfinished);
  90 }
  91
  92 MultiSolvers::MultiSolvers(ParallelSolver *s):
  93   ok (true)
  94   , maxnbthreads(4), nbthreads(opt_nbsolversmultithreads), nbsolvers(opt_nbsolversmultithreads)
  95   , nbcompanions(4), nbcompbysolver(2)
  96   , allClonesAreBuilt(0)
  97   , showModel(false)
  98   , winner(-1)
  99   , var_decay(1 / 0.95), clause_decay(1 / 0.999),cla_inc(1), var_inc(1)
 100   , random_var_freq(0.02)
 101   , restart_first(100), restart_inc(1.5)
 102   , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
 103   , expensive_ccmin(true)
 104   , polarity_mode    (polarity_false)
 105   , maxmemory(opt_maxmemory), maxnbsolvers(opt_maxnbsolvers)
 106   , verb(0) , verbEveryConflicts(10000)
 107   , numvar(0), numclauses(0)
 108
 109 {
 110     result = l_Undef;
 111     SharedCompanion *sc = new SharedCompanion();
 112     this->sharedcomp = sc;
 113
 114     // Generate only solver 0.
 115     // It loads the formula
 116     // All others solvers are clone of this one
 117     solvers.push(s);
 118     s->verbosity = 0; // No reportf in solvers... All is done in MultiSolver
 119     s->setThreadNumber(0);
 120     //s->belongsto = this;
 121     s->sharedcomp = sc;
 122     sc->addSolver(s);
 123     assert(solvers[0]->threadNumber() == 0);
 124
 125     pthread_mutex_init(&m,NULL);  //PTHREAD_MUTEX_INITIALIZER;
 126     pthread_mutex_init(&mfinished,NULL); //PTHREAD_MUTEX_INITIALIZER;
 127     pthread_cond_init(&cfinished,NULL);
 128
 129     if (nbsolvers > 0 )
 130         fprintf(stdout,"c %d solvers engines and 1 companion as a blackboard created.\n", nbsolvers);
 131 }
 132
 133 MultiSolvers::MultiSolvers() : MultiSolvers(new ParallelSolver(-1)) {
 134
 135 }
 136
 137 MultiSolvers::~MultiSolvers()
 138 {}
 139
 140 /**
 141  * Generate All solvers
 142  */
 143
 144 void MultiSolvers::generateAllSolvers() {
 145     assert(solvers[0] != NULL);
 146     assert(allClonesAreBuilt==0);
 147
 148     for(int i=1;i<nbsolvers;i++) {
 149         ParallelSolver *s  = (ParallelSolver*)solvers[0]->clone();
 150         solvers.push(s);
 151         s->verbosity = 0; // No reportf in solvers... All is done in MultiSolver
 152         s->setThreadNumber(i);
 153         s->sharedcomp =   this->sharedcomp;
 154         this->sharedcomp->addSolver(s);
 155         assert(solvers[i]->threadNumber() == i);
 156     }
 157
 158     adjustParameters();
 159
 160     allClonesAreBuilt = 1;
 161 }
 162
 163 /**
 164  * Choose solver for threads i (if no given in command line see above)
 165  */
 166
 167
 168 ParallelSolver* MultiSolvers::retrieveSolver(int i) {
 169     return new ParallelSolver(i);
 170 }
 171
 172 Var MultiSolvers::newVar(bool sign, bool dvar)
 173 {
 174   assert(solvers[0] != NULL);
 175   numvar++;
 176   int v;
 177   sharedcomp->newVar(sign);
 178   if(!allClonesAreBuilt) { // At the beginning we want to generate only solvers 0
 179     v = solvers[0]->newVar(sign,dvar);
 180     assert(numvar == v+1); // Just a useless check
 181   } else {
 182       for(int i=0;i<nbsolvers;i++) {
 183           v = solvers[i]->newVar(sign,dvar);
 184       }
 185   }
 186   return numvar;
 187 }
 188
 189 bool MultiSolvers::addClause_(vec<Lit>&ps) {
 190   assert(solvers[0] != NULL); // There is at least one solver.
 191   // Check if clause is satisfied and remove false/duplicate literals:
 192   if (!okay())  return false;
 193
 194   sort(ps);
 195   Lit p; int i, j;
 196   for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
 197     if (solvers[0]->value(ps[i]) == l_True || ps[i] == ~p)
 198       return true;
 199     else if (solvers[0]->value(ps[i]) != l_False && ps[i] != p)
 200       ps[j++] = p = ps[i];
 201   ps.shrink(i - j);
 202
 203
 204   if (ps.size() == 0) {
 205     return ok = false;
 206   }
 207   else if (ps.size() == 1){
 208     assert(solvers[0]->value(ps[0]) == l_Undef); // TODO : Passes values to all threads
 209     solvers[0]->uncheckedEnqueue(ps[0]);
 210     if(!allClonesAreBuilt) {
 211         return ok = ( (solvers[0]->propagate()) == CRef_Undef); // checks only main solver here for propagation constradiction
 212     }
 213
 214     // Here, all clones are built.
 215     // Gives the unit clause to everybody
 216     for(int i=0;i<nbsolvers;i++)
 217       solvers[i]->uncheckedEnqueue(ps[0]);
 218     return ok = ( (solvers[0]->propagate()) == CRef_Undef); // checks only main solver here for propagation constradiction
 219   }else{
 220     //          printf("Adding clause %0xd for solver %d.\n",(void*)c, thn);
 221     // At the beginning only solver 0 load the formula
 222     solvers[0]->addClause(ps);
 223
 224     if(!allClonesAreBuilt) {
 225         numclauses++;
 226         return true;
 227     }
 228     // Clones are built, need to pass the clause to all the threads
 229     for(int i=1;i<nbsolvers;i++) {
 230       solvers[i]->addClause(ps);
 231     }
 232     numclauses++;
 233   }
 234   return true;
 235 }
 236
 237
 238 bool MultiSolvers::simplify() {
 239   assert(solvers[0] != NULL); // There is at least one solver.
 240
 241   if (!okay()) return false;
 242   return ok = solvers[0]->simplify();
 243 }
 244
 245
 246 bool MultiSolvers::eliminate() {
 247
 248     // TODO allow variable elimination when all threads are built!
 249     assert(allClonesAreBuilt==false);
 250
 251     SimpSolver * s = (SimpSolver*)getPrimarySolver();
 252     return s->eliminate(true);
 253 }
 254
 255
 256 // TODO: Use a template here
 257 void *localLaunch(void*arg) {
 258   ParallelSolver* s = (ParallelSolver*)arg;
 259
 260   (void)s->solve();
 261
 262   pthread_exit(NULL);
 263 }
 264
 265
 266 #define MAXIMUM_SLEEP_DURATION 5
 267 void MultiSolvers::printStats() {
 268         static int nbprinted = 1;
 269         double cpu_time = cpuTime();
 270     printf("c\n");
 271
 272     printf("c |-------------------------------------------------------------------------------------------------------|\n");
 273         printf("c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %%   | \n");
 274         printf("c |-------------------------------------------------------------------------------------------------------|\n");
 275
 276         //printf("%.0fs | ",cpu_time);
 277         for(int i=0;i<solvers.size();i++) {
 278             solvers[i]->reportProgress();
 279     //printf(" %2d: %12ld confl. |", i,  (long int) solvers[i]->conflicts);
 280     }
 281         long long int totalconf = 0;
 282         long long int totalprop = 0;
 283         for(int i=0;i<solvers.size();i++) {
 284                 totalconf+=  (long int) solvers[i]->conflicts;
 285                 totalprop+= solvers[i]->propagations;
 286     }
 287     printf("c \n");
 288
 289     printf("c synthesis %11lld conflicts %11lld propagations %8.0f conflicts/sec %8.0f propagations/sec\n",
 290             totalconf, totalprop, (double)totalconf / cpu_time, (double) totalprop / cpu_time);
 291
 292
 293         nbprinted ++;
 294 }
 295
 296 // Still a ugly function... To be rewritten with some statistics class some day
 297 void MultiSolvers::printFinalStats() {
 298     sharedcomp->printStats();
 299     printf("c\nc\n");
 300     printf("c\n");
 301     printf("c |---------------------------------------- FINAL STATS --------------------------------------------------|\n");
 302     printf("c\n");
 303
 304     printf("c |---------------");
 305     for(int i = 0;i<solvers.size();i++)
 306         printf("|------------");
 307     printf("|-----------------|\n");
 308
 309     printf("c | Threads       ");
 310     for(int i = 0;i < solvers.size();i++) {
 311         printf("| %10d ",i);
 312     }
 313     printf("|      Total      |\n");
 314
 315     printf("c |---------------");
 316     for(int i = 0;i<solvers.size();i++)
 317         printf("|------------");
 318     printf("|-----------------|\n");
 319
 320
 321     printf("c | Conflicts     ");
 322
 323     long long int totalconf = 0;
 324     for(int i=0;i<solvers.size();i++)  {
 325         printf("| %10" PRIu64" ", solvers[i]->conflicts);
 326         totalconf +=  solvers[i]->conflicts;
 327     }
 328     printf("| %15lld |\n",totalconf);
 329
 330     printf("c | Exported      ");
 331     uint64_t exported = 0;
 332     for(int i=0;i<solvers.size();i++) {
 333         printf("| %10" PRIu64" ", solvers[i]->nbexported);
 334         exported += solvers[i]->nbexported;
 335     }
 336     printf("| %15" PRIu64" |\n", exported);
 337
 338     printf("c | Imported      ");
 339     uint64_t imported = 0;
 340     for(int i=0;i<solvers.size();i++) {
 341         printf("| %10" PRIu64" ", solvers[i]->nbimported);
 342         imported += solvers[i]->nbimported;
 343     }
 344     printf("| %15" PRIu64" |\n", imported);
 345
 346     printf("c | Good          ");
 347     uint64_t importedGood = 0;
 348     for(int i=0;i<solvers.size();i++) {
 349         printf("| %10" PRIu64" ", solvers[i]->nbImportedGoodClauses);
 350         importedGood += solvers[i]->nbImportedGoodClauses;
 351     }
 352     printf("| %15" PRIu64" |\n", importedGood);
 353
 354     printf("c | Purge         ");
 355     uint64_t importedPurg = 0;
 356     for(int i=0;i<solvers.size();i++) {
 357         printf("| %10" PRIu64" ", solvers[i]->nbimportedInPurgatory);
 358         importedPurg += solvers[i]->nbimportedInPurgatory;
 359     }
 360     printf("| %15" PRIu64" |\n", importedPurg);
 361
 362     printf("c | Promoted      ");
 363     uint64_t promoted = 0;
 364     for(int i=0;i<solvers.size();i++) {
 365         printf("| %10" PRIu64" ", solvers[i]->nbPromoted);
 366         promoted += solvers[i]->nbPromoted;
 367     }
 368     printf("| %15" PRIu64" |\n", promoted);
 369
 370     printf("c | Remove imp    ");
 371     uint64_t removedimported = 0;
 372     for(int i=0;i<solvers.size();i++) {
 373         printf("| %10" PRIu64" ", solvers[i]->nbRemovedUnaryWatchedClauses);
 374         removedimported += solvers[i]->nbRemovedUnaryWatchedClauses;
 375     }
 376     printf("| %15" PRIu64" |\n", removedimported);
 377
 378     printf("c | Blocked Reuse ");
 379     uint64_t blockedreused = 0;
 380     for(int i=0;i<solvers.size();i++) {
 381         printf("| %10" PRIu64" ", solvers[i]->nbNotExportedBecauseDirectlyReused);
 382         blockedreused += solvers[i]->nbNotExportedBecauseDirectlyReused;
 383     }
 384     printf("| %15" PRIu64" |\n",blockedreused);
 385
 386
 387     printf("c | Orig seen     ");
 388     for(int i=0;i<solvers.size();i++) {
 389         printf("| %10" PRIu64" ", solvers[i]->originalClausesSeen);
 390     }
 391     printf("|                 |\n");
 392
 393     printf("c | Unaries       ");
 394     for(int i=0;i<solvers.size();i++) {
 395         printf("| %10" PRIu64" ", solvers[i]->nbUn);
 396     }
 397     printf("|                 |\n");
 398
 399     printf("c | Binaries      ");
 400     for(int i=0;i<solvers.size();i++) {
 401         printf("| %10" PRIu64" ", solvers[i]->nbBin);
 402     }
 403     printf("|                 |\n");
 404
 405
 406      printf("c | Glues         ");
 407     for(int i=0;i<solvers.size();i++) {
 408         printf("| %10" PRIu64" ", solvers[i]->nbDL2);
 409     }
 410     printf("|                 |\n");
 411
 412
 413     int winner = -1;
 414    for(int i=0;i<solvers.size();i++) {
 415      if(sharedcomp->winner()==solvers[i])
 416        winner = i;
 417      }
 418
 419    if(winner!=-1) {
 420 int sum = 0;
 421    printf("c | Hamming       ");
 422    for(int i = 0;i<solvers.size();i++) {
 423      if(i==winner) {
 424        printf("|      X     ");
 425        continue;
 426      }
 427      int nb = 0;
 428      for(int j = 0;j<nVars();j++) {
 429        if(solvers[i]->valuePhase(j)!= solvers[winner]->valuePhase(j)) nb++;
 430      }
 431      printf("| %10d ",nb);
 432      sum+=nb;
 433
 434    }
 435    printf("| %15d |\n",sum/(solvers.size()>1?solvers.size()-1:1));
 436    }
 437
 438    printf("c |---------------");
 439    for(int i = 0;i<solvers.size();i++)
 440      printf("|------------");
 441    printf("|-----------------|\n");
 442
 443
 444
 445 }
 446
 447 // Well, all those parameteres are just naive guesses... No experimental evidences for this.
 448 void MultiSolvers::adjustParameters() {
 449     SolverConfiguration::configure(this,nbsolvers);
 450 }
 451
 452 void MultiSolvers::adjustNumberOfCores() {
 453  float mem = memUsed();
 454   if (nbthreads==0) { // Automatic configuration
 455       if(verb>=1)
 456           printf("c |  Automatic Adjustement of the number of solvers. MaxMemory=%5d, MaxCores=%3d.                       |\n", maxmemory, maxnbsolvers);
 457       unsigned int tmpnbsolvers = maxmemory * 4 /  10 / mem;
 458       if (tmpnbsolvers > maxnbsolvers) tmpnbsolvers = maxnbsolvers;
 459       if (tmpnbsolvers < 1) tmpnbsolvers = 1;
 460       if(verb>=1)
 461         printf("c |  One Solver is taking %.2fMb... Let's take %d solvers for this run (max 40%% of the maxmemory).       |\n", mem, tmpnbsolvers);
 462       nbsolvers = tmpnbsolvers;
 463       nbthreads = nbsolvers;
 464   } else {
 465       assert(nbthreads == nbsolvers);
 466   }
 467 }
 468
 469 lbool MultiSolvers::solve() {
 470   pthread_attr_t thAttr;
 471   int i;
 472
 473   adjustNumberOfCores();
 474   sharedcomp->setNbThreads(nbsolvers);
 475   if(verb>=1)
 476     printf("c |  Generating clones                                                                                    |\n");
 477   generateAllSolvers();
 478   if(verb>=1) {
 479     printf("c |  all clones generated. Memory = %6.2fMb.                                                             |\n", memUsed());
 480     printf("c ========================================================================================================|\n");
 481   }
 482
 483
 484   model.clear();
 485
 486   /* Initialize and set thread detached attribute */
 487   pthread_attr_init(&thAttr);
 488   pthread_attr_setdetachstate(&thAttr, PTHREAD_CREATE_JOINABLE);
 489
 490
 491
 492   // Launching all solvers
 493   for (i = 0; i < nbsolvers; i++) {
 494     pthread_t * pt = (pthread_t*)malloc(sizeof(pthread_t));
 495     threads.push(pt);
 496     solvers[i]->pmfinished = &mfinished;
 497     solvers[i]->pcfinished = &cfinished;
 498     pthread_create(threads[i], &thAttr, &localLaunch, (void*)solvers[i]);
 499   }
 500
 501   bool done = false;
 502
 503   (void)pthread_mutex_lock(&m);
 504   while (!done) {
 505     struct timespec timeout;
 506     time(&timeout.tv_sec);
 507     timeout.tv_sec += MAXIMUM_SLEEP_DURATION;
 508     timeout.tv_nsec = 0;
 509     if (pthread_cond_timedwait(&cfinished, &mfinished, &timeout) != ETIMEDOUT)
 510             done = true;
 511     else
 512       printStats();
 513
 514     float mem = memUsed();
 515     if(verb>=1) printf("c Total Memory so far : %.2fMb\n",  mem);
 516     if ( (maxmemory > 0) && (mem > maxmemory) && !sharedcomp->panicMode)
 517        printf("c ** reduceDB switching to Panic Mode due to memory limitations !\n"), sharedcomp->panicMode = true;
 518
 519   }
 520   (void)pthread_mutex_unlock(&m);
 521
 522   for (i = 0; i < nbsolvers; i++) { // Wait for all threads to finish
 523       pthread_join(*threads[i], NULL);
 524   }
 525
 526   assert(sharedcomp != NULL);
 527   result = sharedcomp->jobStatus;
 528   if (result == l_True) {
 529       int n = sharedcomp->jobFinishedBy->nVars();
 530         model.growTo(n);
 531         for(int i = 0; i < n; i++)
 532             model[i] = sharedcomp->jobFinishedBy->model[i];
 533   }
 534
 535
 536   return result;
 537   /*
 538   for(int i=0;i<NBTHREADS;i++)
 539     pthread_join(*threads[i],&status);
 540   */
 541
 542 }
 543