backends/minisat/core/Solver.C

   1 /****************************************************************************************[Solver.C]
   2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   5 associated documentation files (the "Software"), to deal in the Software without restriction,
   6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   8 furnished to do so, subject to the following conditions:
   9
  10 The above copyright notice and this permission notice shall be included in all copies or
  11 substantial portions of the Software.
  12
  13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  18 **************************************************************************************************/
  19
  20 #include "Solver.h"
  21 #include "Sort.h"
  22 #include <cmath>
  23
  24
  25 //=================================================================================================
  26 // Constructor/Destructor:
  27
  28
  29 Solver::Solver() :
  30
  31     // Parameters: (formerly in 'SearchParams')
  32     var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
  33   , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
  34
  35     // More parameters:
  36     //
  37   , expensive_ccmin  (true)
  38   , polarity_mode    (polarity_false)
  39   , verbosity        (0)
  40
  41     // Statistics: (formerly in 'SolverStats')
  42     //
  43   , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
  44   , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
  45
  46   , ok               (true)
  47   , cla_inc          (1)
  48   , var_inc          (1)
  49   , qhead            (0)
  50   , simpDB_assigns   (-1)
  51   , simpDB_props     (0)
  52   , order_heap       (VarOrderLt(activity))
  53   , random_seed      (91648253)
  54   , progress_estimate(0)
  55   , remove_satisfied (true)
  56 {}
  57
  58
  59 Solver::~Solver()
  60 {
  61     for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
  62     for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
  63 }
  64
  65
  66 //=================================================================================================
  67 // Minor methods:
  68
  69
  70 // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
  71 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
  72 //
  73 Var Solver::newVar(bool sign, bool dvar)
  74 {
  75     int v = nVars();
  76     watches   .push();          // (list for positive literal)
  77     watches   .push();          // (list for negative literal)
  78     reason    .push(NULL);
  79     assigns   .push(toInt(l_Undef));
  80     level     .push(-1);
  81     activity  .push(0);
  82     seen      .push(0);
  83
  84     polarity    .push((char)sign);
  85     decision_var.push((char)dvar);
  86
  87     insertVarOrder(v);
  88     return v;
  89 }
  90
  91
  92 bool Solver::addClause(vec<Lit>& ps)
  93 {
  94     assert(decisionLevel() == 0);
  95
  96     if (!ok)
  97         return false;
  98     else{
  99         // Check if clause is satisfied and remove false/duplicate literals:
 100         sort(ps);
 101         Lit p; int i, j;
 102         for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
 103             if (value(ps[i]) == l_True || ps[i] == ~p)
 104                 return true;
 105             else if (value(ps[i]) != l_False && ps[i] != p)
 106                 ps[j++] = p = ps[i];
 107         ps.shrink(i - j);
 108     }
 109
 110     if (ps.size() == 0)
 111         return ok = false;
 112     else if (ps.size() == 1){
 113         assert(value(ps[0]) == l_Undef);
 114         uncheckedEnqueue(ps[0]);
 115         return ok = (propagate() == NULL);
 116     }else{
 117         Clause* c = Clause_new(ps, false);
 118         clauses.push(c);
 119         attachClause(*c);
 120     }
 121
 122     return true;
 123 }
 124
 125
 126 void Solver::attachClause(Clause& c) {
 127     assert(c.size() > 1);
 128     watches[toInt(~c[0])].push(&c);
 129     watches[toInt(~c[1])].push(&c);
 130     if (c.learnt()) learnts_literals += c.size();
 131     else            clauses_literals += c.size(); }
 132
 133
 134 void Solver::detachClause(Clause& c) {
 135     assert(c.size() > 1);
 136     assert(find(watches[toInt(~c[0])], &c));
 137     assert(find(watches[toInt(~c[1])], &c));
 138     remove(watches[toInt(~c[0])], &c);
 139     remove(watches[toInt(~c[1])], &c);
 140     if (c.learnt()) learnts_literals -= c.size();
 141     else            clauses_literals -= c.size(); }
 142
 143
 144 void Solver::removeClause(Clause& c) {
 145     detachClause(c);
 146     free(&c); }
 147
 148
 149 bool Solver::satisfied(const Clause& c) const {
 150     for (int i = 0; i < c.size(); i++)
 151         if (value(c[i]) == l_True)
 152             return true;
 153     return false; }
 154
 155
 156 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 157 //
 158 void Solver::cancelUntil(int level) {
 159     if (decisionLevel() > level){
 160         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
 161             Var     x  = var(trail[c]);
 162             assigns[x] = toInt(l_Undef);
 163             insertVarOrder(x); }
 164         qhead = trail_lim[level];
 165         trail.shrink(trail.size() - trail_lim[level]);
 166         trail_lim.shrink(trail_lim.size() - level);
 167     } }
 168
 169
 170 //=================================================================================================
 171 // Major methods:
 172
 173
 174 Lit Solver::pickBranchLit(int polarity_mode, double random_var_freq)
 175 {
 176     Var next = var_Undef;
 177
 178     // Random decision:
 179     if (drand(random_seed) < random_var_freq && !order_heap.empty()){
 180         next = order_heap[irand(random_seed,order_heap.size())];
 181         if (toLbool(assigns[next]) == l_Undef && decision_var[next])
 182             rnd_decisions++; }
 183
 184     // Activity based decision:
 185     while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next])
 186         if (order_heap.empty()){
 187             next = var_Undef;
 188             break;
 189         }else
 190             next = order_heap.removeMin();
 191
 192     bool sign = false;
 193     switch (polarity_mode){
 194     case polarity_true:  sign = false; break;
 195     case polarity_false: sign = true;  break;
 196     case polarity_user:  sign = polarity[next]; break;
 197     case polarity_rnd:   sign = irand(random_seed, 2); break;
 198     default: assert(false); }
 199
 200     return next == var_Undef ? lit_Undef : Lit(next, sign);
 201 }
 202
 203
 204 /*_________________________________________________________________________________________________
 205 |
 206 |  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
 207 |
 208 |  Description:
 209 |    Analyze conflict and produce a reason clause.
 210 |
 211 |    Pre-conditions:
 212 |      * 'out_learnt' is assumed to be cleared.
 213 |      * Current decision level must be greater than root level.
 214 |
 215 |    Post-conditions:
 216 |      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
 217 |
 218 |  Effect:
 219 |    Will undo part of the trail, upto but not beyond the assumption of the current decision level.
 220 |________________________________________________________________________________________________@*/
 221 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
 222 {
 223     int pathC = 0;
 224     Lit p     = lit_Undef;
 225
 226     // Generate conflict clause:
 227     //
 228     out_learnt.push();      // (leave room for the asserting literal)
 229     int index   = trail.size() - 1;
 230     out_btlevel = 0;
 231
 232     do{
 233         assert(confl != NULL);          // (otherwise should be UIP)
 234         Clause& c = *confl;
 235
 236         if (c.learnt())
 237             claBumpActivity(c);
 238
 239         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
 240             Lit q = c[j];
 241
 242             if (!seen[var(q)] && level[var(q)] > 0){
 243                 varBumpActivity(var(q));
 244                 seen[var(q)] = 1;
 245                 if (level[var(q)] >= decisionLevel())
 246                     pathC++;
 247                 else{
 248                     out_learnt.push(q);
 249                     if (level[var(q)] > out_btlevel)
 250                         out_btlevel = level[var(q)];
 251                 }
 252             }
 253         }
 254
 255         // Select next clause to look at:
 256         while (!seen[var(trail[index--])]);
 257         p     = trail[index+1];
 258         confl = reason[var(p)];
 259         seen[var(p)] = 0;
 260         pathC--;
 261
 262     }while (pathC > 0);
 263     out_learnt[0] = ~p;
 264
 265     // Simplify conflict clause:
 266     //
 267     int i, j;
 268     if (expensive_ccmin){
 269         uint32_t abstract_level = 0;
 270         for (i = 1; i < out_learnt.size(); i++)
 271             abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
 272
 273         out_learnt.copyTo(analyze_toclear);
 274         for (i = j = 1; i < out_learnt.size(); i++)
 275             if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level))
 276                 out_learnt[j++] = out_learnt[i];
 277     }else{
 278         out_learnt.copyTo(analyze_toclear);
 279         for (i = j = 1; i < out_learnt.size(); i++){
 280             Clause& c = *reason[var(out_learnt[i])];
 281             for (int k = 1; k < c.size(); k++)
 282                 if (!seen[var(c[k])] && level[var(c[k])] > 0){
 283                     out_learnt[j++] = out_learnt[i];
 284                     break; }
 285         }
 286     }
 287     max_literals += out_learnt.size();
 288     out_learnt.shrink(i - j);
 289     tot_literals += out_learnt.size();
 290
 291     // Find correct backtrack level:
 292     //
 293     if (out_learnt.size() == 1)
 294         out_btlevel = 0;
 295     else{
 296         int max_i = 1;
 297         for (int i = 2; i < out_learnt.size(); i++)
 298             if (level[var(out_learnt[i])] > level[var(out_learnt[max_i])])
 299                 max_i = i;
 300         Lit p             = out_learnt[max_i];
 301         out_learnt[max_i] = out_learnt[1];
 302         out_learnt[1]     = p;
 303         out_btlevel       = level[var(p)];
 304     }
 305
 306
 307     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
 308 }
 309
 310
 311 // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
 312 // visiting literals at levels that cannot be removed later.
 313 bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
 314 {
 315     analyze_stack.clear(); analyze_stack.push(p);
 316     int top = analyze_toclear.size();
 317     while (analyze_stack.size() > 0){
 318         assert(reason[var(analyze_stack.last())] != NULL);
 319         Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
 320
 321         for (int i = 1; i < c.size(); i++){
 322             Lit p  = c[i];
 323             if (!seen[var(p)] && level[var(p)] > 0){
 324                 if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
 325                     seen[var(p)] = 1;
 326                     analyze_stack.push(p);
 327                     analyze_toclear.push(p);
 328                 }else{
 329                     for (int j = top; j < analyze_toclear.size(); j++)
 330                         seen[var(analyze_toclear[j])] = 0;
 331                     analyze_toclear.shrink(analyze_toclear.size() - top);
 332                     return false;
 333                 }
 334             }
 335         }
 336     }
 337
 338     return true;
 339 }
 340
 341
 342 /*_________________________________________________________________________________________________
 343 |
 344 |  analyzeFinal : (p : Lit)  ->  [void]
 345 |
 346 |  Description:
 347 |    Specialized analysis procedure to express the final conflict in terms of assumptions.
 348 |    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
 349 |    stores the result in 'out_conflict'.
 350 |________________________________________________________________________________________________@*/
 351 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 352 {
 353     out_conflict.clear();
 354     out_conflict.push(p);
 355
 356     if (decisionLevel() == 0)
 357         return;
 358
 359     seen[var(p)] = 1;
 360
 361     for (int i = trail.size()-1; i >= trail_lim[0]; i--){
 362         Var x = var(trail[i]);
 363         if (seen[x]){
 364             if (reason[x] == NULL){
 365                 assert(level[x] > 0);
 366                 out_conflict.push(~trail[i]);
 367             }else{
 368                 Clause& c = *reason[x];
 369                 for (int j = 1; j < c.size(); j++)
 370                     if (level[var(c[j])] > 0)
 371                         seen[var(c[j])] = 1;
 372             }
 373             seen[x] = 0;
 374         }
 375     }
 376
 377     seen[var(p)] = 0;
 378 }
 379
 380
 381 void Solver::uncheckedEnqueue(Lit p, Clause* from)
 382 {
 383     assert(value(p) == l_Undef);
 384     assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
 385     level   [var(p)] = decisionLevel();
 386     reason  [var(p)] = from;
 387     trail.push(p);
 388 }
 389
 390
 391 /*_________________________________________________________________________________________________
 392 |
 393 |  propagate : [void]  ->  [Clause*]
 394 |
 395 |  Description:
 396 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
 397 |    otherwise NULL.
 398 |
 399 |    Post-conditions:
 400 |      * the propagation queue is empty, even if there was a conflict.
 401 |________________________________________________________________________________________________@*/
 402 Clause* Solver::propagate()
 403 {
 404     Clause* confl     = NULL;
 405     int     num_props = 0;
 406
 407     while (qhead < trail.size()){
 408         Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
 409         vec<Clause*>&  ws  = watches[toInt(p)];
 410         Clause         **i, **j, **end;
 411         num_props++;
 412
 413         for (i = j = (Clause**)ws, end = i + ws.size();  i != end;){
 414             Clause& c = **i++;
 415
 416             // Make sure the false literal is data[1]:
 417             Lit false_lit = ~p;
 418             if (c[0] == false_lit)
 419                 c[0] = c[1], c[1] = false_lit;
 420
 421             assert(c[1] == false_lit);
 422
 423             // If 0th watch is true, then clause is already satisfied.
 424             Lit first = c[0];
 425             if (value(first) == l_True){
 426                 *j++ = &c;
 427             }else{
 428                 // Look for new watch:
 429                 for (int k = 2; k < c.size(); k++)
 430                     if (value(c[k]) != l_False){
 431                         c[1] = c[k]; c[k] = false_lit;
 432                         watches[toInt(~c[1])].push(&c);
 433                         goto FoundWatch; }
 434
 435                 // Did not find watch -- clause is unit under assignment:
 436                 *j++ = &c;
 437                 if (value(first) == l_False){
 438                     confl = &c;
 439                     qhead = trail.size();
 440                     // Copy the remaining watches:
 441                     while (i < end)
 442                         *j++ = *i++;
 443                 }else
 444                     uncheckedEnqueue(first, &c);
 445             }
 446         FoundWatch:;
 447         }
 448         ws.shrink(i - j);
 449     }
 450     propagations += num_props;
 451     simpDB_props -= num_props;
 452
 453     return confl;
 454 }
 455
 456 /*_________________________________________________________________________________________________
 457 |
 458 |  reduceDB : ()  ->  [void]
 459 |
 460 |  Description:
 461 |    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
 462 |    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
 463 |________________________________________________________________________________________________@*/
 464 struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
 465 void Solver::reduceDB()
 466 {
 467     int     i, j;
 468     double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
 469
 470     sort(learnts, reduceDB_lt());
 471     for (i = j = 0; i < learnts.size() / 2; i++){
 472         if (learnts[i]->size() > 2 && !locked(*learnts[i]))
 473             removeClause(*learnts[i]);
 474         else
 475             learnts[j++] = learnts[i];
 476     }
 477     for (; i < learnts.size(); i++){
 478         if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
 479             removeClause(*learnts[i]);
 480         else
 481             learnts[j++] = learnts[i];
 482     }
 483     learnts.shrink(i - j);
 484 }
 485
 486
 487 void Solver::removeSatisfied(vec<Clause*>& cs)
 488 {
 489     int i,j;
 490     for (i = j = 0; i < cs.size(); i++){
 491         if (satisfied(*cs[i]))
 492             removeClause(*cs[i]);
 493         else
 494             cs[j++] = cs[i];
 495     }
 496     cs.shrink(i - j);
 497 }
 498
 499
 500 /*_________________________________________________________________________________________________
 501 |
 502 |  simplify : [void]  ->  [bool]
 503 |
 504 |  Description:
 505 |    Simplify the clause database according to the current top-level assigment. Currently, the only
 506 |    thing done here is the removal of satisfied clauses, but more things can be put here.
 507 |________________________________________________________________________________________________@*/
 508 bool Solver::simplify()
 509 {
 510     assert(decisionLevel() == 0);
 511
 512     if (!ok || propagate() != NULL)
 513         return ok = false;
 514
 515     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
 516         return true;
 517
 518     // Remove satisfied clauses:
 519     removeSatisfied(learnts);
 520     if (remove_satisfied)        // Can be turned off.
 521         removeSatisfied(clauses);
 522
 523     // Remove fixed variables from the variable heap:
 524     order_heap.filter(VarFilter(*this));
 525
 526     simpDB_assigns = nAssigns();
 527     simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)
 528
 529     return true;
 530 }
 531
 532
 533 /*_________________________________________________________________________________________________
 534 |
 535 |  search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&)  ->  [lbool]
 536 |
 537 |  Description:
 538 |    Search for a model the specified number of conflicts, keeping the number of learnt clauses
 539 |    below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
 540 |    indicate infinity.
 541 |
 542 |  Output:
 543 |    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
 544 |    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
 545 |    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
 546 |________________________________________________________________________________________________@*/
 547 lbool Solver::search(int nof_conflicts, int nof_learnts)
 548 {
 549     assert(ok);
 550     int         backtrack_level;
 551     int         conflictC = 0;
 552     vec<Lit>    learnt_clause;
 553
 554     starts++;
 555
 556     bool first = true;
 557
 558     for (;;){
 559         Clause* confl = propagate();
 560         if (confl != NULL){
 561             // CONFLICT
 562             conflicts++; conflictC++;
 563             if (decisionLevel() == 0) return l_False;
 564
 565             first = false;
 566
 567             learnt_clause.clear();
 568             analyze(confl, learnt_clause, backtrack_level);
 569             cancelUntil(backtrack_level);
 570             assert(value(learnt_clause[0]) == l_Undef);
 571
 572             if (learnt_clause.size() == 1){
 573                 uncheckedEnqueue(learnt_clause[0]);
 574             }else{
 575                 Clause* c = Clause_new(learnt_clause, true);
 576                 learnts.push(c);
 577                 attachClause(*c);
 578                 claBumpActivity(*c);
 579                 uncheckedEnqueue(learnt_clause[0], c);
 580             }
 581
 582             varDecayActivity();
 583             claDecayActivity();
 584
 585         }else{
 586             // NO CONFLICT
 587
 588             if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
 589                 // Reached bound on number of conflicts:
 590                 progress_estimate = progressEstimate();
 591                 cancelUntil(0);
 592                 return l_Undef; }
 593
 594             // Simplify the set of problem clauses:
 595             if (decisionLevel() == 0 && !simplify())
 596                 return l_False;
 597
 598             if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
 599                 // Reduce the set of learnt clauses:
 600                 reduceDB();
 601
 602             Lit next = lit_Undef;
 603             while (decisionLevel() < assumptions.size()){
 604                 // Perform user provided assumption:
 605                 Lit p = assumptions[decisionLevel()];
 606                 if (value(p) == l_True){
 607                     // Dummy decision level:
 608                     newDecisionLevel();
 609                 }else if (value(p) == l_False){
 610                     analyzeFinal(~p, conflict);
 611                     return l_False;
 612                 }else{
 613                     next = p;
 614                     break;
 615                 }
 616             }
 617
 618             if (next == lit_Undef){
 619                 // New variable decision:
 620                 decisions++;
 621                 next = pickBranchLit(polarity_mode, random_var_freq);
 622
 623                 if (next == lit_Undef)
 624                     // Model found:
 625                     return l_True;
 626             }
 627
 628             // Increase decision level and enqueue 'next'
 629             assert(value(next) == l_Undef);
 630             newDecisionLevel();
 631             uncheckedEnqueue(next);
 632         }
 633     }
 634 }
 635
 636
 637 double Solver::progressEstimate() const
 638 {
 639     double  progress = 0;
 640     double  F = 1.0 / nVars();
 641
 642     for (int i = 0; i <= decisionLevel(); i++){
 643         int beg = i == 0 ? 0 : trail_lim[i - 1];
 644         int end = i == decisionLevel() ? trail.size() : trail_lim[i];
 645         progress += pow(F, i) * (end - beg);
 646     }
 647
 648     return progress / nVars();
 649 }
 650
 651
 652 bool Solver::solve(const vec<Lit>& assumps)
 653 {
 654     model.clear();
 655     conflict.clear();
 656
 657     if (!ok) return false;
 658
 659     assumps.copyTo(assumptions);
 660
 661     double  nof_conflicts = restart_first;
 662     double  nof_learnts   = nClauses() * learntsize_factor;
 663     lbool   status        = l_Undef;
 664
 665     if (verbosity >= 1){
 666         reportf("============================[ Search Statistics ]==============================\n");
 667         reportf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
 668         reportf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
 669         reportf("===============================================================================\n");
 670     }
 671
 672     // Search:
 673     while (status == l_Undef){
 674         if (verbosity >= 1)
 675             reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout);
 676         status = search((int)nof_conflicts, (int)nof_learnts);
 677         nof_conflicts *= restart_inc;
 678         nof_learnts   *= learntsize_inc;
 679     }
 680
 681     if (verbosity >= 1)
 682         reportf("===============================================================================\n");
 683
 684
 685     if (status == l_True){
 686         // Extend & copy model:
 687         model.growTo(nVars());
 688         for (int i = 0; i < nVars(); i++) model[i] = value(i);
 689 #ifndef NDEBUG
 690         verifyModel();
 691 #endif
 692     }else{
 693         assert(status == l_False);
 694         if (conflict.size() == 0)
 695             ok = false;
 696     }
 697
 698     cancelUntil(0);
 699     return status == l_True;
 700 }
 701
 702 //=================================================================================================
 703 // Debug methods:
 704
 705
 706 void Solver::verifyModel()
 707 {
 708     bool failed = false;
 709     for (int i = 0; i < clauses.size(); i++){
 710         assert(clauses[i]->mark() == 0);
 711         Clause& c = *clauses[i];
 712         for (int j = 0; j < c.size(); j++)
 713             if (modelValue(c[j]) == l_True)
 714                 goto next;
 715
 716         reportf("unsatisfied clause: ");
 717         printClause(*clauses[i]);
 718         reportf("\n");
 719         failed = true;
 720     next:;
 721     }
 722
 723     assert(!failed);
 724
 725     reportf("Verified %d original clauses.\n", clauses.size());
 726 }
 727
 728
 729 void Solver::checkLiteralCount()
 730 {
 731     // Check that sizes are calculated correctly:
 732     int cnt = 0;
 733     for (int i = 0; i < clauses.size(); i++)
 734         if (clauses[i]->mark() == 0)
 735             cnt += clauses[i]->size();
 736
 737     if ((int)clauses_literals != cnt){
 738         fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt);
 739         assert((int)clauses_literals == cnt);
 740     }
 741 }