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