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
7 Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
8 CRIL - Univ. Artois, France
9 Labri - Univ. Bordeaux, France
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).
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:
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).
29 --------------- Original Minisat Copyrights
31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
32 Copyright (c) 2007-2010, Niklas Sorensson
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:
40 The above copyright notice and this permission notice shall be included in all copies or
41 substantial portions of the Software.
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 **************************************************************************************************/
51 #include "parallel/MultiSolvers.h"
53 #include "utils/System.h"
54 #include "simp/SimpSolver.h"
57 #include "parallel/SolverConfiguration.h"
59 using namespace Glucose;
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);
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);
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);
78 #include <sys/resource.h>
81 static inline double cpuTime(void) {
83 getrusage(RUSAGE_SELF, &ru);
84 return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
87 void MultiSolvers::informEnd(lbool res) {
89 pthread_cond_broadcast(&cfinished);
92 MultiSolvers::MultiSolvers(ParallelSolver *s):
94 , maxnbthreads(4), nbthreads(opt_nbsolversmultithreads), nbsolvers(opt_nbsolversmultithreads)
95 , nbcompanions(4), nbcompbysolver(2)
96 , allClonesAreBuilt(0)
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)
111 SharedCompanion *sc = new SharedCompanion();
112 this->sharedcomp = sc;
114 // Generate only solver 0.
115 // It loads the formula
116 // All others solvers are clone of this one
118 s->verbosity = 0; // No reportf in solvers... All is done in MultiSolver
119 s->setThreadNumber(0);
120 //s->belongsto = this;
123 assert(solvers[0]->threadNumber() == 0);
125 pthread_mutex_init(&m,NULL); //PTHREAD_MUTEX_INITIALIZER;
126 pthread_mutex_init(&mfinished,NULL); //PTHREAD_MUTEX_INITIALIZER;
127 pthread_cond_init(&cfinished,NULL);
130 fprintf(stdout,"c %d solvers engines and 1 companion as a blackboard created.\n", nbsolvers);
133 MultiSolvers::MultiSolvers() : MultiSolvers(new ParallelSolver(-1)) {
137 MultiSolvers::~MultiSolvers()
141 * Generate All solvers
144 void MultiSolvers::generateAllSolvers() {
145 assert(solvers[0] != NULL);
146 assert(allClonesAreBuilt==0);
148 for(int i=1;i<nbsolvers;i++) {
149 ParallelSolver *s = (ParallelSolver*)solvers[0]->clone();
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);
160 allClonesAreBuilt = 1;
164 * Choose solver for threads i (if no given in command line see above)
168 ParallelSolver* MultiSolvers::retrieveSolver(int i) {
169 return new ParallelSolver(i);
172 Var MultiSolvers::newVar(bool sign, bool dvar)
174 assert(solvers[0] != NULL);
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
182 for(int i=0;i<nbsolvers;i++) {
183 v = solvers[i]->newVar(sign,dvar);
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;
196 for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
197 if (solvers[0]->value(ps[i]) == l_True || ps[i] == ~p)
199 else if (solvers[0]->value(ps[i]) != l_False && ps[i] != p)
204 if (ps.size() == 0) {
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
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
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);
224 if(!allClonesAreBuilt) {
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);
238 bool MultiSolvers::simplify() {
239 assert(solvers[0] != NULL); // There is at least one solver.
241 if (!okay()) return false;
242 return ok = solvers[0]->simplify();
246 bool MultiSolvers::eliminate() {
248 // TODO allow variable elimination when all threads are built!
249 assert(allClonesAreBuilt==false);
251 SimpSolver * s = (SimpSolver*)getPrimarySolver();
252 return s->eliminate(true);
256 // TODO: Use a template here
257 void *localLaunch(void*arg) {
258 ParallelSolver* s = (ParallelSolver*)arg;
266 #define MAXIMUM_SLEEP_DURATION 5
267 void MultiSolvers::printStats() {
268 static int nbprinted = 1;
269 double cpu_time = cpuTime();
272 printf("c |-------------------------------------------------------------------------------------------------------|\n");
273 printf("c | id | starts | decisions | confls | Init T | learnts | exported | imported | promoted | %% | \n");
274 printf("c |-------------------------------------------------------------------------------------------------------|\n");
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);
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;
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);
296 // Still a ugly function... To be rewritten with some statistics class some day
297 void MultiSolvers::printFinalStats() {
298 sharedcomp->printStats();
301 printf("c |---------------------------------------- FINAL STATS --------------------------------------------------|\n");
304 printf("c |---------------");
305 for(int i = 0;i<solvers.size();i++)
306 printf("|------------");
307 printf("|-----------------|\n");
309 printf("c | Threads ");
310 for(int i = 0;i < solvers.size();i++) {
313 printf("| Total |\n");
315 printf("c |---------------");
316 for(int i = 0;i<solvers.size();i++)
317 printf("|------------");
318 printf("|-----------------|\n");
321 printf("c | Conflicts ");
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;
328 printf("| %15lld |\n",totalconf);
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;
336 printf("| %15" PRIu64" |\n", exported);
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;
344 printf("| %15" PRIu64" |\n", imported);
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;
352 printf("| %15" PRIu64" |\n", importedGood);
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;
360 printf("| %15" PRIu64" |\n", importedPurg);
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;
368 printf("| %15" PRIu64" |\n", promoted);
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;
376 printf("| %15" PRIu64" |\n", removedimported);
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;
384 printf("| %15" PRIu64" |\n",blockedreused);
387 printf("c | Orig seen ");
388 for(int i=0;i<solvers.size();i++) {
389 printf("| %10" PRIu64" ", solvers[i]->originalClausesSeen);
393 printf("c | Unaries ");
394 for(int i=0;i<solvers.size();i++) {
395 printf("| %10" PRIu64" ", solvers[i]->nbUn);
399 printf("c | Binaries ");
400 for(int i=0;i<solvers.size();i++) {
401 printf("| %10" PRIu64" ", solvers[i]->nbBin);
406 printf("c | Glues ");
407 for(int i=0;i<solvers.size();i++) {
408 printf("| %10" PRIu64" ", solvers[i]->nbDL2);
414 for(int i=0;i<solvers.size();i++) {
415 if(sharedcomp->winner()==solvers[i])
421 printf("c | Hamming ");
422 for(int i = 0;i<solvers.size();i++) {
428 for(int j = 0;j<nVars();j++) {
429 if(solvers[i]->valuePhase(j)!= solvers[winner]->valuePhase(j)) nb++;
431 printf("| %10d ",nb);
435 printf("| %15d |\n",sum/(solvers.size()>1?solvers.size()-1:1));
438 printf("c |---------------");
439 for(int i = 0;i<solvers.size();i++)
440 printf("|------------");
441 printf("|-----------------|\n");
447 // Well, all those parameteres are just naive guesses... No experimental evidences for this.
448 void MultiSolvers::adjustParameters() {
449 SolverConfiguration::configure(this,nbsolvers);
452 void MultiSolvers::adjustNumberOfCores() {
453 float mem = memUsed();
454 if (nbthreads==0) { // Automatic configuration
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;
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;
465 assert(nbthreads == nbsolvers);
469 lbool MultiSolvers::solve() {
470 pthread_attr_t thAttr;
473 adjustNumberOfCores();
474 sharedcomp->setNbThreads(nbsolvers);
476 printf("c | Generating clones |\n");
477 generateAllSolvers();
479 printf("c | all clones generated. Memory = %6.2fMb. |\n", memUsed());
480 printf("c ========================================================================================================|\n");
486 /* Initialize and set thread detached attribute */
487 pthread_attr_init(&thAttr);
488 pthread_attr_setdetachstate(&thAttr, PTHREAD_CREATE_JOINABLE);
492 // Launching all solvers
493 for (i = 0; i < nbsolvers; i++) {
494 pthread_t * pt = (pthread_t*)malloc(sizeof(pthread_t));
496 solvers[i]->pmfinished = &mfinished;
497 solvers[i]->pcfinished = &cfinished;
498 pthread_create(threads[i], &thAttr, &localLaunch, (void*)solvers[i]);
503 (void)pthread_mutex_lock(&m);
505 struct timespec timeout;
506 time(&timeout.tv_sec);
507 timeout.tv_sec += MAXIMUM_SLEEP_DURATION;
509 if (pthread_cond_timedwait(&cfinished, &mfinished, &timeout) != ETIMEDOUT)
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;
520 (void)pthread_mutex_unlock(&m);
522 for (i = 0; i < nbsolvers; i++) { // Wait for all threads to finish
523 pthread_join(*threads[i], NULL);
526 assert(sharedcomp != NULL);
527 result = sharedcomp->jobStatus;
528 if (result == l_True) {
529 int n = sharedcomp->jobFinishedBy->nVars();
531 for(int i = 0; i < n; i++)
532 model[i] = sharedcomp->jobFinishedBy->model[i];
538 for(int i=0;i<NBTHREADS;i++)
539 pthread_join(*threads[i],&status);