glucose-syrup/parallel/ParallelSolver.cc

   1 /***************************************************************************************[ParallelSolver.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 "parallel/ParallelSolver.h"
  51 #include "mtl/Sort.h"
  52
  53 using namespace Glucose;
  54
  55 const char* _cunstable = "CORE/PARALLEL -- UNSTABLE FEATURES";
  56 const char* _parallel = "PARALLEL";
  57
  58 extern BoolOption opt_dontExportDirectReusedClauses; // (_cunstable, "reusedClauses",    "Don't export directly reused clauses", false);
  59 extern BoolOption opt_plingeling; // (_cunstable, "plingeling",    "plingeling strategy for sharing clauses (exploratory feature)", false);
  60
  61
  62 ParallelSolver::ParallelSolver(int threadId) :
  63   SimpSolver()
  64 , thn(threadId) // The thread number of this solver
  65 , nbexported(0)
  66 , nbimported(0)
  67 , nbexportedunit(0), nbimportedunit(0), nbimportedInPurgatory(0), nbImportedGoodClauses(0)
  68 , goodlimitlbd(8)
  69 , goodlimitsize(30)
  70 , purgatory(true)
  71 , shareAfterProbation(!opt_plingeling) // only share clauses after probation
  72 , plingeling(opt_plingeling)
  73 , firstSharing(5000) // Strong limit : do not share anything (except unary clauses) before this number of conflicts
  74 , limitSharingByGoodLBD(true) // Moving limit of what a good LBD is (median value of last learnt clauses set)
  75 , limitSharingByFixedLimitLBD(0) // No fixed bound (like 8 in plingeling)
  76 , limitSharingByFixedLimitSize(0) // No fixed boud (like 40 in plingeling)
  77 , dontExportDirectReusedClauses(opt_dontExportDirectReusedClauses)
  78 , nbNotExportedBecauseDirectlyReused(0)
  79 {
  80     useUnaryWatched = true; // We want to use promoted clauses here !
  81 }
  82
  83
  84
  85
  86 ParallelSolver::~ParallelSolver() {
  87     printf("c Solver of thread %d ended.\n", thn);
  88     fflush(stdout);
  89 }
  90
  91 ParallelSolver::ParallelSolver(const ParallelSolver &s) : SimpSolver(s)
  92 , nbexported(s.nbexported)
  93 , nbimported(s.nbimported)
  94 , nbexportedunit(s.nbexportedunit), nbimportedunit(s.nbimportedunit), nbimportedInPurgatory(s.nbimportedInPurgatory)
  95 , nbImportedGoodClauses(s.nbImportedGoodClauses)
  96 , goodlimitlbd(s.goodlimitlbd)
  97 , goodlimitsize(s.goodlimitsize)
  98 , purgatory(s.purgatory)
  99 , shareAfterProbation(s.shareAfterProbation) // only share clauses after probation
 100 , plingeling(s.plingeling)
 101 , firstSharing(s.firstSharing) // Strong limit : do not share anything (except unary clauses) before this number of conflicts
 102 , limitSharingByGoodLBD(s.limitSharingByGoodLBD) // Moving limit of what a good LBD is (median value of last learnt clauses set)
 103 , limitSharingByFixedLimitLBD(s.limitSharingByFixedLimitLBD) // No fixed bound (like 8 in plingeling)
 104 , limitSharingByFixedLimitSize(s.limitSharingByFixedLimitSize) // No fixed boud (like 40 in plingeling)
 105 , dontExportDirectReusedClauses(s.dontExportDirectReusedClauses)
 106 , nbNotExportedBecauseDirectlyReused(s.nbNotExportedBecauseDirectlyReused)
 107 {
 108     s.goodImportsFromThreads.memCopyTo(goodImportsFromThreads);
 109     useUnaryWatched = s.useUnaryWatched;
 110 }
 111
 112
 113 // Strategy to reduce unary watches list
 114 struct reduceDB_oneWatched_lt {
 115     ClauseAllocator& ca;
 116
 117     reduceDB_oneWatched_lt(ClauseAllocator& ca_) : ca(ca_) {
 118     }
 119
 120     bool operator()(CRef x, CRef y) {
 121
 122         // Main criteria... Like in MiniSat we keep all binary clauses
 123         if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
 124
 125         if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
 126         if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
 127
 128         // Second one  based on literal block distance
 129         if (ca[x].size() > ca[y].size()) return 1;
 130         if (ca[x].size() < ca[y].size()) return 0;
 131
 132         if (ca[x].lbd() > ca[y].lbd()) return 1;
 133         if (ca[x].lbd() < ca[y].lbd()) return 0;
 134
 135         // Finally we can use old activity or size, we choose the last one
 136         return ca[x].activity() < ca[y].activity();
 137         //return x->size() < y->size();
 138
 139         //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
 140     }
 141 };
 142
 143 // @overide
 144 void ParallelSolver::reduceDB() {
 145
 146     int i, j;
 147     nbReduceDB++;
 148     sort(learnts, reduceDB_lt(ca));
 149
 150     int limit;
 151
 152     if (!panicModeIsEnabled()) {
 153         // We have a lot of "good" clauses, it is difficult to compare them. Keep more !
 154         if (ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialIncReduceDB;
 155         // Useless :-)
 156         if (ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB;
 157
 158         // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
 159         // Keep clauses which seem to be usefull (their lbd was reduce during this sequence)
 160
 161         limit = learnts.size() / 2;
 162     } else {
 163         limit = panicModeLastRemoved;
 164     }
 165     panicModeLastRemoved = 0;
 166
 167     uint64_t sumsize = 0;
 168     for (i = j = 0; i < learnts.size(); i++) {
 169
 170         Clause& c = ca[learnts[i]];
 171         if (i == learnts.size() / 2)
 172             goodlimitlbd = c.lbd();
 173         sumsize += c.size();
 174         if (c.lbd() > 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) {
 175             removeClause(learnts[i]);
 176             nbRemovedClauses++;
 177             panicModeLastRemoved++;
 178         } else {
 179             if (!c.canBeDel()) limit++; //we keep c, so we can delete an other clause
 180             c.setCanBeDel(true); // At the next step, c can be delete
 181             learnts[j++] = learnts[i];
 182         }
 183     }
 184     learnts.shrink(i - j);
 185
 186     if (learnts.size() > 0)
 187         goodlimitsize = 1 + (double) sumsize / (double) learnts.size();
 188
 189     // Special treatment for imported clauses
 190     if (!panicModeIsEnabled())
 191         limit = unaryWatchedClauses.size() - (learnts.size() * 2);
 192     else
 193         limit = panicModeLastRemovedShared;
 194     panicModeLastRemovedShared = 0;
 195     if ((unaryWatchedClauses.size() > 100) && (limit > 0)) {
 196
 197         sort(unaryWatchedClauses, reduceDB_oneWatched_lt(ca));
 198
 199         for (i = j = 0; i < unaryWatchedClauses.size(); i++) {
 200             Clause& c = ca[unaryWatchedClauses[i]];
 201             if (c.lbd() > 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) {
 202                 removeClause(unaryWatchedClauses[i], c.getOneWatched()); // remove from the purgatory (or not)
 203                 nbRemovedUnaryWatchedClauses++;
 204                 panicModeLastRemovedShared++;
 205             } else {
 206                 if (!c.canBeDel()) limit++; //we keep c, so we can delete an other clause
 207                 c.setCanBeDel(true); // At the next step, c can be delete
 208                 unaryWatchedClauses[j++] = unaryWatchedClauses[i];
 209             }
 210         }
 211         unaryWatchedClauses.shrink(i - j);
 212     }
 213
 214     checkGarbage();
 215 }
 216
 217
 218 /*_________________________________________________________________________________________________
 219 |
 220 |  parallelImportClauseDuringConflictAnalysis : (Clause &c,CRef confl)   ->  [void]
 221 |
 222 |  Description:
 223 |    Verify if the clause using during conflict analysis is good for export
 224 |    @see : analyze
 225 |  Output:
 226 |________________________________________________________________________________________________@*/
 227
 228
 229 void ParallelSolver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) {
 230     if (dontExportDirectReusedClauses && (confl == lastLearntClause) && (c.getExported() < 2)) { // Experimental stuff
 231         c.setExported(2);
 232         nbNotExportedBecauseDirectlyReused++;
 233     } else if (shareAfterProbation && c.getExported() != 2 && conflicts > firstSharing) {
 234         c.setExported(c.getExported() + 1);
 235         if (!c.wasImported() && c.getExported() == 2) { // It's a new interesting clause:
 236             if (c.lbd() == 2 || (c.size() < goodlimitsize && c.lbd() <= goodlimitlbd)) {
 237                 shareClause(c);
 238             }
 239         }
 240     }
 241
 242 }
 243
 244
 245
 246 // These Two functions are useless here !!
 247 void ParallelSolver::reportProgress() {
 248     printf("c | %2d | %6d | %10d | %10d | %8d | %8d | %8d | %8d | %8d | %6.3f |\n",(int)thn,(int)starts,(int)decisions,(int)conflicts,(int)originalClausesSeen,(int)learnts.size(),(int)nbexported,(int)nbimported,(int)nbPromoted,progressEstimate()*100);
 249
 250     //printf("c thread=%d confl=%lld starts=%llu reduceDB=%llu learnts=%d broadcast=%llu  blockedReuse=%lld imported=%llu promoted=%llu limitlbd=%llu limitsize=%llu\n", thn, conflicts, starts, nbReduceDB, learnts.size(), nbexported, nbNotExportedBecauseDirectlyReused, nbimported, nbPromoted, goodlimitlbd, goodlimitsize);
 251 }
 252
 253 void ParallelSolver::reportProgressArrayImports(vec<unsigned int> &totalColumns) {
 254     return ; // TODO : does not currently work
 255     unsigned int totalImports = 0;
 256     printf("c %3d | ", thn);
 257     for (int i = 0; i <  sharedcomp->nbThreads; i++) {
 258         totalImports += goodImportsFromThreads[i];
 259         totalColumns[i] += goodImportsFromThreads[i];
 260         printf(" %8d", goodImportsFromThreads[i]);
 261     }
 262     printf(" | %8d\n", totalImports);
 263
 264 }
 265
 266
 267
 268 /*_________________________________________________________________________________________________
 269 |
 270 |  shareClause : (Clause &c)   ->  [bool]
 271 |
 272 |  Description:
 273 |  share a clause to other cores
 274 | @see : analyze
 275 |  Output: true if the clause is indeed sent
 276 |________________________________________________________________________________________________@*/
 277
 278 bool ParallelSolver::shareClause(Clause & c) {
 279     bool sent = sharedcomp->addLearnt(this, c);
 280     if (sent)
 281         nbexported++;
 282     return sent;
 283 }
 284
 285 /*_________________________________________________________________________________________________
 286 |
 287 |  panicModeIsEnabled : ()   ->  [bool]
 288 |
 289 |  Description:
 290 |  is panic mode (save memory) is enabled ?
 291 |________________________________________________________________________________________________@*/
 292
 293 bool ParallelSolver::panicModeIsEnabled() {
 294     return sharedcomp->panicMode;
 295 }
 296
 297 /*_________________________________________________________________________________________________
 298 |
 299 |  parallelImportUnaryClauses : ()   ->  [void]
 300 |
 301 |  Description:
 302 |  import all unary clauses from other cores
 303 |________________________________________________________________________________________________@*/
 304
 305 void ParallelSolver::parallelImportUnaryClauses() {
 306     Lit l;
 307     while ((l = sharedcomp->getUnary(this)) != lit_Undef) {
 308         if (value(var(l)) == l_Undef) {
 309             uncheckedEnqueue(l);
 310             nbimportedunit++;
 311         }
 312     }
 313 }
 314
 315 /*_________________________________________________________________________________________________
 316 |
 317 |  parallelImportClauses : ()   ->  [bool]
 318 |
 319 |  Description:
 320 |  import all clauses from other cores
 321 |  Output : if there is a final conflict
 322 |________________________________________________________________________________________________@*/
 323
 324 bool ParallelSolver::parallelImportClauses() {
 325
 326     assert(decisionLevel() == 0);
 327     int importedFromThread;
 328     while (sharedcomp->getNewClause(this, importedFromThread, importedClause)) {
 329         assert(importedFromThread <= sharedcomp->nbThreads);
 330         assert(importedFromThread >= 0);
 331
 332         assert(importedFromThread != thn);
 333
 334         if (importedClause.size() == 0)
 335             return true;
 336
 337         //printf("Thread %d imports clause from thread %d\n", threadNumber(), importedFromThread);
 338         CRef cr = ca.alloc(importedClause, true, true);
 339         ca[cr].setLBD(importedClause.size());
 340         if (plingeling) // 0 means a broadcasted clause (good clause), 1 means a survivor clause, broadcasted
 341             ca[cr].setExported(2); // A broadcasted clause (or a survivor clause) do not share it anymore
 342         else {
 343             ca[cr].setExported(1); // next time we see it in analyze, we share it (follow route / broadcast depending on the global strategy, part of an ongoing experimental stuff: a clause in one Watched will be set to exported 2 when promotted.
 344         }
 345         ca[cr].setImportedFrom(importedFromThread);
 346         unaryWatchedClauses.push(cr);
 347         if (plingeling || ca[cr].size() <= 2) {//|| importedRoute == 0) { // importedRoute == 0 means a glue clause in another thread (or any very good clause)
 348             ca[cr].setOneWatched(false); // Warning: those clauses will never be promoted by a conflict clause (or rarely: they are propagated!)
 349             attachClause(cr);
 350             nbImportedGoodClauses++;
 351         } else {
 352             ca[cr].setOneWatched(true);
 353             attachClausePurgatory(cr); //
 354             nbimportedInPurgatory++;
 355         }
 356         assert(ca[cr].learnt());
 357         nbimported++;
 358     }
 359     return false;
 360 }
 361
 362
 363 /*_________________________________________________________________________________________________
 364 |
 365 |  parallelExportUnaryClause : (Lit p)   ->  [void]
 366 |
 367 |  Description:
 368 |  export unary clauses to other cores
 369 |________________________________________________________________________________________________@*/
 370
 371 void ParallelSolver::parallelExportUnaryClause(Lit p) {
 372     // Multithread
 373     sharedcomp->addLearnt(this,p ); // TODO: there can be a contradiction here (two theads proving a and -a)
 374     nbexportedunit++;
 375 }
 376
 377
 378 /*_________________________________________________________________________________________________
 379 |
 380 |  parallelExportClauseDuringSearch : (Clause &c)   ->  [void]
 381 |
 382 |  Description:
 383 |  Verify if a new learnt clause is useful for export
 384 |  @see search
 385 |
 386 |________________________________________________________________________________________________@*/
 387
 388 void ParallelSolver::parallelExportClauseDuringSearch(Clause &c) {
 389     //
 390     // Multithread
 391     // Now I'm sharing the clause if seen in at least two conflicts analysis shareClause(ca[cr]);
 392     if ((plingeling && !shareAfterProbation && c.lbd() < 8 && c.size() < 40) ||
 393             (c.lbd() <= 2)) { // For this class of clauses, I'm sharing them asap (they are Glue CLauses, no probation for them)
 394         shareClause(c);
 395         c.setExported(2);
 396     }
 397
 398 }
 399
 400
 401 /*_________________________________________________________________________________________________
 402 |
 403 |  parallelJobIsFinished : ()   ->  [bool]
 404 |
 405 |  Description:
 406 |  Is a core already finish the search
 407 |
 408 |________________________________________________________________________________________________@*/
 409
 410 bool ParallelSolver::parallelJobIsFinished() {
 411     // Parallel: another job has finished let's quit
 412     return (sharedcomp->jobFinished());
 413 }
 414
 415 // @overide
 416 lbool ParallelSolver::solve_(bool do_simp, bool turn_off_simp) {
 417        vec<Var> extra_frozen;
 418     lbool    result = l_True;
 419     do_simp &= use_simplification;
 420     if (do_simp){
 421         // Assumptions must be temporarily frozen to run variable elimination:
 422         for (int i = 0; i < assumptions.size(); i++){
 423             Var v = var(assumptions[i]);
 424
 425             // If an assumption has been eliminated, remember it.
 426             assert(!isEliminated(v));
 427
 428             if (!frozen[v]){
 429                 // Freeze and store.
 430                 setFrozen(v, true);
 431                 extra_frozen.push(v);
 432             } }
 433
 434         result = lbool(eliminate(turn_off_simp));
 435     }
 436
 437     model.clear();
 438     conflict.clear();
 439     if (!ok) return l_False;
 440
 441     solves++;
 442
 443
 444     lbool status = l_Undef;
 445
 446     // Search:
 447     int curr_restarts = 0;
 448     while (status == l_Undef && !sharedcomp->jobFinished()) {
 449         status = search(0); // the parameter is useless in glucose, kept to allow modifications
 450         if (!withinBudget()) break;
 451         curr_restarts++;
 452     }
 453
 454     if (verbosity >= 1)
 455         printf("c =========================================================================================================\n");
 456
 457
 458 /*    if (do_simp)
 459         // Unfreeze the assumptions that were frozen:
 460         for (int i = 0; i < extra_frozen.size(); i++)
 461             setFrozen(extra_frozen[i], false);
 462 */
 463
 464     bool firstToFinish = false;
 465     if (status != l_Undef)
 466         firstToFinish = sharedcomp->IFinished(this);
 467     if (firstToFinish) {
 468         printf("c Thread %d is 100%% pure glucose! First thread to finish! (%s answer).\n", threadNumber(), status == l_True ? "SAT" : status == l_False ? "UNSAT" : "UNKOWN");
 469         sharedcomp->jobStatus = status;
 470     }
 471
 472     if (firstToFinish && status == l_True) {
 473         extendModel();
 474
 475
 476         // Extend & copy model:
 477         model.growTo(nVars());
 478         for (int i = 0; i < nVars(); i++) model[i] = value(i);
 479     } else if (status == l_False && conflict.size() == 0)
 480         ok = false;
 481
 482
 483     pthread_cond_signal(pcfinished);
 484
 485     //cancelUntil(0);
 486
 487
 488     return status;
 489
 490 }