glucose-syrup/incremental/SimpSolver.cc

   1 /***************************************************************************************[SimpSolver.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 "mtl/Sort.h"
  51 #include "simp/SimpSolver.h"
  52 #include "utils/System.h"
  53
  54 using namespace Glucose;
  55
  56 //=================================================================================================
  57 // Options:
  58
  59
  60 static const char* _cat = "SIMP";
  61
  62 static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
  63 static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
  64 static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
  65 static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
  66 static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
  67 static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
  68 static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.",  0.5, DoubleRange(0, false, HUGE_VAL, false));
  69
  70
  71 //=================================================================================================
  72 // Constructor/Destructor:
  73
  74
  75 SimpSolver::SimpSolver() :
  76    Solver()
  77   , grow               (opt_grow)
  78   , clause_lim         (opt_clause_lim)
  79   , subsumption_lim    (opt_subsumption_lim)
  80   , simp_garbage_frac  (opt_simp_garbage_frac)
  81   , use_asymm          (opt_use_asymm)
  82   , use_rcheck         (opt_use_rcheck)
  83   , use_elim           (opt_use_elim)
  84   , merges             (0)
  85   , asymm_lits         (0)
  86   , eliminated_vars    (0)
  87   , elimorder          (1)
  88   , use_simplification (true)
  89   , occurs             (ClauseDeleted(ca))
  90   , elim_heap          (ElimLt(n_occ))
  91   , bwdsub_assigns     (0)
  92   , n_touched          (0)
  93 {
  94     vec<Lit> dummy(1,lit_Undef);
  95     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
  96     bwdsub_tmpunit        = ca.alloc(dummy);
  97     remove_satisfied      = false;
  98 }
  99
 100
 101 SimpSolver::~SimpSolver()
 102 {
 103 }
 104
 105
 106
 107 SimpSolver::SimpSolver(const SimpSolver &s) : Solver(s)
 108   , grow               (s.grow)
 109   , clause_lim         (s.clause_lim)
 110   , subsumption_lim    (s.subsumption_lim)
 111   , simp_garbage_frac  (s.simp_garbage_frac)
 112   , use_asymm          (s.use_asymm)
 113   , use_rcheck         (s.use_rcheck)
 114   , use_elim           (s.use_elim)
 115   , merges             (s.merges)
 116   , asymm_lits         (s.asymm_lits)
 117   , eliminated_vars    (s.eliminated_vars)
 118   , elimorder          (s.elimorder)
 119   , use_simplification (s.use_simplification)
 120   , occurs             (ClauseDeleted(ca))
 121   , elim_heap          (ElimLt(n_occ))
 122   , bwdsub_assigns     (s.bwdsub_assigns)
 123   , n_touched          (s.n_touched)
 124 {
 125     // TODO: Copy dummy... what is it???
 126     vec<Lit> dummy(1,lit_Undef);
 127     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
 128     bwdsub_tmpunit        = ca.alloc(dummy);
 129     remove_satisfied      = false;
 130     //End TODO
 131
 132
 133     s.elimclauses.memCopyTo(elimclauses);
 134     s.touched.memCopyTo(touched);
 135     s.occurs.copyTo(occurs);
 136     s.n_occ.memCopyTo(n_occ);
 137     s.elim_heap.copyTo(elim_heap);
 138     s.subsumption_queue.copyTo(subsumption_queue);
 139     s.frozen.memCopyTo(frozen);
 140     s.eliminated.memCopyTo(eliminated);
 141
 142     use_simplification = s.use_simplification;
 143     bwdsub_assigns = s.bwdsub_assigns;
 144     n_touched = s.n_touched;
 145     bwdsub_tmpunit = s.bwdsub_tmpunit;
 146     qhead = s.qhead;
 147     ok = s.ok;
 148 }
 149
 150
 151
 152 Var SimpSolver::newVar(bool sign, bool dvar) {
 153     Var v = Solver::newVar(sign, dvar);
 154     frozen    .push((char)false);
 155     eliminated.push((char)false);
 156
 157     if (use_simplification){
 158         n_occ     .push(0);
 159         n_occ     .push(0);
 160         occurs    .init(v);
 161         touched   .push(0);
 162         elim_heap .insert(v);
 163     }
 164     return v; }
 165
 166 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 167 {
 168     vec<Var> extra_frozen;
 169     lbool    result = l_True;
 170     do_simp &= use_simplification;
 171
 172     if (do_simp){
 173         // Assumptions must be temporarily frozen to run variable elimination:
 174         for (int i = 0; i < assumptions.size(); i++){
 175             Var v = var(assumptions[i]);
 176
 177             // If an assumption has been eliminated, remember it.
 178             assert(!isEliminated(v));
 179
 180             if (!frozen[v]){
 181                 // Freeze and store.
 182                 setFrozen(v, true);
 183                 extra_frozen.push(v);
 184             } }
 185
 186         result = lbool(eliminate(turn_off_simp));
 187     }
 188
 189     if (result == l_True)
 190         result = Solver::solve_();
 191     else if (verbosity >= 1)
 192         printf("===============================================================================\n");
 193
 194     if (result == l_True)
 195         extendModel();
 196
 197     if (do_simp)
 198         // Unfreeze the assumptions that were frozen:
 199         for (int i = 0; i < extra_frozen.size(); i++)
 200             setFrozen(extra_frozen[i], false);
 201
 202
 203     return result;
 204 }
 205
 206
 207
 208 bool SimpSolver::addClause_(vec<Lit>& ps)
 209 {
 210 #ifndef NDEBUG
 211     for (int i = 0; i < ps.size(); i++)
 212         assert(!isEliminated(var(ps[i])));
 213 #endif
 214     int nclauses = clauses.size();
 215
 216     if (use_rcheck && implied(ps))
 217         return true;
 218
 219     if (!Solver::addClause_(ps))
 220         return false;
 221
 222     if(!parsing && certifiedUNSAT) {
 223       for (int i = 0; i < ps.size(); i++)
 224         fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) );
 225       fprintf(certifiedOutput, "0\n");
 226     }
 227
 228     if (use_simplification && clauses.size() == nclauses + 1){
 229         CRef          cr = clauses.last();
 230         const Clause& c  = ca[cr];
 231
 232         // NOTE: the clause is added to the queue immediately and then
 233         // again during 'gatherTouchedClauses()'. If nothing happens
 234         // in between, it will only be checked once. Otherwise, it may
 235         // be checked twice unnecessarily. This is an unfortunate
 236         // consequence of how backward subsumption is used to mimic
 237         // forward subsumption.
 238         subsumption_queue.insert(cr);
 239         for (int i = 0; i < c.size(); i++){
 240             occurs[var(c[i])].push(cr);
 241             n_occ[toInt(c[i])]++;
 242             touched[var(c[i])] = 1;
 243             n_touched++;
 244             if (elim_heap.inHeap(var(c[i])))
 245                 elim_heap.increase(var(c[i]));
 246         }
 247     }
 248
 249     return true;
 250 }
 251
 252
 253
 254 void SimpSolver::removeClause(CRef cr,bool inPurgatory)
 255 {
 256     const Clause& c = ca[cr];
 257
 258     if (use_simplification)
 259         for (int i = 0; i < c.size(); i++){
 260             n_occ[toInt(c[i])]--;
 261             updateElimHeap(var(c[i]));
 262             occurs.smudge(var(c[i]));
 263         }
 264
 265     Solver::removeClause(cr,inPurgatory);
 266 }
 267
 268
 269 bool SimpSolver::strengthenClause(CRef cr, Lit l)
 270 {
 271     Clause& c = ca[cr];
 272     assert(decisionLevel() == 0);
 273     assert(use_simplification);
 274
 275     // FIX: this is too inefficient but would be nice to have (properly implemented)
 276     // if (!find(subsumption_queue, &c))
 277     subsumption_queue.insert(cr);
 278
 279     if (certifiedUNSAT) {
 280       for (int i = 0; i < c.size(); i++)
 281         if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
 282       fprintf(certifiedOutput, "0\n");
 283     }
 284
 285     if (c.size() == 2){
 286         removeClause(cr);
 287         c.strengthen(l);
 288     }else{
 289         if (certifiedUNSAT) {
 290           fprintf(certifiedOutput, "d ");
 291           for (int i = 0; i < c.size(); i++)
 292             fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
 293           fprintf(certifiedOutput, "0\n");
 294         }
 295
 296         detachClause(cr, true);
 297         c.strengthen(l);
 298         attachClause(cr);
 299         remove(occurs[var(l)], cr);
 300         n_occ[toInt(l)]--;
 301         updateElimHeap(var(l));
 302     }
 303
 304     return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
 305 }
 306
 307
 308 // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
 309 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
 310 {
 311     merges++;
 312     out_clause.clear();
 313
 314     bool  ps_smallest = _ps.size() < _qs.size();
 315     const Clause& ps  =  ps_smallest ? _qs : _ps;
 316     const Clause& qs  =  ps_smallest ? _ps : _qs;
 317
 318     for (int i = 0; i < qs.size(); i++){
 319         if (var(qs[i]) != v){
 320             for (int j = 0; j < ps.size(); j++)
 321                 if (var(ps[j]) == var(qs[i]))
 322                     if (ps[j] == ~qs[i])
 323                         return false;
 324                     else
 325                         goto next;
 326             out_clause.push(qs[i]);
 327         }
 328         next:;
 329     }
 330
 331     for (int i = 0; i < ps.size(); i++)
 332         if (var(ps[i]) != v)
 333             out_clause.push(ps[i]);
 334
 335     return true;
 336 }
 337
 338
 339 // Returns FALSE if clause is always satisfied.
 340 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 341 {
 342     merges++;
 343
 344     bool  ps_smallest = _ps.size() < _qs.size();
 345     const Clause& ps  =  ps_smallest ? _qs : _ps;
 346     const Clause& qs  =  ps_smallest ? _ps : _qs;
 347     const Lit*  __ps  = (const Lit*)ps;
 348     const Lit*  __qs  = (const Lit*)qs;
 349
 350     size = ps.size()-1;
 351
 352     for (int i = 0; i < qs.size(); i++){
 353         if (var(__qs[i]) != v){
 354             for (int j = 0; j < ps.size(); j++)
 355                 if (var(__ps[j]) == var(__qs[i]))
 356                     if (__ps[j] == ~__qs[i])
 357                         return false;
 358                     else
 359                         goto next;
 360             size++;
 361         }
 362         next:;
 363     }
 364
 365     return true;
 366 }
 367
 368
 369 void SimpSolver::gatherTouchedClauses()
 370 {
 371     if (n_touched == 0) return;
 372
 373     int i,j;
 374     for (i = j = 0; i < subsumption_queue.size(); i++)
 375         if (ca[subsumption_queue[i]].mark() == 0)
 376             ca[subsumption_queue[i]].mark(2);
 377
 378     for (i = 0; i < touched.size(); i++)
 379         if (touched[i]){
 380             const vec<CRef>& cs = occurs.lookup(i);
 381             for (j = 0; j < cs.size(); j++)
 382                 if (ca[cs[j]].mark() == 0){
 383                     subsumption_queue.insert(cs[j]);
 384                     ca[cs[j]].mark(2);
 385                 }
 386             touched[i] = 0;
 387         }
 388
 389     for (i = 0; i < subsumption_queue.size(); i++)
 390         if (ca[subsumption_queue[i]].mark() == 2)
 391             ca[subsumption_queue[i]].mark(0);
 392
 393     n_touched = 0;
 394 }
 395
 396
 397 bool SimpSolver::implied(const vec<Lit>& c)
 398 {
 399     assert(decisionLevel() == 0);
 400
 401     trail_lim.push(trail.size());
 402     for (int i = 0; i < c.size(); i++)
 403         if (value(c[i]) == l_True){
 404             cancelUntil(0);
 405             return false;
 406         }else if (value(c[i]) != l_False){
 407             assert(value(c[i]) == l_Undef);
 408             uncheckedEnqueue(~c[i]);
 409         }
 410
 411     bool result = propagate() != CRef_Undef;
 412     cancelUntil(0);
 413     return result;
 414 }
 415
 416
 417 // Backward subsumption + backward subsumption resolution
 418 bool SimpSolver::backwardSubsumptionCheck(bool verbose)
 419 {
 420     int cnt = 0;
 421     int subsumed = 0;
 422     int deleted_literals = 0;
 423     assert(decisionLevel() == 0);
 424
 425     while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
 426
 427         // Empty subsumption queue and return immediately on user-interrupt:
 428         if (asynch_interrupt){
 429             subsumption_queue.clear();
 430             bwdsub_assigns = trail.size();
 431             break; }
 432
 433         // Check top-level assignments by creating a dummy clause and placing it in the queue:
 434         if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
 435             Lit l = trail[bwdsub_assigns++];
 436             ca[bwdsub_tmpunit][0] = l;
 437             ca[bwdsub_tmpunit].calcAbstraction();
 438             subsumption_queue.insert(bwdsub_tmpunit); }
 439
 440         CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
 441         Clause& c  = ca[cr];
 442
 443         if (c.mark()) continue;
 444
 445         if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
 446             printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
 447
 448         assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.
 449
 450         // Find best variable to scan:
 451         Var best = var(c[0]);
 452         for (int i = 1; i < c.size(); i++)
 453             if (occurs[var(c[i])].size() < occurs[best].size())
 454                 best = var(c[i]);
 455
 456         // Search all candidates:
 457         vec<CRef>& _cs = occurs.lookup(best);
 458         CRef*       cs = (CRef*)_cs;
 459
 460         for (int j = 0; j < _cs.size(); j++)
 461             if (c.mark())
 462                 break;
 463             else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
 464                 Lit l = c.subsumes(ca[cs[j]]);
 465
 466                 if (l == lit_Undef)
 467                     subsumed++, removeClause(cs[j]);
 468                 else if (l != lit_Error){
 469                     deleted_literals++;
 470
 471                     if (!strengthenClause(cs[j], ~l))
 472                         return false;
 473
 474                     // Did current candidate get deleted from cs? Then check candidate at index j again:
 475                     if (var(l) == best)
 476                         j--;
 477                 }
 478             }
 479     }
 480
 481     return true;
 482 }
 483
 484
 485 bool SimpSolver::asymm(Var v, CRef cr)
 486 {
 487     Clause& c = ca[cr];
 488     assert(decisionLevel() == 0);
 489
 490     if (c.mark() || satisfied(c)) return true;
 491
 492     trail_lim.push(trail.size());
 493     Lit l = lit_Undef;
 494     for (int i = 0; i < c.size(); i++)
 495         if (var(c[i]) != v && value(c[i]) != l_False)
 496             uncheckedEnqueue(~c[i]);
 497         else
 498             l = c[i];
 499
 500     if (propagate() != CRef_Undef){
 501         cancelUntil(0);
 502         asymm_lits++;
 503         if (!strengthenClause(cr, l))
 504             return false;
 505     }else
 506         cancelUntil(0);
 507
 508     return true;
 509 }
 510
 511
 512 bool SimpSolver::asymmVar(Var v)
 513 {
 514     assert(use_simplification);
 515
 516     const vec<CRef>& cls = occurs.lookup(v);
 517
 518     if (value(v) != l_Undef || cls.size() == 0)
 519         return true;
 520
 521     for (int i = 0; i < cls.size(); i++)
 522         if (!asymm(v, cls[i]))
 523             return false;
 524
 525     return backwardSubsumptionCheck();
 526 }
 527
 528
 529 static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
 530 {
 531     elimclauses.push(toInt(x));
 532     elimclauses.push(1);
 533 }
 534
 535
 536 static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
 537 {
 538     int first = elimclauses.size();
 539     int v_pos = -1;
 540
 541     // Copy clause to elimclauses-vector. Remember position where the
 542     // variable 'v' occurs:
 543     for (int i = 0; i < c.size(); i++){
 544         elimclauses.push(toInt(c[i]));
 545         if (var(c[i]) == v)
 546             v_pos = i + first;
 547     }
 548     assert(v_pos != -1);
 549
 550     // Swap the first literal with the 'v' literal, so that the literal
 551     // containing 'v' will occur first in the clause:
 552     uint32_t tmp = elimclauses[v_pos];
 553     elimclauses[v_pos] = elimclauses[first];
 554     elimclauses[first] = tmp;
 555
 556     // Store the length of the clause last:
 557     elimclauses.push(c.size());
 558 }
 559
 560
 561
 562 bool SimpSolver::eliminateVar(Var v)
 563 {
 564     assert(!frozen[v]);
 565     assert(!isEliminated(v));
 566     assert(value(v) == l_Undef);
 567
 568     // Split the occurrences into positive and negative:
 569     //
 570     const vec<CRef>& cls = occurs.lookup(v);
 571     vec<CRef>        pos, neg;
 572     for (int i = 0; i < cls.size(); i++)
 573         (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
 574
 575     // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
 576     // clause must exceed the limit on the maximal clause size (if it is set):
 577     //
 578     int cnt         = 0;
 579     int clause_size = 0;
 580
 581     for (int i = 0; i < pos.size(); i++)
 582         for (int j = 0; j < neg.size(); j++)
 583             if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
 584                 (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
 585                 return true;
 586
 587     // Delete and store old clauses:
 588     eliminated[v] = true;
 589     setDecisionVar(v, false);
 590     eliminated_vars++;
 591
 592     if (pos.size() > neg.size()){
 593         for (int i = 0; i < neg.size(); i++)
 594             mkElimClause(elimclauses, v, ca[neg[i]]);
 595         mkElimClause(elimclauses, mkLit(v));
 596     }else{
 597         for (int i = 0; i < pos.size(); i++)
 598             mkElimClause(elimclauses, v, ca[pos[i]]);
 599         mkElimClause(elimclauses, ~mkLit(v));
 600     }
 601
 602
 603     // Produce clauses in cross product:
 604     vec<Lit>& resolvent = add_tmp;
 605     for (int i = 0; i < pos.size(); i++)
 606         for (int j = 0; j < neg.size(); j++)
 607             if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
 608                 return false;
 609
 610     for (int i = 0; i < cls.size(); i++)
 611         removeClause(cls[i]);
 612
 613     // Free occurs list for this variable:
 614     occurs[v].clear(true);
 615
 616     // Free watchers lists for this variable, if possible:
 617     if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
 618     if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
 619
 620     return backwardSubsumptionCheck();
 621 }
 622
 623
 624 bool SimpSolver::substitute(Var v, Lit x)
 625 {
 626     assert(!frozen[v]);
 627     assert(!isEliminated(v));
 628     assert(value(v) == l_Undef);
 629
 630     if (!ok) return false;
 631
 632     eliminated[v] = true;
 633     setDecisionVar(v, false);
 634     const vec<CRef>& cls = occurs.lookup(v);
 635
 636     vec<Lit>& subst_clause = add_tmp;
 637     for (int i = 0; i < cls.size(); i++){
 638         Clause& c = ca[cls[i]];
 639
 640         subst_clause.clear();
 641         for (int j = 0; j < c.size(); j++){
 642             Lit p = c[j];
 643             subst_clause.push(var(p) == v ? x ^ sign(p) : p);
 644         }
 645
 646
 647         if (!addClause_(subst_clause))
 648             return ok = false;
 649
 650        removeClause(cls[i]);
 651
 652    }
 653
 654     return true;
 655 }
 656
 657
 658 void SimpSolver::extendModel()
 659 {
 660     int i, j;
 661     Lit x;
 662
 663     if(model.size()==0) model.growTo(nVars());
 664
 665     for (i = elimclauses.size()-1; i > 0; i -= j){
 666         for (j = elimclauses[i--]; j > 1; j--, i--)
 667             if (modelValue(toLit(elimclauses[i])) != l_False)
 668                 goto next;
 669
 670         x = toLit(elimclauses[i]);
 671         model[var(x)] = lbool(!sign(x));
 672     next:;
 673     }
 674 }
 675
 676
 677 bool SimpSolver::eliminate(bool turn_off_elim)
 678 {
 679     if (!simplify()) {
 680         ok = false;
 681         return false;
 682     }
 683     else if (!use_simplification)
 684         return true;
 685
 686     // Main simplification loop:
 687     //
 688
 689     int toPerform = clauses.size()<=4800000;
 690
 691     if(!toPerform) {
 692       printf("c Too many clauses... No preprocessing\n");
 693     }
 694
 695     while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
 696
 697         gatherTouchedClauses();
 698         // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
 699         if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
 700             !backwardSubsumptionCheck(true)){
 701             ok = false; goto cleanup; }
 702
 703         // Empty elim_heap and return immediately on user-interrupt:
 704         if (asynch_interrupt){
 705             assert(bwdsub_assigns == trail.size());
 706             assert(subsumption_queue.size() == 0);
 707             assert(n_touched == 0);
 708             elim_heap.clear();
 709             goto cleanup; }
 710
 711         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
 712         for (int cnt = 0; !elim_heap.empty(); cnt++){
 713             Var elim = elim_heap.removeMin();
 714
 715             if (asynch_interrupt) break;
 716
 717             if (isEliminated(elim) || value(elim) != l_Undef) continue;
 718
 719             if (verbosity >= 2 && cnt % 100 == 0)
 720                 printf("elimination left: %10d\r", elim_heap.size());
 721
 722             if (use_asymm){
 723                 // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
 724                 bool was_frozen = frozen[elim];
 725                 frozen[elim] = true;
 726                 if (!asymmVar(elim)){
 727                     ok = false; goto cleanup; }
 728                 frozen[elim] = was_frozen; }
 729
 730             // At this point, the variable may have been set by assymetric branching, so check it
 731             // again. Also, don't eliminate frozen variables:
 732             if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
 733                 ok = false; goto cleanup; }
 734
 735             checkGarbage(simp_garbage_frac);
 736         }
 737
 738         assert(subsumption_queue.size() == 0);
 739     }
 740  cleanup:
 741
 742     // If no more simplification is needed, free all simplification-related data structures:
 743     if (turn_off_elim){
 744         touched  .clear(true);
 745         occurs   .clear(true);
 746         n_occ    .clear(true);
 747         elim_heap.clear(true);
 748         subsumption_queue.clear(true);
 749
 750         use_simplification    = false;
 751         remove_satisfied      = true;
 752         ca.extra_clause_field = false;
 753
 754         // Force full cleanup (this is safe and desirable since it only happens once):
 755         rebuildOrderHeap();
 756         garbageCollect();
 757     }else{
 758         // Cheaper cleanup:
 759         cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
 760         checkGarbage();
 761     }
 762
 763     if (verbosity >= 0 && elimclauses.size() > 0)
 764         printf("c |  Eliminated clauses:     %10.2f Mb                                                                |\n",
 765                double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
 766
 767
 768     return ok;
 769
 770
 771 }
 772
 773
 774 void SimpSolver::cleanUpClauses()
 775 {
 776     occurs.cleanAll();
 777     int i,j;
 778     for (i = j = 0; i < clauses.size(); i++)
 779         if (ca[clauses[i]].mark() == 0)
 780             clauses[j++] = clauses[i];
 781     clauses.shrink(i - j);
 782 }
 783
 784
 785 //=================================================================================================
 786 // Garbage Collection methods:
 787
 788
 789 void SimpSolver::relocAll(ClauseAllocator& to)
 790 {
 791     if (!use_simplification) return;
 792
 793     // All occurs lists:
 794     //
 795     for (int i = 0; i < nVars(); i++){
 796         vec<CRef>& cs = occurs[i];
 797         for (int j = 0; j < cs.size(); j++)
 798             ca.reloc(cs[j], to);
 799     }
 800
 801     // Subsumption queue:
 802     //
 803     for (int i = 0; i < subsumption_queue.size(); i++)
 804         ca.reloc(subsumption_queue[i], to);
 805
 806     // Temporary clause:
 807     //
 808     ca.reloc(bwdsub_tmpunit, to);
 809 }
 810
 811
 812 void SimpSolver::garbageCollect()
 813 {
 814     // Initialize the next region to a size corresponding to the estimated utilization degree. This
 815     // is not precise but should avoid some unnecessary reallocations for the new region:
 816     ClauseAllocator to(ca.size() - ca.wasted());
 817
 818     cleanUpClauses();
 819     to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
 820     relocAll(to);
 821     Solver::relocAll(to);
 822     if (verbosity >= 2)
 823         printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n",
 824                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
 825     to.moveTo(ca);
 826 }