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
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 **************************************************************************************************/
50 #include "parallel/ParallelSolver.h"
53 using namespace Glucose;
55 const char* _cunstable = "CORE/PARALLEL -- UNSTABLE FEATURES";
56 const char* _parallel = "PARALLEL";
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);
62 ParallelSolver::ParallelSolver(int threadId) :
64 , thn(threadId) // The thread number of this solver
67 , nbexportedunit(0), nbimportedunit(0), nbimportedInPurgatory(0), nbImportedGoodClauses(0)
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)
80 useUnaryWatched = true; // We want to use promoted clauses here !
86 ParallelSolver::~ParallelSolver() {
87 printf("c Solver of thread %d ended.\n", thn);
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)
108 s.goodImportsFromThreads.memCopyTo(goodImportsFromThreads);
109 useUnaryWatched = s.useUnaryWatched;
113 // Strategy to reduce unary watches list
114 struct reduceDB_oneWatched_lt {
117 reduceDB_oneWatched_lt(ClauseAllocator& ca_) : ca(ca_) {
120 bool operator()(CRef x, CRef y) {
122 // Main criteria... Like in MiniSat we keep all binary clauses
123 if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
125 if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
126 if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
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;
132 if (ca[x].lbd() > ca[y].lbd()) return 1;
133 if (ca[x].lbd() < ca[y].lbd()) return 0;
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();
139 //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
144 void ParallelSolver::reduceDB() {
148 sort(learnts, reduceDB_lt(ca));
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;
156 if (ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB;
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)
161 limit = learnts.size() / 2;
163 limit = panicModeLastRemoved;
165 panicModeLastRemoved = 0;
167 uint64_t sumsize = 0;
168 for (i = j = 0; i < learnts.size(); i++) {
170 Clause& c = ca[learnts[i]];
171 if (i == learnts.size() / 2)
172 goodlimitlbd = c.lbd();
174 if (c.lbd() > 2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) {
175 removeClause(learnts[i]);
177 panicModeLastRemoved++;
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];
184 learnts.shrink(i - j);
186 if (learnts.size() > 0)
187 goodlimitsize = 1 + (double) sumsize / (double) learnts.size();
189 // Special treatment for imported clauses
190 if (!panicModeIsEnabled())
191 limit = unaryWatchedClauses.size() - (learnts.size() * 2);
193 limit = panicModeLastRemovedShared;
194 panicModeLastRemovedShared = 0;
195 if ((unaryWatchedClauses.size() > 100) && (limit > 0)) {
197 sort(unaryWatchedClauses, reduceDB_oneWatched_lt(ca));
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++;
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];
211 unaryWatchedClauses.shrink(i - j);
218 /*_________________________________________________________________________________________________
220 | parallelImportClauseDuringConflictAnalysis : (Clause &c,CRef confl) -> [void]
223 | Verify if the clause using during conflict analysis is good for export
226 |________________________________________________________________________________________________@*/
229 void ParallelSolver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) {
230 if (dontExportDirectReusedClauses && (confl == lastLearntClause) && (c.getExported() < 2)) { // Experimental stuff
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)) {
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);
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);
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]);
262 printf(" | %8d\n", totalImports);
268 /*_________________________________________________________________________________________________
270 | shareClause : (Clause &c) -> [bool]
273 | share a clause to other cores
275 | Output: true if the clause is indeed sent
276 |________________________________________________________________________________________________@*/
278 bool ParallelSolver::shareClause(Clause & c) {
279 bool sent = sharedcomp->addLearnt(this, c);
285 /*_________________________________________________________________________________________________
287 | panicModeIsEnabled : () -> [bool]
290 | is panic mode (save memory) is enabled ?
291 |________________________________________________________________________________________________@*/
293 bool ParallelSolver::panicModeIsEnabled() {
294 return sharedcomp->panicMode;
297 /*_________________________________________________________________________________________________
299 | parallelImportUnaryClauses : () -> [void]
302 | import all unary clauses from other cores
303 |________________________________________________________________________________________________@*/
305 void ParallelSolver::parallelImportUnaryClauses() {
307 while ((l = sharedcomp->getUnary(this)) != lit_Undef) {
308 if (value(var(l)) == l_Undef) {
315 /*_________________________________________________________________________________________________
317 | parallelImportClauses : () -> [bool]
320 | import all clauses from other cores
321 | Output : if there is a final conflict
322 |________________________________________________________________________________________________@*/
324 bool ParallelSolver::parallelImportClauses() {
326 assert(decisionLevel() == 0);
327 int importedFromThread;
328 while (sharedcomp->getNewClause(this, importedFromThread, importedClause)) {
329 assert(importedFromThread <= sharedcomp->nbThreads);
330 assert(importedFromThread >= 0);
332 assert(importedFromThread != thn);
334 if (importedClause.size() == 0)
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
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.
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!)
350 nbImportedGoodClauses++;
352 ca[cr].setOneWatched(true);
353 attachClausePurgatory(cr); //
354 nbimportedInPurgatory++;
356 assert(ca[cr].learnt());
363 /*_________________________________________________________________________________________________
365 | parallelExportUnaryClause : (Lit p) -> [void]
368 | export unary clauses to other cores
369 |________________________________________________________________________________________________@*/
371 void ParallelSolver::parallelExportUnaryClause(Lit p) {
373 sharedcomp->addLearnt(this,p ); // TODO: there can be a contradiction here (two theads proving a and -a)
378 /*_________________________________________________________________________________________________
380 | parallelExportClauseDuringSearch : (Clause &c) -> [void]
383 | Verify if a new learnt clause is useful for export
386 |________________________________________________________________________________________________@*/
388 void ParallelSolver::parallelExportClauseDuringSearch(Clause &c) {
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)
401 /*_________________________________________________________________________________________________
403 | parallelJobIsFinished : () -> [bool]
406 | Is a core already finish the search
408 |________________________________________________________________________________________________@*/
410 bool ParallelSolver::parallelJobIsFinished() {
411 // Parallel: another job has finished let's quit
412 return (sharedcomp->jobFinished());
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;
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]);
425 // If an assumption has been eliminated, remember it.
426 assert(!isEliminated(v));
431 extra_frozen.push(v);
434 result = lbool(eliminate(turn_off_simp));
439 if (!ok) return l_False;
444 lbool status = l_Undef;
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;
455 printf("c =========================================================================================================\n");
459 // Unfreeze the assumptions that were frozen:
460 for (int i = 0; i < extra_frozen.size(); i++)
461 setFrozen(extra_frozen[i], false);
464 bool firstToFinish = false;
465 if (status != l_Undef)
466 firstToFinish = sharedcomp->IFinished(this);
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;
472 if (firstToFinish && status == l_True) {
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)
483 pthread_cond_signal(pcfinished);