1 /***************************************************************************************[Solver.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 **************************************************************************************************/
52 #include "utils/System.h"
54 #include "core/Solver.h"
55 #include "core/Constants.h"
57 using namespace Glucose;
59 //=================================================================================================
62 static const char* _cat = "CORE";
63 static const char* _cr = "CORE -- RESTART";
64 static const char* _cred = "CORE -- REDUCE";
65 static const char* _cm = "CORE -- MINIMIZE";
70 static DoubleOption opt_K(_cr, "K", "The constant used to force restart", 0.8, DoubleRange(0, false, 1, false));
71 static DoubleOption opt_R(_cr, "R", "The constant used to block restart", 1.4, DoubleRange(1, false, 5, false));
72 static IntOption opt_size_lbd_queue(_cr, "szLBDQueue", "The size of moving average for LBD (restarts)", 50, IntRange(10, INT32_MAX));
73 static IntOption opt_size_trail_queue(_cr, "szTrailQueue", "The size of moving average for trail (block restarts)", 5000, IntRange(10, INT32_MAX));
75 static IntOption opt_first_reduce_db(_cred, "firstReduceDB", "The number of conflicts before the first reduce DB", 2000, IntRange(0, INT32_MAX));
76 static IntOption opt_inc_reduce_db(_cred, "incReduceDB", "Increment for reduce DB", 300, IntRange(0, INT32_MAX));
77 static IntOption opt_spec_inc_reduce_db(_cred, "specialIncReduceDB", "Special increment for reduce DB", 1000, IntRange(0, INT32_MAX));
78 static IntOption opt_lb_lbd_frozen_clause(_cred, "minLBDFrozenClause", "Protect clauses if their LBD decrease and is lower than (for one turn)", 30, IntRange(0, INT32_MAX));
80 static IntOption opt_lb_size_minimzing_clause(_cm, "minSizeMinimizingClause", "The min size required to minimize clause", 30, IntRange(3, INT32_MAX));
81 static IntOption opt_lb_lbd_minimzing_clause(_cm, "minLBDMinimizingClause", "The min LBD required to minimize clause", 6, IntRange(3, INT32_MAX));
84 static DoubleOption opt_var_decay(_cat, "var-decay", "The variable activity decay factor (starting point)", 0.8, DoubleRange(0, false, 1, false));
85 static DoubleOption opt_max_var_decay(_cat, "max-var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false));
86 static DoubleOption opt_clause_decay(_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false));
87 static DoubleOption opt_random_var_freq(_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
88 static DoubleOption opt_random_seed(_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false));
89 static IntOption opt_ccmin_mode(_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
90 static IntOption opt_phase_saving(_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
91 static BoolOption opt_rnd_init_act(_cat, "rnd-init", "Randomize the initial activity", false);
92 static DoubleOption opt_garbage_frac(_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
95 //=================================================================================================
96 // Constructor/Destructor:
100 // Parameters (user settable):
106 , sizeLBDQueue(opt_size_lbd_queue)
107 , sizeTrailQueue(opt_size_trail_queue)
108 , firstReduceDB(opt_first_reduce_db)
109 , incReduceDB(opt_inc_reduce_db)
110 , specialIncReduceDB(opt_spec_inc_reduce_db)
111 , lbLBDFrozenClause(opt_lb_lbd_frozen_clause)
112 , lbSizeMinimizingClause(opt_lb_size_minimzing_clause)
113 , lbLBDMinimizingClause(opt_lb_lbd_minimzing_clause)
114 , var_decay(opt_var_decay)
115 , max_var_decay(opt_max_var_decay)
116 , clause_decay(opt_clause_decay)
117 , random_var_freq(opt_random_var_freq)
118 , random_seed(opt_random_seed)
119 , ccmin_mode(opt_ccmin_mode)
120 , phase_saving(opt_phase_saving)
122 , rnd_init_act(opt_rnd_init_act)
123 , garbage_frac(opt_garbage_frac)
124 , certifiedOutput(NULL)
125 , certifiedUNSAT(false) // Not in the first parallel version
126 , panicModeLastRemoved(0), panicModeLastRemovedShared(0)
127 , useUnaryWatched(false)
128 , promoteOneWatchedClause(true)
129 // Statistics: (formerly in 'SolverStats')
132 , originalClausesSeen(0)
133 , sumDecisionLevels(0)
134 , nbRemovedClauses(0), nbRemovedUnaryWatchedClauses(0), nbReducedClauses(0), nbDL2(0), nbBin(0), nbUn(0), nbReduceDB(0)
135 , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), conflictsRestarts(0)
136 , nbstopsrestarts(0), nbstopsrestartssame(0), lastblockatrestart(0)
137 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
143 , watches(WatcherDeleted(ca))
144 , watchesBin(WatcherDeleted(ca))
145 , unaryWatches(WatcherDeleted(ca))
149 , order_heap(VarOrderLt(activity))
150 , progress_estimate(0)
151 , remove_satisfied(true)
152 , reduceOnSize(false) //
153 , reduceOnSizeSize(12) // Constant to use on size reductions
154 ,lastLearntClause(CRef_Undef)
155 // Resource constraints:
157 , conflict_budget(-1)
158 , propagation_budget(-1)
159 , asynch_interrupt(false)
161 , nbVarsInitialFormula(INT32_MAX)
163 , totalTime4Unsat(0.)
168 // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise
169 // Kept here for simplicity
170 lbdQueue.initSize(sizeLBDQueue);
171 trailQueue.initSize(sizeTrailQueue);
173 nbclausesbeforereduce = firstReduceDB;
176 //-------------------------------------------------------
177 // Special constructor used for cloning solvers
178 //-------------------------------------------------------
180 Solver::Solver(const Solver &s) :
181 verbosity(s.verbosity)
182 , showModel(s.showModel)
185 , sizeLBDQueue(s.sizeLBDQueue)
186 , sizeTrailQueue(s.sizeTrailQueue)
187 , firstReduceDB(s.firstReduceDB)
188 , incReduceDB(s.incReduceDB)
189 , specialIncReduceDB(s.specialIncReduceDB)
190 , lbLBDFrozenClause(s.lbLBDFrozenClause)
191 , lbSizeMinimizingClause(s.lbSizeMinimizingClause)
192 , lbLBDMinimizingClause(s.lbLBDMinimizingClause)
193 , var_decay(s.var_decay)
194 , max_var_decay(s.max_var_decay)
195 , clause_decay(s.clause_decay)
196 , random_var_freq(s.random_var_freq)
197 , random_seed(s.random_seed)
198 , ccmin_mode(s.ccmin_mode)
199 , phase_saving(s.phase_saving)
201 , rnd_init_act(s.rnd_init_act)
202 , garbage_frac(s.garbage_frac)
203 , certifiedOutput(NULL)
204 , certifiedUNSAT(false) // Not in the first parallel version
205 , panicModeLastRemoved(s.panicModeLastRemoved), panicModeLastRemovedShared(s.panicModeLastRemovedShared)
206 , useUnaryWatched(s.useUnaryWatched)
207 , promoteOneWatchedClause(s.promoteOneWatchedClause)
208 // Statistics: (formerly in 'SolverStats')
210 , nbPromoted(s.nbPromoted)
211 , originalClausesSeen(s.originalClausesSeen)
212 , sumDecisionLevels(s.sumDecisionLevels)
213 , nbRemovedClauses(s.nbRemovedClauses), nbRemovedUnaryWatchedClauses(s.nbRemovedUnaryWatchedClauses)
214 , nbReducedClauses(s.nbReducedClauses), nbDL2(s.nbDL2), nbBin(s.nbBin), nbUn(s.nbUn), nbReduceDB(s.nbReduceDB)
215 , solves(s.solves), starts(s.starts), decisions(s.decisions), rnd_decisions(s.rnd_decisions)
216 , propagations(s.propagations), conflicts(s.conflicts), conflictsRestarts(s.conflictsRestarts)
217 , nbstopsrestarts(s.nbstopsrestarts), nbstopsrestartssame(s.nbstopsrestartssame)
218 , lastblockatrestart(s.lastblockatrestart)
219 , dec_vars(s.dec_vars), clauses_literals(s.clauses_literals)
220 , learnts_literals(s.learnts_literals), max_literals(s.max_literals), tot_literals(s.tot_literals)
221 , curRestart(s.curRestart)
226 , watches(WatcherDeleted(ca))
227 , watchesBin(WatcherDeleted(ca))
228 , unaryWatches(WatcherDeleted(ca))
230 , simpDB_assigns(s.simpDB_assigns)
231 , simpDB_props(s.simpDB_props)
232 , order_heap(VarOrderLt(activity))
233 , progress_estimate(s.progress_estimate)
234 , remove_satisfied(s.remove_satisfied)
235 , reduceOnSize(s.reduceOnSize) //
236 , reduceOnSizeSize(s.reduceOnSizeSize) // Constant to use on size reductions
237 ,lastLearntClause(CRef_Undef)
238 // Resource constraints:
240 , conflict_budget(s.conflict_budget)
241 , propagation_budget(s.propagation_budget)
242 , asynch_interrupt(s.asynch_interrupt)
243 , incremental(s.incremental)
244 , nbVarsInitialFormula(s.nbVarsInitialFormula)
245 , totalTime4Sat(s.totalTime4Sat)
246 , totalTime4Unsat(s.totalTime4Unsat)
247 , nbSatCalls(s.nbSatCalls)
248 , nbUnsatCalls(s.nbUnsatCalls)
252 ca.extra_clause_field = s.ca.extra_clause_field;
254 // Initialize other variables
256 // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise
257 // Kept here for simplicity
259 nbclausesbeforereduce = s.nbclausesbeforereduce;
261 // Copy all search vectors
262 s.watches.copyTo(watches);
263 s.watchesBin.copyTo(watchesBin);
264 s.unaryWatches.copyTo(unaryWatches);
265 s.assigns.memCopyTo(assigns);
266 s.vardata.memCopyTo(vardata);
267 s.activity.memCopyTo(activity);
268 s.seen.memCopyTo(seen);
269 s.permDiff.memCopyTo(permDiff);
270 s.polarity.memCopyTo(polarity);
271 s.decision.memCopyTo(decision);
272 s.trail.memCopyTo(trail);
273 s.order_heap.copyTo(order_heap);
274 s.clauses.memCopyTo(clauses);
275 s.learnts.memCopyTo(learnts);
277 s.lbdQueue.copyTo(lbdQueue);
278 s.trailQueue.copyTo(trailQueue);
285 /****************************************************************
286 Set the incremental mode
287 ****************************************************************/
289 // This function set the incremental mode to true.
290 // You can add special code for this mode here.
292 void Solver::setIncrementalMode() {
296 // Number of variables without selectors
297 void Solver::initNbInitialVars(int nb) {
298 nbVarsInitialFormula = nb;
301 bool Solver::isIncremental() {
306 //=================================================================================================
310 // Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
311 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
314 Var Solver::newVar(bool sign, bool dvar) {
316 watches .init(mkLit(v, false));
317 watches .init(mkLit(v, true));
318 watchesBin .init(mkLit(v, false));
319 watchesBin .init(mkLit(v, true));
320 unaryWatches .init(mkLit(v, false));
321 unaryWatches .init(mkLit(v, true));
322 assigns .push(l_Undef);
323 vardata .push(mkVarData(CRef_Undef, 0));
324 activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
327 polarity .push(sign);
329 trail .capacity(v + 1);
330 setDecisionVar(v, dvar);
334 bool Solver::addClause_(vec<Lit>& ps) {
336 assert(decisionLevel() == 0);
337 if (!ok) return false;
339 // Check if clause is satisfied and remove false/duplicate literals:
347 if (certifiedUNSAT) {
348 for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
350 if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False)
355 for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
356 if (value(ps[i]) == l_True || ps[i] == ~p)
358 else if (value(ps[i]) != l_False && ps[i] != p)
362 if (flag && (certifiedUNSAT)) {
363 for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
364 fprintf(certifiedOutput, "%i ", (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1));
365 fprintf(certifiedOutput, "0\n");
367 fprintf(certifiedOutput, "d ");
368 for (i = j = 0, p = lit_Undef; i < oc.size(); i++)
369 fprintf(certifiedOutput, "%i ", (var(oc[i]) + 1) * (-2 * sign(oc[i]) + 1));
370 fprintf(certifiedOutput, "0\n");
376 else if (ps.size() == 1) {
377 uncheckedEnqueue(ps[0]);
378 return ok = (propagate() == CRef_Undef);
380 CRef cr = ca.alloc(ps, false);
388 void Solver::attachClause(CRef cr) {
389 const Clause& c = ca[cr];
391 assert(c.size() > 1);
393 watchesBin[~c[0]].push(Watcher(cr, c[1]));
394 watchesBin[~c[1]].push(Watcher(cr, c[0]));
396 watches[~c[0]].push(Watcher(cr, c[1]));
397 watches[~c[1]].push(Watcher(cr, c[0]));
399 if (c.learnt()) learnts_literals += c.size();
400 else clauses_literals += c.size();
403 void Solver::attachClausePurgatory(CRef cr) {
404 const Clause& c = ca[cr];
406 assert(c.size() > 1);
407 unaryWatches[~c[0]].push(Watcher(cr, c[1]));
411 void Solver::detachClause(CRef cr, bool strict) {
412 const Clause& c = ca[cr];
414 assert(c.size() > 1);
417 remove(watchesBin[~c[0]], Watcher(cr, c[1]));
418 remove(watchesBin[~c[1]], Watcher(cr, c[0]));
420 // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
421 watchesBin.smudge(~c[0]);
422 watchesBin.smudge(~c[1]);
426 remove(watches[~c[0]], Watcher(cr, c[1]));
427 remove(watches[~c[1]], Watcher(cr, c[0]));
429 // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
430 watches.smudge(~c[0]);
431 watches.smudge(~c[1]);
434 if (c.learnt()) learnts_literals -= c.size();
435 else clauses_literals -= c.size();
439 // The purgatory is the 1-Watched scheme for imported clauses
441 void Solver::detachClausePurgatory(CRef cr, bool strict) {
442 const Clause& c = ca[cr];
444 assert(c.size() > 1);
446 remove(unaryWatches[~c[0]], Watcher(cr, c[1]));
448 unaryWatches.smudge(~c[0]);
451 void Solver::removeClause(CRef cr, bool inPurgatory) {
455 if (certifiedUNSAT) {
456 fprintf(certifiedOutput, "d ");
457 for (int i = 0; i < c.size(); i++)
458 fprintf(certifiedOutput, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1));
459 fprintf(certifiedOutput, "0\n");
463 detachClausePurgatory(cr);
466 // Don't leave pointers to free'd memory!
467 if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
472 bool Solver::satisfied(const Clause& c) const {
474 return (value(c[0]) == l_True) || (value(c[1]) == l_True);
477 for (int i = 0; i < c.size(); i++)
478 if (value(c[i]) == l_True)
483 /************************************************************
484 * Compute LBD functions
485 *************************************************************/
487 inline unsigned int Solver::computeLBD(const vec<Lit> & lits,int end) {
491 if(incremental) { // ----------------- INCREMENTAL MODE
492 if(end==-1) end = lits.size();
494 for(int i=0;i<lits.size();i++) {
495 if(nbDone>=end) break;
496 if(isSelector(var(lits[i]))) continue;
498 int l = level(var(lits[i]));
499 if (permDiff[l] != MYFLAG) {
500 permDiff[l] = MYFLAG;
504 } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
505 for(int i=0;i<lits.size();i++) {
506 int l = level(var(lits[i]));
507 if (permDiff[l] != MYFLAG) {
508 permDiff[l] = MYFLAG;
516 if (lits.size() < reduceOnSizeSize) return lits.size(); // See the XMinisat paper
517 return lits.size() + nblevels;
520 inline unsigned int Solver::computeLBD(const Clause &c) {
524 if(incremental) { // ----------------- INCREMENTAL MODE
525 unsigned int nbDone = 0;
526 for(int i=0;i<c.size();i++) {
527 if(nbDone>=c.sizeWithoutSelectors()) break;
528 if(isSelector(var(c[i]))) continue;
530 int l = level(var(c[i]));
531 if (permDiff[l] != MYFLAG) {
532 permDiff[l] = MYFLAG;
536 } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
537 for(int i=0;i<c.size();i++) {
538 int l = level(var(c[i]));
539 if (permDiff[l] != MYFLAG) {
540 permDiff[l] = MYFLAG;
548 if (c.size() < reduceOnSizeSize) return c.size(); // See the XMinisat paper
549 return c.size() + nblevels;
553 /******************************************************************
554 * Minimisation with binary reolution
555 ******************************************************************/
556 void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
558 // Find the LBD measure
559 unsigned int lbd = computeLBD(out_learnt);
560 Lit p = ~out_learnt[0];
562 if (lbd <= lbLBDMinimizingClause) {
565 for (int i = 1; i < out_learnt.size(); i++) {
566 permDiff[var(out_learnt[i])] = MYFLAG;
569 vec<Watcher>& wbin = watchesBin[p];
571 for (int k = 0; k < wbin.size(); k++) {
572 Lit imp = wbin[k].blocker;
573 if (permDiff[var(imp)] == MYFLAG && value(imp) == l_True) {
575 permDiff[var(imp)] = MYFLAG - 1;
578 int l = out_learnt.size() - 1;
581 for (int i = 1; i < out_learnt.size() - nb; i++) {
582 if (permDiff[var(out_learnt[i])] != MYFLAG) {
583 Lit p = out_learnt[l];
584 out_learnt[l] = out_learnt[i];
591 out_learnt.shrink(nb);
597 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
600 void Solver::cancelUntil(int level) {
601 if (decisionLevel() > level) {
602 for (int c = trail.size() - 1; c >= trail_lim[level]; c--) {
603 Var x = var(trail[c]);
604 assigns [x] = l_Undef;
605 if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) {
606 polarity[x] = sign(trail[c]);
610 qhead = trail_lim[level];
611 trail.shrink(trail.size() - trail_lim[level]);
612 trail_lim.shrink(trail_lim.size() - level);
617 //=================================================================================================
620 Lit Solver::pickBranchLit() {
621 Var next = var_Undef;
624 if (drand(random_seed) < random_var_freq && !order_heap.empty()) {
625 next = order_heap[irand(random_seed, order_heap.size())];
626 if (value(next) == l_Undef && decision[next])
630 // Activity based decision:
631 while (next == var_Undef || value(next) != l_Undef || !decision[next])
632 if (order_heap.empty()) {
636 next = order_heap.removeMin();
639 return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
642 /*_________________________________________________________________________________________________
644 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
647 | Analyze conflict and produce a reason clause.
650 | * 'out_learnt' is assumed to be cleared.
651 | * Current decision level must be greater than root level.
654 | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
655 | * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
656 | rest of literals. There may be others from the same level though.
658 |________________________________________________________________________________________________@*/
659 void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors) {
664 // Generate conflict clause:
666 out_learnt.push(); // (leave room for the asserting literal)
667 int index = trail.size() - 1;
669 assert(confl != CRef_Undef); // (otherwise should be UIP)
670 Clause& c = ca[confl];
671 // Special case for binary clauses
672 // The first one has to be SAT
673 if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False) {
675 assert(value(c[1]) == l_True);
677 c[0] = c[1], c[1] = tmp;
681 parallelImportClauseDuringConflictAnalysis(c,confl);
683 } else { // original clause
685 originalClausesSeen++;
690 // DYNAMIC NBLEVEL trick (see competition'09 companion paper)
691 if (c.learnt() && c.lbd() > 2) {
692 unsigned int nblevels = computeLBD(c);
693 if (nblevels + 1 < c.lbd()) { // improve the LBD
694 if (c.lbd() <= lbLBDFrozenClause) {
695 c.setCanBeDel(false);
697 // seems to be interesting : keep it for the next round
698 c.setLBD(nblevels); // Update it
703 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) {
707 if (level(var(q)) == 0) {
708 } else { // Here, the old case
709 if(!isSelector(var(q)))
710 varBumpActivity(var(q));
712 if (level(var(q)) >= decisionLevel()) {
714 // UPDATEVARACTIVITY trick (see competition'09 companion paper)
715 if (!isSelector(var(q)) && (reason(var(q)) != CRef_Undef) && ca[reason(var(q))].learnt())
716 lastDecisionLevel.push(q);
718 if(isSelector(var(q))) {
719 assert(value(q) == l_False);
728 // Select next clause to look at:
729 while (!seen[var(trail[index--])]);
730 p = trail[index + 1];
731 confl = reason(var(p));
738 // Simplify conflict clause:
742 for (int i = 0; i < selectors.size(); i++)
743 out_learnt.push(selectors[i]);
745 out_learnt.copyTo(analyze_toclear);
746 if (ccmin_mode == 2) {
747 uint32_t abstract_level = 0;
748 for (i = 1; i < out_learnt.size(); i++)
749 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
751 for (i = j = 1; i < out_learnt.size(); i++)
752 if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
753 out_learnt[j++] = out_learnt[i];
755 } else if (ccmin_mode == 1) {
756 for (i = j = 1; i < out_learnt.size(); i++) {
757 Var x = var(out_learnt[i]);
759 if (reason(x) == CRef_Undef)
760 out_learnt[j++] = out_learnt[i];
762 Clause& c = ca[reason(var(out_learnt[i]))];
763 // Thanks to Siert Wieringa for this bug fix!
764 for (int k = ((c.size() == 2) ? 0 : 1); k < c.size(); k++)
765 if (!seen[var(c[k])] && level(var(c[k])) > 0) {
766 out_learnt[j++] = out_learnt[i];
772 i = j = out_learnt.size();
774 max_literals += out_learnt.size();
775 out_learnt.shrink(i - j);
776 tot_literals += out_learnt.size();
779 /* ***************************************
780 Minimisation with binary clauses of the asserting clause
781 First of all : we look for small clauses
782 Then, we reduce clauses with small LBD.
783 Otherwise, this can be useless
785 if (!incremental && out_learnt.size() <= lbSizeMinimizingClause) {
786 minimisationWithBinaryResolution(out_learnt);
788 // Find correct backtrack level:
790 if (out_learnt.size() == 1)
794 // Find the first literal assigned at the next-highest level:
795 for (int i = 2; i < out_learnt.size(); i++)
796 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
798 // Swap-in this literal at index 1:
799 Lit p = out_learnt[max_i];
800 out_learnt[max_i] = out_learnt[1];
802 out_btlevel = level(var(p));
805 szWithoutSelectors = 0;
806 for(int i=0;i<out_learnt.size();i++) {
807 if(!isSelector(var((out_learnt[i])))) szWithoutSelectors++;
811 szWithoutSelectors = out_learnt.size();
814 lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size());
816 // UPDATEVARACTIVITY trick (see competition'09 companion paper)
817 if (lastDecisionLevel.size() > 0) {
818 for (int i = 0; i < lastDecisionLevel.size(); i++) {
819 if (ca[reason(var(lastDecisionLevel[i]))].lbd() < lbd)
820 varBumpActivity(var(lastDecisionLevel[i]));
822 lastDecisionLevel.clear();
827 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
828 for (int j = 0; j < selectors.size(); j++) seen[var(selectors[j])] = 0;
832 // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
833 // visiting literals at levels that cannot be removed later.
835 bool Solver::litRedundant(Lit p, uint32_t abstract_levels) {
836 analyze_stack.clear();
837 analyze_stack.push(p);
838 int top = analyze_toclear.size();
839 while (analyze_stack.size() > 0) {
840 assert(reason(var(analyze_stack.last())) != CRef_Undef);
841 Clause& c = ca[reason(var(analyze_stack.last()))];
842 analyze_stack.pop(); //
843 if (c.size() == 2 && value(c[0]) == l_False) {
844 assert(value(c[1]) == l_True);
846 c[0] = c[1], c[1] = tmp;
849 for (int i = 1; i < c.size(); i++) {
852 if (level(var(p)) > 0) {
853 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0) {
855 analyze_stack.push(p);
856 analyze_toclear.push(p);
858 for (int j = top; j < analyze_toclear.size(); j++)
859 seen[var(analyze_toclear[j])] = 0;
860 analyze_toclear.shrink(analyze_toclear.size() - top);
872 /*_________________________________________________________________________________________________
874 | analyzeFinal : (p : Lit) -> [void]
877 | Specialized analysis procedure to express the final conflict in terms of assumptions.
878 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
879 | stores the result in 'out_conflict'.
880 |________________________________________________________________________________________________@*/
881 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) {
882 out_conflict.clear();
883 out_conflict.push(p);
885 if (decisionLevel() == 0)
890 for (int i = trail.size() - 1; i >= trail_lim[0]; i--) {
891 Var x = var(trail[i]);
893 if (reason(x) == CRef_Undef) {
894 assert(level(x) > 0);
895 out_conflict.push(~trail[i]);
897 Clause& c = ca[reason(x)];
898 // for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop
899 // Bug in case of assumptions due to special data structures for Binary.
900 // Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug.
901 for (int j = ((c.size() == 2) ? 0 : 1); j < c.size(); j++)
902 if (level(var(c[j])) > 0)
913 void Solver::uncheckedEnqueue(Lit p, CRef from) {
914 assert(value(p) == l_Undef);
915 assigns[var(p)] = lbool(!sign(p));
916 vardata[var(p)] = mkVarData(from, decisionLevel());
920 /*_________________________________________________________________________________________________
922 | propagate : [void] -> [Clause*]
925 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
926 | otherwise CRef_Undef.
929 | * the propagation queue is empty, even if there was a conflict.
930 |________________________________________________________________________________________________@*/
931 CRef Solver::propagate() {
932 CRef confl = CRef_Undef;
934 int previousqhead = qhead;
936 watchesBin.cleanAll();
937 unaryWatches.cleanAll();
938 while (qhead < trail.size()) {
939 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
940 vec<Watcher>& ws = watches[p];
941 Watcher *i, *j, *end;
945 // First, Propagate binary clauses
946 vec<Watcher>& wbin = watchesBin[p];
948 for (int k = 0; k < wbin.size(); k++) {
950 Lit imp = wbin[k].blocker;
952 if (value(imp) == l_False) {
956 if (value(imp) == l_Undef) {
957 uncheckedEnqueue(imp, wbin[k].cref);
961 // Now propagate other 2-watched clauses
962 for (i = j = (Watcher*) ws, end = i + ws.size(); i != end;) {
963 // Try to avoid inspecting the clause:
964 Lit blocker = i->blocker;
965 if (value(blocker) == l_True) {
970 // Make sure the false literal is data[1]:
973 assert(!c.getOneWatched());
975 if (c[0] == false_lit)
976 c[0] = c[1], c[1] = false_lit;
977 assert(c[1] == false_lit);
980 // If 0th watch is true, then clause is already satisfied.
982 Watcher w = Watcher(cr, first);
983 if (first != blocker && value(first) == l_True) {
988 if(incremental) { // ----------------- INCREMENTAL MODE
990 for (int k = 2; k < c.size(); k++) {
992 if (value(c[k]) != l_False){
993 if(decisionLevel()>assumptions.size()) {
999 if(value(c[k])==l_True || !isSelector(var(c[k]))) {
1006 if(choosenPos!=-1) {
1007 c[1] = c[choosenPos]; c[choosenPos] = false_lit;
1008 watches[~c[1]].push(w);
1010 } else { // ----------------- DEFAULT MODE (NOT INCREMENTAL)
1011 for (int k = 2; k < c.size(); k++) {
1013 if (value(c[k]) != l_False){
1014 c[1] = c[k]; c[k] = false_lit;
1015 watches[~c[1]].push(w);
1020 // Did not find watch -- clause is unit under assignment:
1022 if (value(first) == l_False) {
1024 qhead = trail.size();
1025 // Copy the remaining watches:
1029 uncheckedEnqueue(first, cr);
1038 // unaryWatches "propagation"
1039 if (useUnaryWatched && confl == CRef_Undef) {
1040 confl = propagateUnaryWatches(p);
1048 propagations += num_props;
1049 simpDB_props -= num_props;
1054 /*_________________________________________________________________________________________________
1056 | propagateUnaryWatches : [Lit] -> [Clause*]
1059 | Propagates unary watches of Lit p, return a conflict
1060 | otherwise CRef_Undef
1062 |________________________________________________________________________________________________@*/
1064 CRef Solver::propagateUnaryWatches(Lit p) {
1065 CRef confl= CRef_Undef;
1066 Watcher *i, *j, *end;
1067 vec<Watcher>& ws = unaryWatches[p];
1068 for (i = j = (Watcher*) ws, end = i + ws.size(); i != end;) {
1069 // Try to avoid inspecting the clause:
1070 Lit blocker = i->blocker;
1071 if (value(blocker) == l_True) {
1076 // Make sure the false literal is data[1]:
1079 assert(c.getOneWatched());
1081 assert(c[0] == false_lit); // this is unary watch... No other choice if "propagated"
1082 //if (c[0] == false_lit)
1083 //c[0] = c[1], c[1] = false_lit;
1084 //assert(c[1] == false_lit);
1086 Watcher w = Watcher(cr, c[0]);
1087 for (int k = 1; k < c.size(); k++) {
1088 if (value(c[k]) != l_False) {
1091 unaryWatches[~c[0]].push(w);
1092 goto NextClauseUnary;
1096 // Did not find watch -- clause is empty under assignment:
1100 qhead = trail.size();
1101 // Copy the remaining watches:
1105 // We can add it now to the set of clauses when backtracking
1107 if (promoteOneWatchedClause) {
1109 // Let's find the two biggest decision levels in the clause s.t. it will correctly be propagated when we'll backtrack
1112 for (int k = 1; k < c.size(); k++) {
1113 assert(value(c[k]) == l_False);
1114 assert(level(var(c[k])) <= level(var(c[0])));
1115 if (level(var(c[k])) > maxlevel) {
1117 maxlevel = level(var(c[k]));
1120 detachClausePurgatory(cr, true); // TODO: check that the cleanAll is ok (use ",true" otherwise)
1121 assert(index != -1);
1123 c[1] = c[index], c[index] = tmp;
1125 // TODO used in function ParallelSolver::reportProgressArrayImports
1127 //goodImportsFromThreads[ca[cr].importedFrom()]++;
1128 ca[cr].setOneWatched(false);
1129 ca[cr].setExported(2);
1139 /*_________________________________________________________________________________________________
1141 | reduceDB : () -> [void]
1144 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
1145 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
1146 |________________________________________________________________________________________________@*/
1149 void Solver::reduceDB()
1154 sort(learnts, reduceDB_lt(ca));
1156 // We have a lot of "good" clauses, it is difficult to compare them. Keep more !
1157 if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncReduceDB;
1159 if(ca[learnts.last()].lbd()<=5) nbclausesbeforereduce +=specialIncReduceDB;
1162 // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
1163 // Keep clauses which seem to be usefull (their lbd was reduce during this sequence)
1165 int limit = learnts.size() / 2;
1167 for (i = j = 0; i < learnts.size(); i++){
1168 Clause& c = ca[learnts[i]];
1169 if (c.lbd()>2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) {
1170 removeClause(learnts[i]);
1174 if(!c.canBeDel()) limit++; //we keep c, so we can delete an other clause
1175 c.setCanBeDel(true); // At the next step, c can be delete
1176 learnts[j++] = learnts[i];
1179 learnts.shrink(i - j);
1184 void Solver::removeSatisfied(vec<CRef>& cs) {
1187 for (i = j = 0; i < cs.size(); i++) {
1188 Clause& c = ca[cs[i]];
1192 if (c.getOneWatched())
1193 removeClause(cs[i], true);
1195 removeClause(cs[i]);
1202 void Solver::rebuildOrderHeap() {
1204 for (Var v = 0; v < nVars(); v++)
1205 if (decision[v] && value(v) == l_Undef)
1207 order_heap.build(vs);
1211 /*_________________________________________________________________________________________________
1213 | simplify : [void] -> [bool]
1216 | Simplify the clause database according to the current top-level assigment. Currently, the only
1217 | thing done here is the removal of satisfied clauses, but more things can be put here.
1218 |________________________________________________________________________________________________@*/
1219 bool Solver::simplify() {
1220 assert(decisionLevel() == 0);
1222 if (!ok) return ok = false;
1224 CRef cr = propagate();
1225 if (cr != CRef_Undef) {
1231 if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
1234 // Remove satisfied clauses:
1235 removeSatisfied(learnts);
1236 removeSatisfied(unaryWatchedClauses);
1237 if (remove_satisfied) // Can be turned off.
1238 removeSatisfied(clauses);
1242 simpDB_assigns = nAssigns();
1243 simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
1249 /*_________________________________________________________________________________________________
1251 | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
1254 | Search for a model the specified number of conflicts.
1255 | NOTE! Use negative value for 'nof_conflicts' indicate infinity.
1258 | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
1259 | all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
1260 | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
1261 |________________________________________________________________________________________________@*/
1262 lbool Solver::search(int nof_conflicts) {
1264 int backtrack_level;
1266 vec<Lit> learnt_clause, selectors;
1267 unsigned int nblevels,szWithoutSelectors = 0;
1268 bool blocked = false;
1271 if (decisionLevel() == 0) { // We import clauses FIXME: ensure that we will import clauses enventually (restart after some point)
1272 parallelImportUnaryClauses();
1274 if (parallelImportClauses())
1278 CRef confl = propagate();
1280 if (confl != CRef_Undef) {
1281 if(parallelJobIsFinished())
1285 sumDecisionLevels += decisionLevel();
1289 conflictsRestarts++;
1290 if (conflicts % 5000 == 0 && var_decay < max_var_decay)
1293 if (verbosity >= 1 && conflicts % verbEveryConflicts == 0) {
1294 printf("c | %8d %7d %5d | %7d %8d %8d | %5d %8d %6d %8d | %6.3f %% |\n",
1295 (int) starts, (int) nbstopsrestarts, (int) (conflicts / starts),
1296 (int) dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int) clauses_literals,
1297 (int) nbReduceDB, nLearnts(), (int) nbDL2, (int) nbRemovedClauses, progressEstimate()*100);
1299 if (decisionLevel() == 0) {
1304 trailQueue.push(trail.size());
1305 // BLOCK RESTART (CP 2012 paper)
1306 if (conflictsRestarts > LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid() && trail.size() > R * trailQueue.getavg()) {
1307 lbdQueue.fastclear();
1310 lastblockatrestart = starts;
1311 nbstopsrestartssame++;
1316 learnt_clause.clear();
1319 analyze(confl, learnt_clause, selectors, backtrack_level, nblevels,szWithoutSelectors);
1321 lbdQueue.push(nblevels);
1324 cancelUntil(backtrack_level);
1326 if (certifiedUNSAT) {
1327 for (int i = 0; i < learnt_clause.size(); i++)
1328 fprintf(certifiedOutput, "%i ", (var(learnt_clause[i]) + 1) *
1329 (-2 * sign(learnt_clause[i]) + 1));
1330 fprintf(certifiedOutput, "0\n");
1334 if (learnt_clause.size() == 1) {
1335 uncheckedEnqueue(learnt_clause[0]);
1337 parallelExportUnaryClause(learnt_clause[0]);
1339 CRef cr = ca.alloc(learnt_clause, true);
1340 ca[cr].setLBD(nblevels);
1341 ca[cr].setOneWatched(false);
1342 ca[cr].setSizeWithoutSelectors(szWithoutSelectors);
1343 if (nblevels <= 2) nbDL2++; // stats
1344 if (ca[cr].size() == 2) nbBin++; // stats
1347 lastLearntClause = cr; // Use in multithread (to hard to put inside ParallelSolver)
1348 parallelExportClauseDuringSearch(ca[cr]);
1349 claBumpActivity(ca[cr]);
1350 uncheckedEnqueue(learnt_clause[0], cr);
1358 // Our dynamic restart, see the SAT09 competition compagnion paper
1360 (lbdQueue.isvalid() && ((lbdQueue.getavg() * K) > (sumLBD / conflictsRestarts)))) {
1361 lbdQueue.fastclear();
1362 progress_estimate = progressEstimate();
1364 if(incremental) // DO NOT BACKTRACK UNTIL 0.. USELESS
1365 bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
1371 // Simplify the set of problem clauses:
1372 if (decisionLevel() == 0 && !simplify()) {
1375 // Perform clause database reduction !
1376 if (conflicts >= ((unsigned int) curRestart * nbclausesbeforereduce)) {
1378 if (learnts.size() > 0) {
1379 curRestart = (conflicts / nbclausesbeforereduce) + 1;
1381 if (!panicModeIsEnabled())
1382 nbclausesbeforereduce += incReduceDB;
1386 lastLearntClause = CRef_Undef;
1387 Lit next = lit_Undef;
1388 while (decisionLevel() < assumptions.size()) {
1389 // Perform user provided assumption:
1390 Lit p = assumptions[decisionLevel()];
1391 if (value(p) == l_True) {
1392 // Dummy decision level:
1394 } else if (value(p) == l_False) {
1395 analyzeFinal(~p, conflict);
1403 if (next == lit_Undef) {
1404 // New variable decision:
1406 next = pickBranchLit();
1407 if (next == lit_Undef) {
1408 printf("c last restart ## conflicts : %d %d \n", conflictC, decisionLevel());
1414 // Increase decision level and enqueue 'next'
1416 uncheckedEnqueue(next);
1421 double Solver::progressEstimate() const {
1422 double progress = 0;
1423 double F = 1.0 / nVars();
1425 for (int i = 0; i <= decisionLevel(); i++) {
1426 int beg = i == 0 ? 0 : trail_lim[i - 1];
1427 int end = i == decisionLevel() ? trail.size() : trail_lim[i];
1428 progress += pow(F, i) * (end - beg);
1431 return progress / nVars();
1434 void Solver::printIncrementalStats() {
1436 printf("c---------- Glucose Stats -------------------------\n");
1437 printf("c restarts : %" PRIu64"\n", starts);
1438 printf("c nb ReduceDB : %" PRIu64"\n", nbReduceDB);
1439 printf("c nb removed Clauses : %" PRIu64"\n", nbRemovedClauses);
1440 printf("c nb learnts DL2 : %" PRIu64"\n", nbDL2);
1441 printf("c nb learnts size 2 : %" PRIu64"\n", nbBin);
1442 printf("c nb learnts size 1 : %" PRIu64"\n", nbUn);
1444 printf("c conflicts : %" PRIu64"\n", conflicts);
1445 printf("c decisions : %" PRIu64"\n", decisions);
1446 printf("c propagations : %" PRIu64"\n", propagations);
1448 printf("\nc SAT Calls : %d in %g seconds\n",nbSatCalls,totalTime4Sat);
1449 printf("c UNSAT Calls : %d in %g seconds\n",nbUnsatCalls,totalTime4Unsat);
1451 printf("c--------------------------------------------------\n");
1454 // NOTE: assumptions passed in member-variable 'assumptions'.
1456 lbool Solver::solve_(bool do_simp, bool turn_off_simp) // Parameters are useless in core but useful for SimpSolver....
1459 if(incremental && certifiedUNSAT) {
1460 printf("Can not use incremental and certified unsat in the same time\n");
1466 if (!ok) return l_False;
1467 double curTime = cpuTime();
1473 lbool status = l_Undef;
1474 if(!incremental && verbosity>=1) {
1475 printf("c ========================================[ MAGIC CONSTANTS ]==============================================\n");
1476 printf("c | Constants are supposed to work well together :-) |\n");
1477 printf("c | however, if you find better choices, please let us known... |\n");
1478 printf("c |-------------------------------------------------------------------------------------------------------|\n");
1479 printf("c | | | |\n");
1480 printf("c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |\n");
1481 printf("c | * LBD Queue : %6d | * First : %6d | * size < %3d |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMinimizingClause);
1482 printf("c | * Trail Queue : %6d | * Inc : %6d | * lbd < %3d |\n",trailQueue.maxSize(),incReduceDB,lbLBDMinimizingClause);
1483 printf("c | * K : %6.2f | * Special : %6d | |\n",K,specialIncReduceDB);
1484 printf("c | * R : %6.2f | * Protected : (lbd)< %2d | |\n",R,lbLBDFrozenClause);
1485 printf("c | | | |\n");
1486 printf("c ==================================[ Search Statistics (every %6d conflicts) ]=========================\n",verbEveryConflicts);
1489 printf("c | RESTARTS | ORIGINAL | LEARNT | Progress |\n");
1490 printf("c | NB Blocked Avg Cfc | Vars Clauses Literals | Red Learnts LBD2 Removed | |\n");
1491 printf("c =========================================================================================================\n");
1495 int curr_restarts = 0;
1496 while (status == l_Undef){
1497 status = search(0); // the parameter is useless in glucose, kept to allow modifications
1499 if (!withinBudget()) break;
1503 if (!incremental && verbosity >= 1)
1504 printf("c =========================================================================================================\n");
1506 if (certifiedUNSAT){ // Want certified output
1507 if (status == l_False)
1508 fprintf(certifiedOutput, "0\n");
1509 fclose(certifiedOutput);
1513 if (status == l_True){
1514 // Extend & copy model:
1515 model.growTo(nVars());
1516 for (int i = 0; i < nVars(); i++) model[i] = value(i);
1517 }else if (status == l_False && conflict.size() == 0)
1525 double finalTime = cpuTime();
1526 if(status==l_True) {
1528 totalTime4Sat +=(finalTime-curTime);
1530 if(status==l_False) {
1532 totalTime4Unsat +=(finalTime-curTime);
1544 //=================================================================================================
1545 // Writing CNF to DIMACS:
1547 // FIXME: this needs to be rewritten completely.
1549 static Var mapVar(Var x, vec<Var>& map, Var& max) {
1550 if (map.size() <= x || map[x] == -1) {
1551 map.growTo(x + 1, -1);
1557 void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max) {
1558 if (satisfied(c)) return;
1560 for (int i = 0; i < c.size(); i++)
1561 if (value(c[i]) != l_False)
1562 fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max) + 1);
1566 void Solver::toDimacs(const char *file, const vec<Lit>& assumps) {
1567 FILE* f = fopen(file, "wr");
1569 fprintf(stderr, "could not open file %s\n", file), exit(1);
1570 toDimacs(f, assumps);
1574 void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) {
1575 // Handle case when solver is in contradictory state:
1577 fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
1584 // Cannot use removeClauses here because it is not safe
1585 // to deallocate them at this point. Could be improved.
1587 for (int i = 0; i < clauses.size(); i++)
1588 if (!satisfied(ca[clauses[i]]))
1591 for (int i = 0; i < clauses.size(); i++)
1592 if (!satisfied(ca[clauses[i]])) {
1593 Clause& c = ca[clauses[i]];
1594 for (int j = 0; j < c.size(); j++)
1595 if (value(c[j]) != l_False)
1596 mapVar(var(c[j]), map, max);
1599 // Assumptions are added as unit clauses:
1600 cnt += assumptions.size();
1602 fprintf(f, "p cnf %d %d\n", max, cnt);
1604 for (int i = 0; i < assumptions.size(); i++) {
1605 assert(value(assumptions[i]) != l_False);
1606 fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max) + 1);
1609 for (int i = 0; i < clauses.size(); i++)
1610 toDimacs(f, ca[clauses[i]], map, max);
1613 printf("Wrote %d clauses with %d variables.\n", cnt, max);
1617 //=================================================================================================
1618 // Garbage Collection methods:
1620 void Solver::relocAll(ClauseAllocator& to) {
1623 // for (int i = 0; i < watches.size(); i++)
1625 watchesBin.cleanAll();
1626 unaryWatches.cleanAll();
1627 for (int v = 0; v < nVars(); v++)
1628 for (int s = 0; s < 2; s++) {
1629 Lit p = mkLit(v, s);
1630 // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
1631 vec<Watcher>& ws = watches[p];
1632 for (int j = 0; j < ws.size(); j++)
1633 ca.reloc(ws[j].cref, to);
1634 vec<Watcher>& ws2 = watchesBin[p];
1635 for (int j = 0; j < ws2.size(); j++)
1636 ca.reloc(ws2[j].cref, to);
1637 vec<Watcher>& ws3 = unaryWatches[p];
1638 for (int j = 0; j < ws3.size(); j++)
1639 ca.reloc(ws3[j].cref, to);
1644 for (int i = 0; i < trail.size(); i++) {
1645 Var v = var(trail[i]);
1647 if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
1648 ca.reloc(vardata[v].reason, to);
1653 for (int i = 0; i < learnts.size(); i++)
1654 ca.reloc(learnts[i], to);
1658 for (int i = 0; i < clauses.size(); i++)
1659 ca.reloc(clauses[i], to);
1661 for (int i = 0; i < unaryWatchedClauses.size(); i++)
1662 ca.reloc(unaryWatchedClauses[i], to);
1667 void Solver::garbageCollect() {
1668 // Initialize the next region to a size corresponding to the estimated utilization degree. This
1669 // is not precise but should avoid some unnecessary reallocations for the new region:
1670 ClauseAllocator to(ca.size() - ca.wasted());
1674 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
1675 ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size);
1679 //--------------------------------------------------------------
1680 // Functions related to MultiThread.
1681 // Useless in case of single core solver (aka original glucose)
1682 // Keep them empty if you just use core solver
1683 //--------------------------------------------------------------
1685 bool Solver::panicModeIsEnabled() {
1689 void Solver::parallelImportUnaryClauses() {
1692 bool Solver::parallelImportClauses() {
1697 void Solver::parallelExportUnaryClause(Lit p) {
1699 void Solver::parallelExportClauseDuringSearch(Clause &c) {
1702 bool Solver::parallelJobIsFinished() {
1703 // Parallel: another job has finished let's quit
1707 void Solver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) {