glucose-syrup/core/Solver.cc

   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
   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 <math.h>
  51
  52 #include "utils/System.h"
  53 #include "mtl/Sort.h"
  54 #include "core/Solver.h"
  55 #include "core/Constants.h"
  56
  57 using namespace Glucose;
  58
  59 //=================================================================================================
  60 // Options:
  61
  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";
  66
  67
  68
  69
  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));
  74
  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));
  79
  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));
  82
  83
  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));
  93
  94
  95 //=================================================================================================
  96 // Constructor/Destructor:
  97
  98 Solver::Solver() :
  99
 100 // Parameters (user settable):
 101 //
 102 verbosity(0)
 103 , showModel(0)
 104 , K(opt_K)
 105 , R(opt_R)
 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)
 121 , rnd_pol(false)
 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')
 130 //
 131 , nbPromoted(0)
 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)
 138 , curRestart(1)
 139
 140 , ok(true)
 141 , cla_inc(1)
 142 , var_inc(1)
 143 , watches(WatcherDeleted(ca))
 144 , watchesBin(WatcherDeleted(ca))
 145 , unaryWatches(WatcherDeleted(ca))
 146 , qhead(0)
 147 , simpDB_assigns(-1)
 148 , simpDB_props(0)
 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:
 156 //
 157 , conflict_budget(-1)
 158 , propagation_budget(-1)
 159 , asynch_interrupt(false)
 160 , incremental(false)
 161 , nbVarsInitialFormula(INT32_MAX)
 162 , totalTime4Sat(0.)
 163 , totalTime4Unsat(0.)
 164 , nbSatCalls(0)
 165 , nbUnsatCalls(0)
 166 {
 167     MYFLAG = 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);
 172     sumLBD = 0;
 173     nbclausesbeforereduce = firstReduceDB;
 174 }
 175
 176 //-------------------------------------------------------
 177 // Special constructor used for cloning solvers
 178 //-------------------------------------------------------
 179
 180 Solver::Solver(const Solver &s) :
 181   verbosity(s.verbosity)
 182 , showModel(s.showModel)
 183 , K(s.K)
 184 , R(s.R)
 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)
 200 , rnd_pol(s.rnd_pol)
 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')
 209 //
 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)
 222
 223 , ok(true)
 224 , cla_inc(s.cla_inc)
 225 , var_inc(s.var_inc)
 226 , watches(WatcherDeleted(ca))
 227 , watchesBin(WatcherDeleted(ca))
 228 , unaryWatches(WatcherDeleted(ca))
 229 , qhead(s.qhead)
 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:
 239 //
 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)
 249 {
 250     // Copy clauses.
 251     s.ca.copyTo(ca);
 252     ca.extra_clause_field = s.ca.extra_clause_field;
 253
 254     // Initialize  other variables
 255      MYFLAG = 0;
 256     // Initialize only first time. Useful for incremental solving (not in // version), useless otherwise
 257     // Kept here for simplicity
 258     sumLBD = s.sumLBD;
 259     nbclausesbeforereduce = s.nbclausesbeforereduce;
 260
 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);
 276
 277     s.lbdQueue.copyTo(lbdQueue);
 278     s.trailQueue.copyTo(trailQueue);
 279
 280 }
 281
 282 Solver::~Solver() {
 283 }
 284
 285 /****************************************************************
 286  Set the incremental mode
 287 ****************************************************************/
 288
 289 // This function set the incremental mode to true.
 290 // You can add special code for this mode here.
 291
 292 void Solver::setIncrementalMode() {
 293   incremental = true;
 294 }
 295
 296 // Number of variables without selectors
 297 void Solver::initNbInitialVars(int nb) {
 298   nbVarsInitialFormula = nb;
 299 }
 300
 301 bool Solver::isIncremental() {
 302   return incremental;
 303 }
 304
 305
 306 //=================================================================================================
 307 // Minor methods:
 308
 309
 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).
 312 //
 313
 314 Var Solver::newVar(bool sign, bool dvar) {
 315     int v = nVars();
 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);
 325     seen .push(0);
 326     permDiff .push(0);
 327     polarity .push(sign);
 328     decision .push();
 329     trail .capacity(v + 1);
 330     setDecisionVar(v, dvar);
 331     return v;
 332 }
 333
 334 bool Solver::addClause_(vec<Lit>& ps) {
 335
 336     assert(decisionLevel() == 0);
 337     if (!ok) return false;
 338
 339     // Check if clause is satisfied and remove false/duplicate literals:
 340     sort(ps);
 341
 342     vec<Lit> oc;
 343     oc.clear();
 344
 345     Lit p;
 346     int i, j, flag = 0;
 347     if (certifiedUNSAT) {
 348         for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
 349             oc.push(ps[i]);
 350             if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False)
 351                 flag = 1;
 352         }
 353     }
 354
 355     for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
 356         if (value(ps[i]) == l_True || ps[i] == ~p)
 357             return true;
 358         else if (value(ps[i]) != l_False && ps[i] != p)
 359             ps[j++] = p = ps[i];
 360     ps.shrink(i - j);
 361
 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");
 366
 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");
 371     }
 372
 373
 374     if (ps.size() == 0)
 375         return ok = false;
 376     else if (ps.size() == 1) {
 377         uncheckedEnqueue(ps[0]);
 378         return ok = (propagate() == CRef_Undef);
 379     } else {
 380         CRef cr = ca.alloc(ps, false);
 381         clauses.push(cr);
 382         attachClause(cr);
 383     }
 384
 385     return true;
 386 }
 387
 388 void Solver::attachClause(CRef cr) {
 389     const Clause& c = ca[cr];
 390
 391     assert(c.size() > 1);
 392     if (c.size() == 2) {
 393         watchesBin[~c[0]].push(Watcher(cr, c[1]));
 394         watchesBin[~c[1]].push(Watcher(cr, c[0]));
 395     } else {
 396         watches[~c[0]].push(Watcher(cr, c[1]));
 397         watches[~c[1]].push(Watcher(cr, c[0]));
 398     }
 399     if (c.learnt()) learnts_literals += c.size();
 400     else clauses_literals += c.size();
 401 }
 402
 403 void Solver::attachClausePurgatory(CRef cr) {
 404     const Clause& c = ca[cr];
 405
 406     assert(c.size() > 1);
 407     unaryWatches[~c[0]].push(Watcher(cr, c[1]));
 408
 409 }
 410
 411 void Solver::detachClause(CRef cr, bool strict) {
 412     const Clause& c = ca[cr];
 413
 414     assert(c.size() > 1);
 415     if (c.size() == 2) {
 416         if (strict) {
 417             remove(watchesBin[~c[0]], Watcher(cr, c[1]));
 418             remove(watchesBin[~c[1]], Watcher(cr, c[0]));
 419         } else {
 420             // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
 421             watchesBin.smudge(~c[0]);
 422             watchesBin.smudge(~c[1]);
 423         }
 424     } else {
 425         if (strict) {
 426             remove(watches[~c[0]], Watcher(cr, c[1]));
 427             remove(watches[~c[1]], Watcher(cr, c[0]));
 428         } else {
 429             // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
 430             watches.smudge(~c[0]);
 431             watches.smudge(~c[1]);
 432         }
 433     }
 434     if (c.learnt()) learnts_literals -= c.size();
 435     else clauses_literals -= c.size();
 436 }
 437
 438
 439 // The purgatory is the 1-Watched scheme for imported clauses
 440
 441 void Solver::detachClausePurgatory(CRef cr, bool strict) {
 442     const Clause& c = ca[cr];
 443
 444     assert(c.size() > 1);
 445     if (strict)
 446         remove(unaryWatches[~c[0]], Watcher(cr, c[1]));
 447     else
 448         unaryWatches.smudge(~c[0]);
 449 }
 450
 451 void Solver::removeClause(CRef cr, bool inPurgatory) {
 452
 453     Clause& c = ca[cr];
 454
 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");
 460     }
 461
 462     if (inPurgatory)
 463         detachClausePurgatory(cr);
 464     else
 465         detachClause(cr);
 466     // Don't leave pointers to free'd memory!
 467     if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
 468     c.mark(1);
 469     ca.free(cr);
 470 }
 471
 472 bool Solver::satisfied(const Clause& c) const {
 473     if(incremental)
 474         return (value(c[0]) == l_True) || (value(c[1]) == l_True);
 475
 476     // Default mode
 477     for (int i = 0; i < c.size(); i++)
 478         if (value(c[i]) == l_True)
 479             return true;
 480     return false;
 481 }
 482
 483 /************************************************************
 484  * Compute LBD functions
 485  *************************************************************/
 486
 487 inline unsigned int Solver::computeLBD(const vec<Lit> & lits,int end) {
 488   int nblevels = 0;
 489   MYFLAG++;
 490
 491   if(incremental) { // ----------------- INCREMENTAL MODE
 492     if(end==-1) end = lits.size();
 493     int nbDone = 0;
 494     for(int i=0;i<lits.size();i++) {
 495       if(nbDone>=end) break;
 496       if(isSelector(var(lits[i]))) continue;
 497       nbDone++;
 498       int l = level(var(lits[i]));
 499       if (permDiff[l] != MYFLAG) {
 500         permDiff[l] = MYFLAG;
 501         nblevels++;
 502       }
 503     }
 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;
 509         nblevels++;
 510       }
 511     }
 512   }
 513
 514   if (!reduceOnSize)
 515     return nblevels;
 516   if (lits.size() < reduceOnSizeSize) return lits.size(); // See the XMinisat paper
 517     return lits.size() + nblevels;
 518 }
 519
 520 inline unsigned int Solver::computeLBD(const Clause &c) {
 521   int nblevels = 0;
 522   MYFLAG++;
 523
 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;
 529       nbDone++;
 530       int l = level(var(c[i]));
 531       if (permDiff[l] != MYFLAG) {
 532         permDiff[l] = MYFLAG;
 533         nblevels++;
 534       }
 535     }
 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;
 541         nblevels++;
 542       }
 543     }
 544   }
 545
 546   if (!reduceOnSize)
 547     return nblevels;
 548   if (c.size() < reduceOnSizeSize) return c.size(); // See the XMinisat paper
 549     return c.size() + nblevels;
 550
 551 }
 552
 553 /******************************************************************
 554  * Minimisation with binary reolution
 555  ******************************************************************/
 556 void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
 557
 558     // Find the LBD measure
 559     unsigned int lbd = computeLBD(out_learnt);
 560     Lit p = ~out_learnt[0];
 561
 562     if (lbd <= lbLBDMinimizingClause) {
 563         MYFLAG++;
 564
 565         for (int i = 1; i < out_learnt.size(); i++) {
 566             permDiff[var(out_learnt[i])] = MYFLAG;
 567         }
 568
 569         vec<Watcher>& wbin = watchesBin[p];
 570         int nb = 0;
 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) {
 574                 nb++;
 575                 permDiff[var(imp)] = MYFLAG - 1;
 576             }
 577         }
 578         int l = out_learnt.size() - 1;
 579         if (nb > 0) {
 580             nbReducedClauses++;
 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];
 585                     out_learnt[i] = p;
 586                     l--;
 587                     i--;
 588                 }
 589             }
 590
 591             out_learnt.shrink(nb);
 592
 593         }
 594     }
 595 }
 596
 597 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 598 //
 599
 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]);
 607             }
 608             insertVarOrder(x);
 609         }
 610         qhead = trail_lim[level];
 611         trail.shrink(trail.size() - trail_lim[level]);
 612         trail_lim.shrink(trail_lim.size() - level);
 613     }
 614 }
 615
 616
 617 //=================================================================================================
 618 // Major methods:
 619
 620 Lit Solver::pickBranchLit() {
 621     Var next = var_Undef;
 622
 623     // Random decision:
 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])
 627             rnd_decisions++;
 628     }
 629
 630     // Activity based decision:
 631     while (next == var_Undef || value(next) != l_Undef || !decision[next])
 632         if (order_heap.empty()) {
 633             next = var_Undef;
 634             break;
 635         } else {
 636             next = order_heap.removeMin();
 637         }
 638
 639     return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
 640 }
 641
 642 /*_________________________________________________________________________________________________
 643 |
 644 |  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
 645 |
 646 |  Description:
 647 |    Analyze conflict and produce a reason clause.
 648 |
 649 |    Pre-conditions:
 650 |      * 'out_learnt' is assumed to be cleared.
 651 |      * Current decision level must be greater than root level.
 652 |
 653 |    Post-conditions:
 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.
 657 |
 658 |________________________________________________________________________________________________@*/
 659 void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors) {
 660     int pathC = 0;
 661     Lit p = lit_Undef;
 662
 663
 664     // Generate conflict clause:
 665     //
 666     out_learnt.push(); // (leave room for the asserting literal)
 667     int index = trail.size() - 1;
 668     do {
 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) {
 674
 675             assert(value(c[1]) == l_True);
 676             Lit tmp = c[0];
 677             c[0] = c[1], c[1] = tmp;
 678         }
 679
 680         if (c.learnt()) {
 681             parallelImportClauseDuringConflictAnalysis(c,confl);
 682             claBumpActivity(c);
 683          } else { // original clause
 684             if (!c.getSeen()) {
 685                 originalClausesSeen++;
 686                 c.setSeen(true);
 687             }
 688         }
 689
 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);
 696                 }
 697                 // seems to be interesting : keep it for the next round
 698                 c.setLBD(nblevels); // Update it
 699             }
 700         }
 701
 702
 703         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) {
 704             Lit q = c[j];
 705
 706             if (!seen[var(q)]) {
 707                 if (level(var(q)) == 0) {
 708                 } else { // Here, the old case
 709                     if(!isSelector(var(q)))
 710                         varBumpActivity(var(q));
 711                     seen[var(q)] = 1;
 712                     if (level(var(q)) >= decisionLevel()) {
 713                         pathC++;
 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);
 717                     } else {
 718                         if(isSelector(var(q))) {
 719                             assert(value(q) == l_False);
 720                             selectors.push(q);
 721                         } else
 722                             out_learnt.push(q);
 723                    }
 724                 }
 725             }
 726         }
 727
 728         // Select next clause to look at:
 729         while (!seen[var(trail[index--])]);
 730         p = trail[index + 1];
 731         confl = reason(var(p));
 732         seen[var(p)] = 0;
 733         pathC--;
 734
 735     } while (pathC > 0);
 736     out_learnt[0] = ~p;
 737
 738     // Simplify conflict clause:
 739     //
 740     int i, j;
 741
 742     for (int i = 0; i < selectors.size(); i++)
 743         out_learnt.push(selectors[i]);
 744
 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)
 750
 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];
 754
 755     } else if (ccmin_mode == 1) {
 756         for (i = j = 1; i < out_learnt.size(); i++) {
 757             Var x = var(out_learnt[i]);
 758
 759             if (reason(x) == CRef_Undef)
 760                 out_learnt[j++] = out_learnt[i];
 761             else {
 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];
 767                         break;
 768                     }
 769             }
 770         }
 771     } else
 772         i = j = out_learnt.size();
 773
 774     max_literals += out_learnt.size();
 775     out_learnt.shrink(i - j);
 776     tot_literals += out_learnt.size();
 777
 778
 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
 784      */
 785     if (!incremental && out_learnt.size() <= lbSizeMinimizingClause) {
 786         minimisationWithBinaryResolution(out_learnt);
 787     }
 788     // Find correct backtrack level:
 789     //
 790     if (out_learnt.size() == 1)
 791         out_btlevel = 0;
 792     else {
 793         int max_i = 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])))
 797                 max_i = i;
 798         // Swap-in this literal at index 1:
 799         Lit p = out_learnt[max_i];
 800         out_learnt[max_i] = out_learnt[1];
 801         out_learnt[1] = p;
 802         out_btlevel = level(var(p));
 803     }
 804    if(incremental) {
 805       szWithoutSelectors = 0;
 806       for(int i=0;i<out_learnt.size();i++) {
 807         if(!isSelector(var((out_learnt[i])))) szWithoutSelectors++;
 808         else if(i>0) break;
 809       }
 810     } else
 811       szWithoutSelectors = out_learnt.size();
 812
 813     // Compute LBD
 814     lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size());
 815
 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]));
 821         }
 822         lastDecisionLevel.clear();
 823     }
 824
 825
 826
 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;
 829 }
 830
 831
 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.
 834
 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);
 845             Lit tmp = c[0];
 846             c[0] = c[1], c[1] = tmp;
 847         }
 848
 849         for (int i = 1; i < c.size(); i++) {
 850             Lit p = c[i];
 851             if (!seen[var(p)]) {
 852                 if (level(var(p)) > 0) {
 853                     if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0) {
 854                         seen[var(p)] = 1;
 855                         analyze_stack.push(p);
 856                         analyze_toclear.push(p);
 857                     } else {
 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);
 861                         return false;
 862                     }
 863                 }
 864             }
 865         }
 866     }
 867
 868     return true;
 869 }
 870
 871
 872 /*_________________________________________________________________________________________________
 873 |
 874 |  analyzeFinal : (p : Lit)  ->  [void]
 875 |
 876 |  Description:
 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);
 884
 885     if (decisionLevel() == 0)
 886         return;
 887
 888     seen[var(p)] = 1;
 889
 890     for (int i = trail.size() - 1; i >= trail_lim[0]; i--) {
 891         Var x = var(trail[i]);
 892         if (seen[x]) {
 893             if (reason(x) == CRef_Undef) {
 894                 assert(level(x) > 0);
 895                 out_conflict.push(~trail[i]);
 896             } else {
 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)
 903                         seen[var(c[j])] = 1;
 904             }
 905
 906             seen[x] = 0;
 907         }
 908     }
 909
 910     seen[var(p)] = 0;
 911 }
 912
 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());
 917     trail.push_(p);
 918 }
 919
 920 /*_________________________________________________________________________________________________
 921 |
 922 |  propagate : [void]  ->  [Clause*]
 923 |
 924 |  Description:
 925 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
 926 |    otherwise CRef_Undef.
 927 |
 928 |    Post-conditions:
 929 |      * the propagation queue is empty, even if there was a conflict.
 930 |________________________________________________________________________________________________@*/
 931 CRef Solver::propagate() {
 932     CRef confl = CRef_Undef;
 933     int num_props = 0;
 934     int previousqhead = qhead;
 935     watches.cleanAll();
 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;
 942         num_props++;
 943
 944
 945         // First, Propagate binary clauses
 946         vec<Watcher>& wbin = watchesBin[p];
 947
 948         for (int k = 0; k < wbin.size(); k++) {
 949
 950             Lit imp = wbin[k].blocker;
 951
 952             if (value(imp) == l_False) {
 953                 return wbin[k].cref;
 954             }
 955
 956             if (value(imp) == l_Undef) {
 957                 uncheckedEnqueue(imp, wbin[k].cref);
 958             }
 959         }
 960
 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) {
 966                 *j++ = *i++;
 967                 continue;
 968             }
 969
 970             // Make sure the false literal is data[1]:
 971             CRef cr = i->cref;
 972             Clause& c = ca[cr];
 973             assert(!c.getOneWatched());
 974             Lit false_lit = ~p;
 975             if (c[0] == false_lit)
 976                 c[0] = c[1], c[1] = false_lit;
 977             assert(c[1] == false_lit);
 978             i++;
 979
 980             // If 0th watch is true, then clause is already satisfied.
 981             Lit first = c[0];
 982             Watcher w = Watcher(cr, first);
 983             if (first != blocker && value(first) == l_True) {
 984
 985                 *j++ = w;
 986                 continue;
 987             }
 988             if(incremental) { // ----------------- INCREMENTAL MODE
 989               int choosenPos = -1;
 990               for (int k = 2; k < c.size(); k++) {
 991
 992                 if (value(c[k]) != l_False){
 993                   if(decisionLevel()>assumptions.size()) {
 994                     choosenPos = k;
 995                     break;
 996                   } else {
 997                     choosenPos = k;
 998
 999                     if(value(c[k])==l_True || !isSelector(var(c[k]))) {
1000                       break;
1001                     }
1002                   }
1003
1004                 }
1005               }
1006               if(choosenPos!=-1) {
1007                 c[1] = c[choosenPos]; c[choosenPos] = false_lit;
1008                 watches[~c[1]].push(w);
1009                 goto NextClause; }
1010             } else {  // ----------------- DEFAULT  MODE (NOT INCREMENTAL)
1011               for (int k = 2; k < c.size(); k++) {
1012
1013                 if (value(c[k]) != l_False){
1014                   c[1] = c[k]; c[k] = false_lit;
1015                   watches[~c[1]].push(w);
1016                   goto NextClause; }
1017               }
1018             }
1019
1020             // Did not find watch -- clause is unit under assignment:
1021             *j++ = w;
1022             if (value(first) == l_False) {
1023                 confl = cr;
1024                 qhead = trail.size();
1025                 // Copy the remaining watches:
1026                 while (i < end)
1027                     *j++ = *i++;
1028             } else {
1029                 uncheckedEnqueue(first, cr);
1030
1031
1032             }
1033 NextClause:
1034             ;
1035         }
1036         ws.shrink(i - j);
1037
1038        // unaryWatches "propagation"
1039         if (useUnaryWatched &&  confl == CRef_Undef) {
1040             confl = propagateUnaryWatches(p);
1041
1042         }
1043
1044     }
1045
1046
1047
1048     propagations += num_props;
1049     simpDB_props -= num_props;
1050
1051     return confl;
1052 }
1053
1054 /*_________________________________________________________________________________________________
1055 |
1056 |  propagateUnaryWatches : [Lit]  ->  [Clause*]
1057 |
1058 |  Description:
1059 |    Propagates unary watches of Lit p, return a conflict
1060 |    otherwise CRef_Undef
1061 |
1062 |________________________________________________________________________________________________@*/
1063
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) {
1072             *j++ = *i++;
1073             continue;
1074         }
1075
1076         // Make sure the false literal is data[1]:
1077         CRef cr = i->cref;
1078         Clause& c = ca[cr];
1079         assert(c.getOneWatched());
1080         Lit false_lit = ~p;
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);
1085         i++;
1086         Watcher w = Watcher(cr, c[0]);
1087         for (int k = 1; k < c.size(); k++) {
1088             if (value(c[k]) != l_False) {
1089                 c[0] = c[k];
1090                 c[k] = false_lit;
1091                 unaryWatches[~c[0]].push(w);
1092                 goto NextClauseUnary;
1093             }
1094         }
1095
1096         // Did not find watch -- clause is empty under assignment:
1097         *j++ = w;
1098
1099         confl = cr;
1100         qhead = trail.size();
1101         // Copy the remaining watches:
1102         while (i < end)
1103             *j++ = *i++;
1104
1105         // We can add it now to the set of clauses when backtracking
1106         //printf("*");
1107         if (promoteOneWatchedClause) {
1108             nbPromoted++;
1109             // Let's find the two biggest decision levels in the clause s.t. it will correctly be propagated when we'll backtrack
1110             int maxlevel = -1;
1111             int index = -1;
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) {
1116                     index = k;
1117                     maxlevel = level(var(c[k]));
1118                 }
1119             }
1120             detachClausePurgatory(cr, true); // TODO: check that the cleanAll is ok (use ",true" otherwise)
1121             assert(index != -1);
1122             Lit tmp = c[1];
1123             c[1] = c[index], c[index] = tmp;
1124             attachClause(cr);
1125             // TODO used in function ParallelSolver::reportProgressArrayImports
1126             //Override :-(
1127             //goodImportsFromThreads[ca[cr].importedFrom()]++;
1128             ca[cr].setOneWatched(false);
1129             ca[cr].setExported(2);
1130         }
1131 NextClauseUnary:
1132         ;
1133     }
1134     ws.shrink(i - j);
1135
1136     return confl;
1137 }
1138
1139 /*_________________________________________________________________________________________________
1140 |
1141 |  reduceDB : ()  ->  [void]
1142 |
1143 |  Description:
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 |________________________________________________________________________________________________@*/
1147
1148
1149 void Solver::reduceDB()
1150 {
1151
1152   int     i, j;
1153   nbReduceDB++;
1154   sort(learnts, reduceDB_lt(ca));
1155
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;
1158   // Useless :-)
1159   if(ca[learnts.last()].lbd()<=5)  nbclausesbeforereduce +=specialIncReduceDB;
1160
1161
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)
1164
1165   int limit = learnts.size() / 2;
1166
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]);
1171       nbRemovedClauses++;
1172     }
1173     else {
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];
1177     }
1178   }
1179   learnts.shrink(i - j);
1180   checkGarbage();
1181 }
1182
1183
1184 void Solver::removeSatisfied(vec<CRef>& cs) {
1185
1186     int i, j;
1187     for (i = j = 0; i < cs.size(); i++) {
1188         Clause& c = ca[cs[i]];
1189
1190
1191         if (satisfied(c))
1192             if (c.getOneWatched())
1193                 removeClause(cs[i], true);
1194             else
1195                 removeClause(cs[i]);
1196         else
1197             cs[j++] = cs[i];
1198     }
1199     cs.shrink(i - j);
1200 }
1201
1202 void Solver::rebuildOrderHeap() {
1203     vec<Var> vs;
1204     for (Var v = 0; v < nVars(); v++)
1205         if (decision[v] && value(v) == l_Undef)
1206             vs.push(v);
1207     order_heap.build(vs);
1208
1209 }
1210
1211 /*_________________________________________________________________________________________________
1212 |
1213 |  simplify : [void]  ->  [bool]
1214 |
1215 |  Description:
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);
1221
1222     if (!ok) return ok = false;
1223     else {
1224         CRef cr = propagate();
1225         if (cr != CRef_Undef) {
1226             return ok = false;
1227         }
1228     }
1229
1230
1231     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
1232         return true;
1233
1234     // Remove satisfied clauses:
1235     removeSatisfied(learnts);
1236     removeSatisfied(unaryWatchedClauses);
1237     if (remove_satisfied) // Can be turned off.
1238         removeSatisfied(clauses);
1239     checkGarbage();
1240     rebuildOrderHeap();
1241
1242     simpDB_assigns = nAssigns();
1243     simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
1244
1245     return true;
1246 }
1247
1248
1249 /*_________________________________________________________________________________________________
1250 |
1251 |  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
1252 |
1253 |  Description:
1254 |    Search for a model the specified number of conflicts.
1255 |    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
1256 |
1257 |  Output:
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) {
1263     assert(ok);
1264     int backtrack_level;
1265     int conflictC = 0;
1266     vec<Lit> learnt_clause, selectors;
1267     unsigned int nblevels,szWithoutSelectors = 0;
1268     bool blocked = false;
1269     starts++;
1270     for (;;) {
1271         if (decisionLevel() == 0) { // We import clauses FIXME: ensure that we will import clauses enventually (restart after some point)
1272             parallelImportUnaryClauses();
1273
1274             if (parallelImportClauses())
1275                 return l_False;
1276
1277         }
1278         CRef confl = propagate();
1279
1280         if (confl != CRef_Undef) {
1281             if(parallelJobIsFinished())
1282                 return l_Undef;
1283
1284
1285             sumDecisionLevels += decisionLevel();
1286             // CONFLICT
1287             conflicts++;
1288             conflictC++;
1289             conflictsRestarts++;
1290            if (conflicts % 5000 == 0 && var_decay < max_var_decay)
1291                 var_decay += 0.01;
1292
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);
1298             }
1299             if (decisionLevel() == 0) {
1300                 return l_False;
1301
1302             }
1303
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();
1308                 nbstopsrestarts++;
1309                 if (!blocked) {
1310                     lastblockatrestart = starts;
1311                     nbstopsrestartssame++;
1312                     blocked = true;
1313                 }
1314             }
1315
1316             learnt_clause.clear();
1317             selectors.clear();
1318
1319             analyze(confl, learnt_clause, selectors, backtrack_level, nblevels,szWithoutSelectors);
1320
1321             lbdQueue.push(nblevels);
1322             sumLBD += nblevels;
1323
1324             cancelUntil(backtrack_level);
1325
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");
1331             }
1332
1333
1334             if (learnt_clause.size() == 1) {
1335                 uncheckedEnqueue(learnt_clause[0]);
1336                 nbUn++;
1337                 parallelExportUnaryClause(learnt_clause[0]);
1338             } else {
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
1345                 learnts.push(cr);
1346                 attachClause(cr);
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);
1351
1352             }
1353             varDecayActivity();
1354             claDecayActivity();
1355
1356
1357         } else {
1358             // Our dynamic restart, see the SAT09 competition compagnion paper
1359             if (
1360                     (lbdQueue.isvalid() && ((lbdQueue.getavg() * K) > (sumLBD / conflictsRestarts)))) {
1361                 lbdQueue.fastclear();
1362                 progress_estimate = progressEstimate();
1363                 int bt = 0;
1364                 if(incremental) // DO NOT BACKTRACK UNTIL 0.. USELESS
1365                     bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
1366                 cancelUntil(bt);
1367                 return l_Undef;
1368             }
1369
1370
1371             // Simplify the set of problem clauses:
1372             if (decisionLevel() == 0 && !simplify()) {
1373                 return l_False;
1374             }
1375             // Perform clause database reduction !
1376             if (conflicts >= ((unsigned int) curRestart * nbclausesbeforereduce)) {
1377
1378                 if (learnts.size() > 0) {
1379                     curRestart = (conflicts / nbclausesbeforereduce) + 1;
1380                     reduceDB();
1381                     if (!panicModeIsEnabled())
1382                         nbclausesbeforereduce += incReduceDB;
1383                 }
1384             }
1385
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:
1393                     newDecisionLevel();
1394                 } else if (value(p) == l_False) {
1395                     analyzeFinal(~p, conflict);
1396                     return l_False;
1397                 } else {
1398                     next = p;
1399                     break;
1400                 }
1401             }
1402
1403             if (next == lit_Undef) {
1404                 // New variable decision:
1405                 decisions++;
1406                 next = pickBranchLit();
1407                 if (next == lit_Undef) {
1408                     printf("c last restart ## conflicts  :  %d %d \n", conflictC, decisionLevel());
1409                     // Model found:
1410                     return l_True;
1411                 }
1412             }
1413
1414             // Increase decision level and enqueue 'next'
1415             newDecisionLevel();
1416             uncheckedEnqueue(next);
1417         }
1418     }
1419 }
1420
1421 double Solver::progressEstimate() const {
1422     double progress = 0;
1423     double F = 1.0 / nVars();
1424
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);
1429     }
1430
1431     return progress / nVars();
1432 }
1433
1434 void Solver::printIncrementalStats() {
1435
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);
1443
1444     printf("c conflicts             : %" PRIu64"\n", conflicts);
1445     printf("c decisions             : %" PRIu64"\n", decisions);
1446     printf("c propagations          : %" PRIu64"\n", propagations);
1447
1448   printf("\nc SAT Calls             : %d in %g seconds\n",nbSatCalls,totalTime4Sat);
1449   printf("c UNSAT Calls           : %d in %g seconds\n",nbUnsatCalls,totalTime4Unsat);
1450
1451     printf("c--------------------------------------------------\n");
1452 }
1453
1454 // NOTE: assumptions passed in member-variable 'assumptions'.
1455
1456 lbool Solver::solve_(bool do_simp, bool turn_off_simp) // Parameters are useless in core but useful for SimpSolver....
1457 {
1458
1459     if(incremental && certifiedUNSAT) {
1460     printf("Can not use incremental and certified unsat in the same time\n");
1461     exit(-1);
1462   }
1463
1464     model.clear();
1465     conflict.clear();
1466     if (!ok) return l_False;
1467     double curTime = cpuTime();
1468
1469     solves++;
1470
1471
1472
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);
1487       printf("c |                                                                                                       |\n");
1488
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");
1492     }
1493
1494     // Search:
1495     int curr_restarts = 0;
1496     while (status == l_Undef){
1497       status = search(0); // the parameter is useless in glucose, kept to allow modifications
1498
1499         if (!withinBudget()) break;
1500         curr_restarts++;
1501     }
1502
1503     if (!incremental && verbosity >= 1)
1504       printf("c =========================================================================================================\n");
1505
1506     if (certifiedUNSAT){ // Want certified output
1507       if (status == l_False)
1508         fprintf(certifiedOutput, "0\n");
1509       fclose(certifiedOutput);
1510     }
1511
1512
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)
1518         ok = false;
1519
1520
1521
1522     cancelUntil(0);
1523
1524
1525     double finalTime = cpuTime();
1526     if(status==l_True) {
1527         nbSatCalls++;
1528         totalTime4Sat +=(finalTime-curTime);
1529     }
1530     if(status==l_False) {
1531         nbUnsatCalls++;
1532         totalTime4Unsat +=(finalTime-curTime);
1533     }
1534
1535
1536     return status;
1537
1538 }
1539
1540
1541
1542
1543
1544 //=================================================================================================
1545 // Writing CNF to DIMACS:
1546 //
1547 // FIXME: this needs to be rewritten completely.
1548
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);
1552         map[x] = max++;
1553     }
1554     return map[x];
1555 }
1556
1557 void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max) {
1558     if (satisfied(c)) return;
1559
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);
1563     fprintf(f, "0\n");
1564 }
1565
1566 void Solver::toDimacs(const char *file, const vec<Lit>& assumps) {
1567     FILE* f = fopen(file, "wr");
1568     if (f == NULL)
1569         fprintf(stderr, "could not open file %s\n", file), exit(1);
1570     toDimacs(f, assumps);
1571     fclose(f);
1572 }
1573
1574 void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) {
1575     // Handle case when solver is in contradictory state:
1576     if (!ok) {
1577         fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
1578         return;
1579     }
1580
1581     vec<Var> map;
1582     Var max = 0;
1583
1584     // Cannot use removeClauses here because it is not safe
1585     // to deallocate them at this point. Could be improved.
1586     int cnt = 0;
1587     for (int i = 0; i < clauses.size(); i++)
1588         if (!satisfied(ca[clauses[i]]))
1589             cnt++;
1590
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);
1597         }
1598
1599     // Assumptions are added as unit clauses:
1600     cnt += assumptions.size();
1601
1602     fprintf(f, "p cnf %d %d\n", max, cnt);
1603
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);
1607     }
1608
1609     for (int i = 0; i < clauses.size(); i++)
1610         toDimacs(f, ca[clauses[i]], map, max);
1611
1612     if (verbosity > 0)
1613         printf("Wrote %d clauses with %d variables.\n", cnt, max);
1614 }
1615
1616
1617 //=================================================================================================
1618 // Garbage Collection methods:
1619
1620 void Solver::relocAll(ClauseAllocator& to) {
1621     // All watchers:
1622     //
1623     // for (int i = 0; i < watches.size(); i++)
1624     watches.cleanAll();
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);
1640         }
1641
1642     // All reasons:
1643     //
1644     for (int i = 0; i < trail.size(); i++) {
1645         Var v = var(trail[i]);
1646
1647         if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
1648             ca.reloc(vardata[v].reason, to);
1649     }
1650
1651     // All learnt:
1652     //
1653     for (int i = 0; i < learnts.size(); i++)
1654         ca.reloc(learnts[i], to);
1655
1656     // All original:
1657     //
1658     for (int i = 0; i < clauses.size(); i++)
1659         ca.reloc(clauses[i], to);
1660
1661     for (int i = 0; i < unaryWatchedClauses.size(); i++)
1662         ca.reloc(unaryWatchedClauses[i], to);
1663 }
1664
1665
1666
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());
1671
1672     relocAll(to);
1673     if (verbosity >= 2)
1674         printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n",
1675             ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size);
1676     to.moveTo(ca);
1677 }
1678
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 //--------------------------------------------------------------
1684
1685 bool Solver::panicModeIsEnabled() {
1686     return false;
1687 }
1688
1689 void Solver::parallelImportUnaryClauses() {
1690 }
1691
1692 bool Solver::parallelImportClauses() {
1693     return false;
1694 }
1695
1696
1697 void Solver::parallelExportUnaryClause(Lit p) {
1698 }
1699 void Solver::parallelExportClauseDuringSearch(Clause &c) {
1700 }
1701
1702 bool Solver::parallelJobIsFinished() {
1703     // Parallel: another job has finished let's quit
1704     return false;
1705 }
1706
1707 void Solver::parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl) {
1708 }