zchaff64/zchaff_solver.cpp

   1 // *********************************************************************
   2 // Copyright 2000-2004, Princeton University.  All rights reserved.
   3 // By using this software the USER indicates that he or she has read,
   4 // understood and will comply with the following:
   5 //
   6 // --- Princeton University hereby grants USER nonexclusive permission
   7 // to use, copy and/or modify this software for internal, noncommercial,
   8 // research purposes only. Any distribution, including commercial sale
   9 // or license, of this software, copies of the software, its associated
  10 // documentation and/or modifications of either is strictly prohibited
  11 // without the prior consent of Princeton University.  Title to copyright
  12 // to this software and its associated documentation shall at all times
  13 // remain with Princeton University.  Appropriate copyright notice shall
  14 // be placed on all software copies, and a complete copy of this notice
  15 // shall be included in all copies of the associated documentation.
  16 // No right is  granted to use in advertising, publicity or otherwise
  17 // any trademark, service mark, or the name of Princeton University.
  18 //
  19 //
  20 // --- This software and any associated documentation is provided "as is"
  21 //
  22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 // PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 // Princeton University shall not be liable under any circumstances for
  29 // any direct, indirect, special, incidental, or consequential damages
  30 // with respect to any claim by USER or any third party on account of
  31 // or arising from the use, or inability to use, this software or its
  32 // associated documentation, even if Princeton University has been advised
  33 // of the possibility of those damages.
  34 // ********************************************************************
  35
  36 #include <iostream>
  37 #include <algorithm>
  38 #include <fstream>
  39 #include <vector>
  40 #include <map>
  41 #include <set>
  42 #include <queue>
  43
  44 using namespace std;
  45
  46 #include "zchaff_solver.h"
  47
  48 // #define VERIFY_ON
  49
  50 #ifdef VERIFY_ON
  51 ofstream verify_out("resolve_trace");
  52 #endif
  53
  54 void CSolver::re_init_stats(void) {
  55   _stats.is_mem_out           = false;
  56   _stats.outcome              = UNDETERMINED;
  57   _stats.next_restart         = _params.restart.first_restart;
  58   _stats.restart_incr         = _params.restart.backtrack_incr;
  59   _stats.next_cls_deletion    = _params.cls_deletion.interval;
  60   _stats.next_var_score_decay = _params.decision.decay_period;
  61   _stats.current_randomness   = _params.decision.base_randomness;
  62
  63   _stats.total_bubble_move            = 0;
  64   _stats.num_decisions                = 0;
  65   _stats.num_decisions_stack_conf     = 0;
  66   _stats.num_decisions_vsids          = 0;
  67   _stats.num_decisions_shrinking      = 0;
  68   _stats.num_backtracks               = 0;
  69   _stats.max_dlevel                   = 0;
  70   _stats.num_implications             = 0;
  71   _stats.num_restarts                 = 0;
  72   _stats.num_del_orig_cls             = 0;
  73   _stats.num_shrinkings               = 0;
  74   _stats.start_cpu_time               = get_cpu_time();
  75   _stats.finish_cpu_time              = 0;
  76   _stats.random_seed                  = 0;
  77 }
  78
  79 void CSolver::init_stats(void) {
  80   re_init_stats();
  81
  82   _stats.been_reset                   = true;
  83   _stats.num_free_variables           = 0;
  84   _stats.num_free_branch_vars         = 0;
  85 }
  86
  87 void CSolver::init_parameters(void) {
  88   _params.verbosity                           = 0;
  89   _params.time_limit                          = 3600 * 24;  // a day
  90   _params.shrinking.size                      = 95;
  91   _params.shrinking.enable                    = true;
  92   _params.shrinking.upper_bound               = 800;
  93   _params.shrinking.lower_bound               = 600;
  94   _params.shrinking.upper_delta               = -5;
  95   _params.shrinking.lower_delta               = 10;
  96   _params.shrinking.window_width              = 20;
  97   _params.shrinking.bound_update_frequency    = 20;
  98
  99   _params.decision.base_randomness            = 0;
 100   _params.decision.decay_period               = 40;
 101   _params.decision.bubble_init_step           = 0x400;
 102
 103   _params.cls_deletion.enable                 = true ;
 104   _params.cls_deletion.head_activity          = 500;
 105   _params.cls_deletion.tail_activity          = 10;
 106   _params.cls_deletion.head_num_lits          = 6;
 107   _params.cls_deletion.tail_num_lits          = 45;
 108   _params.cls_deletion.tail_vs_head           = 16;
 109   _params.cls_deletion.interval               = 600;
 110
 111   _params.restart.enable                      = true;
 112   _params.restart.interval                    = 700;
 113   _params.restart.first_restart               = 7000;
 114   _params.restart.backtrack_incr              = 700;
 115 }
 116
 117 CSolver::CSolver(void) {
 118   init_parameters();
 119   init_stats();
 120   _dlevel                       = 0;
 121   _force_terminate              = false;
 122   _implication_id               = 0;
 123   _num_marked                   = 0;
 124   _num_in_new_cl                = 0;
 125   _outside_constraint_hook      = NULL;
 126   _sat_hook                     = NULL;
 127 }
 128
 129 CSolver::~CSolver(void) {
 130   while (!_assignment_stack.empty()) {
 131     delete _assignment_stack.back();
 132     _assignment_stack.pop_back();
 133   }
 134 }
 135
 136 void CSolver::set_time_limit(float t) {
 137   _params.time_limit = t;
 138 }
 139
 140 float CSolver::elapsed_cpu_time(void) {
 141   return get_cpu_time() - _stats.start_cpu_time;
 142 }
 143
 144 float CSolver::cpu_run_time(void) {
 145   return (_stats.finish_cpu_time - _stats.start_cpu_time);
 146 }
 147
 148 void CSolver::set_variable_number(int n) {
 149   assert(num_variables() == 0);
 150   CDatabase::set_variable_number(n);
 151   _stats.num_free_variables = num_variables();
 152   while (_assignment_stack.size() <= num_variables())
 153     _assignment_stack.push_back(new vector<int>);
 154   assert(_assignment_stack.size() == num_variables() + 1);
 155 }
 156
 157 int CSolver::add_variable(void) {
 158   int num = CDatabase::add_variable();
 159   ++_stats.num_free_variables;
 160   while (_assignment_stack.size() <= num_variables())
 161     _assignment_stack.push_back(new vector<int>);
 162   assert(_assignment_stack.size() == num_variables() + 1);
 163   return num;
 164 }
 165
 166 void CSolver::set_mem_limit(int s) {
 167   CDatabase::set_mem_limit(s);
 168 }
 169
 170 void CSolver::set_randomness(int n) {
 171   _params.decision.base_randomness = n;
 172 }
 173
 174 void CSolver::set_random_seed(int seed) {
 175   srand(seed);
 176 }
 177
 178 void CSolver::enable_cls_deletion(bool allow) {
 179   _params.cls_deletion.enable = allow;
 180 }
 181
 182 void CSolver::add_hook(HookFunPtrT fun, int interval) {
 183   pair<HookFunPtrT, int> a(fun, interval);
 184   _hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a));
 185 }
 186
 187 void CSolver::run_periodic_functions(void) {
 188   // a. restart
 189   if (_params.restart.enable && _stats.num_backtracks > _stats.next_restart &&
 190       _shrinking_cls.empty()) {
 191     _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
 192     delete_unrelevant_clauses();
 193     restart();
 194     if (_stats.num_restarts % 5 == 1)
 195       compact_lit_pool();
 196     cout << "\rDecision: " << _assignment_stack[0]->size() << "/"
 197          <<num_variables() << "\tTime: " << get_cpu_time() -
 198            _stats.start_cpu_time << "/" << _params.time_limit << flush;
 199   }
 200
 201   // b. decay variable score
 202   if (_stats.num_backtracks > _stats.next_var_score_decay) {
 203     _stats.next_var_score_decay = _stats.num_backtracks +
 204                                   _params.decision.decay_period;
 205     decay_variable_score();
 206   }
 207
 208   // c. run hook functions
 209   for (unsigned i = 0; i< _hooks.size(); ++i) {
 210     pair<int, pair<HookFunPtrT, int> > & hook = _hooks[i];
 211     if (_stats.num_decisions >= hook.first) {
 212       hook.first += hook.second.second;
 213       hook.second.first((void *) this);
 214     }
 215   }
 216 }
 217
 218 void CSolver::init_solve(void) {
 219   CDatabase::init_stats();
 220   re_init_stats();
 221   _stats.been_reset = false;
 222
 223   assert(_conflicts.empty());
 224   assert(_conflict_lits.empty());
 225   assert(_num_marked == 0);
 226   assert(_num_in_new_cl == 0);
 227   assert(_dlevel == 0);
 228
 229   for (unsigned i = 0, sz = variables()->size(); i < sz; ++i) {
 230     variable(i).score(0) = variable(i).lits_count(0);
 231     variable(i).score(1) = variable(i).lits_count(1);
 232   }
 233
 234   _ordered_vars.resize(num_variables());
 235   update_var_score();
 236
 237   set_random_seed(_stats.random_seed);
 238
 239   top_unsat_cls = clauses()->size() - 1;
 240
 241   _stats.shrinking_benefit = 0;
 242   _shrinking_cls.clear();
 243   _stats.shrinking_cls_length = 0;
 244 }
 245
 246 void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl) {
 247     assert(value == 0 || value == 1);
 248     CVariable & var = variable(v);
 249     assert(var.value() == UNKNOWN);
 250     assert(dl == dlevel());
 251
 252     var.set_dlevel(dl);
 253     var.set_value(value);
 254     var.antecedent() = ante;
 255     var.assgn_stack_pos() = _assignment_stack[dl]->size();
 256     _assignment_stack[dl]->push_back(v * 2 + !value);
 257     set_var_value_BCP(v, value);
 258
 259     ++_stats.num_implications ;
 260     if (var.is_branchable())
 261         --num_free_variables();
 262 }
 263
 264 void CSolver::set_var_value_BCP(int v, int value) {
 265   vector<CLitPoolElement *> & watchs = variable(v).watched(value);
 266   for (vector <CLitPoolElement *>::iterator itr = watchs.begin();
 267        itr != watchs.end(); ++itr) {
 268     ClauseIdx cl_idx;
 269     CLitPoolElement * other_watched = *itr;
 270     CLitPoolElement * watched = *itr;
 271     int dir = watched->direction();
 272     CLitPoolElement * ptr = watched;
 273     while (true) {
 274       ptr += dir;
 275       if (ptr->val() <= 0) {  // reached one end of the clause
 276         if (dir == 1)  // reached the right end, i.e. spacing element is cl_id
 277           cl_idx = ptr->get_clause_index();
 278         if (dir == watched->direction()) {  // we haven't go both directions.
 279           ptr = watched;
 280           dir = -dir;                     // change direction, go the other way
 281           continue;
 282         }
 283         // otherwise, we have already go through the whole clause
 284         int the_value = literal_value(*other_watched);
 285         if (the_value == 0)  // a conflict
 286           _conflicts.push_back(cl_idx);
 287         else if (the_value != 1)  // i.e. unknown
 288           queue_implication(other_watched->s_var(), cl_idx);
 289         break;
 290       }
 291       if (ptr->is_watched()) {  // literal is the other watched lit, skip it.
 292         other_watched = ptr;
 293         continue;
 294       }
 295       if (literal_value(*ptr) == 0)  // literal value is 0, keep going
 296         continue;
 297       // now the literal's value is either 1 or unknown, watch it instead
 298       int v1 = ptr->var_index();
 299       int sign = ptr->var_sign();
 300       variable(v1).watched(sign).push_back(ptr);
 301       ptr->set_watch(dir);
 302       // remove the original watched literal from watched list
 303       watched->unwatch();
 304       *itr = watchs.back();  // copy the last element in it's place
 305       watchs.pop_back();     // remove the last element
 306       --itr;                 // do this so with don't skip one during traversal
 307       break;
 308     }
 309   }
 310 }
 311
 312 void CSolver::unset_var_value(int v) {
 313   if (v == 0)
 314     return;
 315   CVariable & var = variable(v);
 316   var.set_value(UNKNOWN);
 317   var.set_antecedent(NULL_CLAUSE);
 318   var.set_dlevel(-1);
 319   var.assgn_stack_pos() = -1;
 320
 321   if (var.is_branchable()) {
 322     ++num_free_variables();
 323     if (var.var_score_pos() < _max_score_pos)
 324       _max_score_pos = var.var_score_pos();
 325   }
 326 }
 327
 328 void CSolver::dump_assignment_stack(ostream & os ) {
 329   os << "Assignment Stack:  ";
 330   for (int i = 0; i <= dlevel(); ++i) {
 331     os << "(" <<i << ":";
 332     for (unsigned j = 0; j < (*_assignment_stack[i]).size(); ++j) {
 333       os << ((*_assignment_stack[i])[j]&0x1?"-":"+")
 334          << ((*_assignment_stack[i])[j] >> 1) << " ";
 335     }
 336     os << ") " << endl;
 337   }
 338   os << endl;
 339 }
 340
 341 void CSolver::dump_implication_queue(ostream & os) {
 342   _implication_queue.dump(os);
 343 }
 344
 345 void CSolver::delete_clause_group(int gid) {
 346   assert(is_gid_allocated(gid));
 347
 348   if (_stats.been_reset == false)
 349     reset();  // if delete some clause, then implication queue are invalidated
 350
 351   for (vector<CClause>::iterator itr = clauses()->begin();
 352        itr != clauses()->end(); ++itr) {
 353     CClause & cl = *itr;
 354     if (cl.status() != DELETED_CL) {
 355       if (cl.gid(gid) == true) {
 356         mark_clause_deleted(cl);
 357       }
 358     }
 359   }
 360
 361   // delete the index from variables
 362   for (vector<CVariable>::iterator itr = variables()->begin();
 363          itr != variables()->end(); ++itr) {
 364     for (unsigned i = 0; i < 2; ++i) {  // for each phase
 365       // delete the lit index from the vars
 366 #ifdef KEEP_LIT_CLAUSES
 367       vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);
 368       for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();
 369            itr1 != lit_clauses.end(); ++itr1) {
 370         if (clause(*itr1).status() == DELETED_CL) {
 371           *itr1 = lit_clauses.back();
 372           lit_clauses.pop_back();
 373           --itr1;
 374         }
 375       }
 376 #endif
 377       // delete the watched index from the vars
 378       vector<CLitPoolElement *> & watched = (*itr).watched(i);
 379       for (vector<CLitPoolElement *>::iterator itr1 = watched.begin();
 380            itr1 != watched.end(); ++itr1) {
 381         if ((*itr1)->val() <= 0) {
 382           *itr1 = watched.back();
 383           watched.pop_back();
 384           --itr1;
 385         }
 386       }
 387     }
 388   }
 389   free_gid(gid);
 390 }
 391
 392 void CSolver::reset(void) {
 393   if (_stats.been_reset)
 394     return;
 395   if (num_variables() == 0)
 396     return;
 397   back_track(0);
 398   _conflicts.clear();
 399   while (!_implication_queue.empty())
 400     _implication_queue.pop();
 401
 402   _stats.outcome = UNDETERMINED;
 403   _stats.been_reset = true;
 404 }
 405
 406 void CSolver::delete_unrelevant_clauses(void) {
 407   unsigned original_del_cls = num_deleted_clauses();
 408   int num_conf_cls = num_clauses() - init_num_clauses() + num_del_orig_cls();
 409   int head_count = num_conf_cls / _params.cls_deletion.tail_vs_head;
 410   int count = 0;
 411   for (vector<CClause>::iterator itr = clauses()->begin();
 412                                  itr != clauses()->end() - 1; ++itr) {
 413     CClause & cl = *itr;
 414     if (cl.status() != CONFLICT_CL) {
 415       continue;
 416     }
 417     bool cls_sat_at_dl_0 = false;
 418     for (int i = 0, sz = cl.num_lits(); i < sz; ++i) {
 419       if (literal_value(cl.literal(i)) == 1 &&
 420           variable(cl.literal(i).var_index()).dlevel() == 0) {
 421         cls_sat_at_dl_0 = true;
 422         break;
 423       }
 424     }
 425     if (cls_sat_at_dl_0) {
 426       int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
 427       for (unsigned i = 0; i < cl.num_lits(); ++i) {
 428         int lit_value = literal_value(cl.literal(i));
 429         if (lit_value == 0)
 430           ++val_0_lits;
 431         if (lit_value == 1)
 432           ++val_1_lits;
 433         if (lit_value == UNKNOWN)
 434           ++unknown_lits;
 435         if (unknown_lits + val_1_lits > 1) {
 436           mark_clause_deleted(cl);
 437           break;
 438         }
 439       }
 440       continue;
 441     }
 442
 443     count++;
 444     int max_activity = _params.cls_deletion.head_activity -
 445                        (_params.cls_deletion.head_activity -
 446                         _params.cls_deletion.tail_activity) *
 447                        count/num_conf_cls;
 448     int max_conf_cls_size;
 449
 450     if (head_count > 0) {
 451       max_conf_cls_size = _params.cls_deletion.head_num_lits;
 452       --head_count;
 453     } else {
 454       max_conf_cls_size = _params.cls_deletion.tail_num_lits;
 455     }
 456
 457     if (cl.activity() > max_activity)
 458       continue;
 459
 460     int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0, lit_value;
 461     for (unsigned i = 0; i < cl.num_lits(); ++i) {
 462       lit_value = literal_value(cl.literal(i));
 463       if (lit_value == 0)
 464         ++val_0_lits;
 465       else if (lit_value == 1)
 466         ++val_1_lits;
 467       else
 468         ++unknown_lits;
 469       if ((unknown_lits > max_conf_cls_size)) {
 470         mark_clause_deleted(cl);
 471         break;
 472       }
 473     }
 474   }
 475
 476   // if none were recently marked for deletion...
 477   if (original_del_cls == num_deleted_clauses())
 478     return;
 479
 480   // delete the index from variables
 481   for (vector<CVariable>::iterator itr = variables()->begin();
 482        itr != variables()->end(); ++itr) {
 483     for (unsigned i = 0; i < 2; ++i) {  // for each phase
 484       // delete the lit index from the vars
 485 #ifdef KEEP_LIT_CLAUSES
 486       vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);
 487       for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();
 488            itr1 != lit_clauses.end(); ++itr1) {
 489         if (clause(*itr1).status() == DELETED_CL) {
 490           *itr1 = lit_clauses.back();
 491           lit_clauses.pop_back();
 492           --itr1;
 493         }
 494       }
 495 #endif
 496       // delete the watched index from the vars
 497       vector<CLitPoolElement *> & watched = (*itr).watched(i);
 498       for (vector<CLitPoolElement *>::iterator itr1 = watched.begin();
 499            itr1 != watched.end(); ++itr1) {
 500         if ((*itr1)->val() <= 0) {
 501           *itr1 = watched.back();
 502           watched.pop_back();
 503           --itr1;
 504         }
 505       }
 506     }
 507   }
 508
 509   for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
 510     if (variable(i).dlevel() != 0) {
 511       variable(i).score(0) = variable(i).lits_count(0);
 512       variable(i).score(1) = variable(i).lits_count(1);
 513       if (variable(i).lits_count(0) == 0 && variable(i).value() == UNKNOWN) {
 514         queue_implication(i * 2 + 1, NULL_CLAUSE);
 515       }
 516       else if (variable(i).lits_count(1) == 0 &&
 517                variable(i).value() == UNKNOWN) {
 518         queue_implication(i * 2, NULL_CLAUSE);
 519       }
 520     } else {
 521       variable(i).score(0) = 0;
 522       variable(i).score(1) = 0;
 523     }
 524   }
 525   update_var_score();
 526 }
 527
 528 bool CSolver::time_out(void) {
 529   return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit);
 530 }
 531
 532 void CSolver::adjust_variable_order(int * lits, int n_lits) {
 533   // note lits are signed vars, not CLitPoolElements
 534   for (int i = 0; i < n_lits; ++i) {
 535     int var_idx = lits[i] >> 1;
 536     CVariable & var = variable(var_idx);
 537     assert(var.value() != UNKNOWN);
 538     int orig_score = var.score();
 539     ++variable(var_idx).score(lits[i] & 0x1);
 540     int new_score = var.score();
 541     if (orig_score == new_score)
 542       continue;
 543     int pos = var.var_score_pos();
 544     int orig_pos = pos;
 545     assert(_ordered_vars[pos].first == & var);
 546     assert(_ordered_vars[pos].second == orig_score);
 547     int bubble_step = _params.decision.bubble_init_step;
 548     for (pos = orig_pos ; pos >= 0; pos -= bubble_step) {
 549       if (_ordered_vars[pos].second >= new_score)
 550         break;
 551     }
 552     pos += bubble_step;
 553     for (bubble_step = bubble_step >> 1; bubble_step > 0;
 554          bubble_step = bubble_step >> 1) {
 555       if (pos - bubble_step >= 0 &&
 556           _ordered_vars[pos - bubble_step].second < new_score)
 557         pos -= bubble_step;
 558     }
 559     // now found the position, do a swap
 560     _ordered_vars[orig_pos] = _ordered_vars[pos];
 561     _ordered_vars[orig_pos].first->set_var_score_pos(orig_pos);
 562     _ordered_vars[pos].first = & var;
 563     _ordered_vars[pos].second = new_score;
 564     _ordered_vars[pos].first->set_var_score_pos(pos);
 565     _stats.total_bubble_move += orig_pos - pos;
 566   }
 567 }
 568
 569 void CSolver::decay_variable_score(void) {
 570   unsigned i, sz;
 571   for (i = 1, sz = variables()->size(); i < sz; ++i) {
 572     CVariable & var = variable(i);
 573     var.score(0) /= 2;
 574     var.score(1) /= 2;
 575   }
 576   for (i = 0, sz = _ordered_vars.size(); i < sz; ++i) {
 577     _ordered_vars[i].second = _ordered_vars[i].first->score();
 578   }
 579 }
 580
 581 bool CSolver::decide_next_branch(void) {
 582   if (dlevel() > 0)
 583     assert(_assignment_stack[dlevel()]->size() > 0);
 584   if (!_implication_queue.empty()) {
 585     // some hook function did a decision, so skip my own decision making.
 586     // if the front of implication queue is 0, that means it's finished
 587     // because var index start from 1, so 2 *vid + sign won't be 0.
 588     // else it's a valid decision.
 589     return (_implication_queue.front().lit != 0);
 590   }
 591   int s_var = 0;
 592   if (_params.shrinking.enable) {
 593     while (!_shrinking_cls.empty()) {
 594       s_var = _shrinking_cls.begin()->second;
 595       _shrinking_cls.erase(_shrinking_cls.begin());
 596       if (variable(s_var >> 1).value() == UNKNOWN) {
 597         _stats.num_decisions++;
 598         _stats.num_decisions_shrinking++;
 599         ++dlevel();
 600         queue_implication(s_var ^ 0x1, NULL_CLAUSE);
 601         return true;
 602       }
 603     }
 604   }
 605
 606   if (_outside_constraint_hook != NULL)
 607      _outside_constraint_hook(this);
 608
 609   if (!_implication_queue.empty())
 610      return (_implication_queue.front().lit != 0);
 611
 612   ++_stats.num_decisions;
 613   if (num_free_variables() == 0)  // no more free vars
 614      return false;
 615
 616   bool cls_sat = true;
 617   int i, sz, var_idx, score, max_score = -1;
 618
 619   for (; clause(top_unsat_cls).status() != ORIGINAL_CL; --top_unsat_cls) {
 620     CClause &cl=clause(top_unsat_cls);
 621     if (cl.status() != CONFLICT_CL)
 622       continue;
 623     cls_sat = false;
 624     if (cl.sat_lit_idx() < (int)cl.num_lits() &&
 625         literal_value(cl.literal(cl.sat_lit_idx())) == 1)
 626       cls_sat = true;
 627     if (!cls_sat) {
 628       max_score = -1;
 629       for (i = 0, sz = cl.num_lits(); i < sz; ++i) {
 630         var_idx = cl.literal(i).var_index();
 631         if (literal_value(cl.literal(i)) == 1) {
 632           cls_sat = true;
 633           cl.sat_lit_idx() = i;
 634           break;
 635         }
 636         else if (variable(var_idx).value() == UNKNOWN) {
 637           score = variable(var_idx).score();
 638           if (score > max_score) {
 639             max_score = score;
 640             s_var = var_idx * 2;
 641           }
 642         }
 643       }
 644     }
 645     if (!cls_sat)
 646       break;
 647   }
 648   if (!cls_sat && max_score != -1) {
 649     ++dlevel();
 650     if (dlevel() > _stats.max_dlevel)
 651       _stats.max_dlevel = dlevel();
 652     CVariable& v = variable(s_var >> 1);
 653     if (v.score(0) < v.score(1))
 654       s_var += 1;
 655     else if (v.score(0) == v.score(1)) {
 656       if (v.two_lits_count(0) > v.two_lits_count(1))
 657         s_var+=1;
 658       else if (v.two_lits_count(0) == v.two_lits_count(1))
 659         s_var+=rand()%2;
 660     }
 661     assert(s_var >= 2);
 662     queue_implication(s_var, NULL_CLAUSE);
 663     ++_stats.num_decisions_stack_conf;
 664     return true;
 665   }
 666
 667   for (unsigned i = _max_score_pos; i < _ordered_vars.size(); ++i) {
 668     CVariable & var = *_ordered_vars[i].first;
 669     if (var.value() == UNKNOWN && var.is_branchable()) {
 670       // move th max score position pointer
 671       _max_score_pos = i;
 672       // make some randomness happen
 673       if (--_stats.current_randomness < _params.decision.base_randomness)
 674         _stats.current_randomness = _params.decision.base_randomness;
 675       int randomness = _stats.current_randomness;
 676       if (randomness >= num_free_variables())
 677         randomness = num_free_variables() - 1;
 678       int skip = rand() % (1 + randomness);
 679       int index = i;
 680       while (skip > 0) {
 681         ++index;
 682       if (_ordered_vars[index].first->value() == UNKNOWN &&
 683           _ordered_vars[index].first->is_branchable())
 684         --skip;
 685       }
 686       CVariable * ptr = _ordered_vars[index].first;
 687       assert(ptr->value() == UNKNOWN && ptr->is_branchable());
 688       int sign = 0;
 689       if (ptr->score(0) < ptr->score(1))
 690         sign += 1;
 691       else if (ptr->score(0) == ptr->score(1)) {
 692         if (ptr->two_lits_count(0) > ptr->two_lits_count(1))
 693           sign += 1;
 694         else if (ptr->two_lits_count(0) == ptr->two_lits_count(1))
 695           sign += rand() % 2;
 696       }
 697       int var_idx = ptr - &(*variables()->begin());
 698       s_var = var_idx + var_idx + sign;
 699       break;
 700     }
 701   }
 702   assert(s_var >= 2);  // there must be a free var somewhere
 703   ++dlevel();
 704   if (dlevel() > _stats.max_dlevel)
 705     _stats.max_dlevel = dlevel();
 706   ++_stats.num_decisions_vsids;
 707   _implication_id = 0;
 708   queue_implication(s_var, NULL_CLAUSE);
 709   return true;
 710 }
 711
 712 int CSolver::preprocess(void) {
 713   assert(dlevel() == 0);
 714
 715   // 1. detect all the unused variables
 716   vector<int> un_used;
 717   for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
 718     CVariable & v = variable(i);
 719     if (v.lits_count(0) == 0 && v.lits_count(1) == 0) {
 720       un_used.push_back(i);
 721       queue_implication(i+i, NULL_CLAUSE);
 722       int r = deduce();
 723       assert(r == NO_CONFLICT);
 724     }
 725   }
 726   if (_params.verbosity > 1 && un_used.size() > 0) {
 727     cout << un_used.size() << " Variables are defined but not used " << endl;
 728     if (_params.verbosity > 2) {
 729       for (unsigned i = 0; i< un_used.size(); ++i)
 730          cout << un_used[i] << " ";
 731       cout << endl;
 732     }
 733   }
 734
 735   // 2. detect all variables with only one phase occuring (i.e. pure literals)
 736   vector<int> uni_phased;
 737   for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
 738     CVariable & v = variable(i);
 739     if (v.value() != UNKNOWN)
 740       continue;
 741     if (v.lits_count(0) == 0) {  // no positive phased lits.
 742       queue_implication(i+i+1, NULL_CLAUSE);
 743       uni_phased.push_back(-i);
 744     }
 745     else if (v.lits_count(1) == 0) {  // no negative phased lits.
 746       queue_implication(i+i, NULL_CLAUSE);
 747       uni_phased.push_back(i);
 748     }
 749   }
 750   if (_params.verbosity > 1 && uni_phased.size() > 0) {
 751     cout << uni_phased.size() << " Variables only appear in one phase." <<endl;
 752     if (_params.verbosity > 2) {
 753       for (unsigned i = 0; i< uni_phased.size(); ++i)
 754         cout << uni_phased[i] << " ";
 755       cout <<endl;
 756     }
 757   }
 758
 759   // 3. Unit clauses
 760   for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) {
 761     if (clause(i).status() != DELETED_CL &&
 762         clause(i).num_lits() == 1 &&
 763         variable(clause(i).literal(0).var_index()).value() == UNKNOWN)
 764       queue_implication(clause(i).literal(0).s_var(), i);
 765   }
 766
 767   if (deduce() == CONFLICT) {
 768     cout << " CONFLICT during preprocess " <<endl;
 769 #ifdef VERIFY_ON
 770     for (unsigned i = 1; i < variables()->size(); ++i) {
 771       if (variable(i).value() != UNKNOWN) {
 772         assert(variable(i).dlevel() <= 0);
 773         int ante = variable(i).antecedent();
 774         int ante_id = 0;
 775         if (ante >= 0) {
 776           ante_id = clause(ante).id();
 777           verify_out << "VAR: " << i
 778                      << " L: " << variable(i).assgn_stack_pos()
 779                      << " V: " << variable(i).value()
 780                      << " A: " << ante_id
 781                      << " Lits:";
 782           for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
 783             verify_out <<" " <<  clause(ante).literal(j).s_var();
 784           verify_out << endl;
 785          }
 786        }
 787     }
 788     verify_out << "CONF: " << clause(_conflicts[0]).id() << " ==";
 789     for (unsigned i = 0; i < clause(_conflicts[0]).num_lits(); ++i) {
 790       int svar = clause(_conflicts[0]).literal(i).s_var();
 791       verify_out << " " << svar;
 792     }
 793     verify_out << endl;
 794 #endif
 795     return CONFLICT;
 796   }
 797   if (_params.verbosity > 1) {
 798     cout << _assignment_stack[0]->size() << " vars set during preprocess; "
 799          << endl;
 800   }
 801   return NO_CONFLICT;
 802 }
 803
 804 void CSolver::mark_var_unbranchable(int vid) {
 805   if (variable(vid).is_branchable()) {
 806     variable(vid).disable_branch();
 807     if (variable(vid).value() == UNKNOWN)
 808       --num_free_variables();
 809   }
 810 }
 811
 812 void CSolver::mark_var_branchable(int vid) {
 813   CVariable & var = variable(vid);
 814   if (!var.is_branchable()) {
 815     var.enable_branch();
 816     if (var.value() == UNKNOWN) {
 817       ++num_free_variables();
 818       if (var.var_score_pos() < _max_score_pos)
 819         _max_score_pos = var.var_score_pos();
 820     }
 821   }
 822 }
 823
 824 ClauseIdx CSolver::add_orig_clause(int * lits, int n_lits, int gid) {
 825   int cid = add_clause_with_gid(lits, n_lits, gid);
 826   if (cid >= 0) {
 827     clause(cid).set_status(ORIGINAL_CL);
 828     clause(cid).activity() = 0;
 829   }
 830   return cid;
 831 }
 832
 833 ClauseIdx CSolver::add_clause_with_gid(int * lits, int n_lits, int gid) {
 834   unsigned gflag;
 835   if (gid == PERMANENT_GID )
 836     gflag = 0;
 837   else if (gid == VOLATILE_GID) {
 838     gflag = (~0x0);
 839   } else {
 840     assert(gid <= WORD_WIDTH && gid > 0);
 841     gflag = (1 << (gid- 1));
 842   }
 843   ClauseIdx cid = add_clause(lits, n_lits, gflag);
 844   if (cid < 0) {
 845     _stats.is_mem_out = true;
 846     _stats.outcome = MEM_OUT;
 847   }
 848   return cid;
 849 }
 850
 851 ClauseIdx CSolver::add_conflict_clause(int * lits, int n_lits, int gflag) {
 852   ClauseIdx cid = add_clause(lits, n_lits, gflag);
 853   if (cid >= 0) {
 854     clause(cid).set_status(CONFLICT_CL);
 855     clause(cid).activity() = 0;
 856   } else {
 857     _stats.is_mem_out = true;
 858     _stats.outcome = MEM_OUT;
 859   }
 860   return cid;
 861 }
 862
 863 void CSolver::real_solve(void) {
 864   while (_stats.outcome == UNDETERMINED) {
 865     run_periodic_functions();
 866     if (decide_next_branch()) {
 867       while (deduce() == CONFLICT) {
 868         int blevel;
 869         blevel = analyze_conflicts();
 870         if (blevel < 0) {
 871           _stats.outcome = UNSATISFIABLE;
 872           return;
 873         }
 874       }
 875     } else {
 876       if (_sat_hook != NULL && _sat_hook(this))
 877         continue;
 878       _stats.outcome = SATISFIABLE;
 879       return;
 880     }
 881     if (time_out()) {
 882       _stats.outcome = TIME_OUT;
 883       return;
 884     }
 885     if (_force_terminate) {
 886       _stats.outcome = ABORTED;
 887       return;
 888     }
 889     if (_stats.is_mem_out) {
 890       _stats.outcome = MEM_OUT;
 891        return;
 892     }
 893   }
 894 }
 895
 896 int CSolver::solve(void) {
 897   if (_stats.outcome == UNDETERMINED) {
 898     init_solve();
 899
 900     if (preprocess() == CONFLICT)
 901       _stats.outcome = UNSATISFIABLE;
 902     else  // the real search
 903       real_solve();
 904     cout << endl;
 905     _stats.finish_cpu_time = get_cpu_time();
 906   }
 907   return _stats.outcome;
 908 }
 909
 910 void CSolver::back_track(int blevel) {
 911   assert(blevel <= dlevel());
 912   for (int i = dlevel(); i >= blevel; --i) {
 913     vector<int> & assignments = *_assignment_stack[i];
 914     for (int j = assignments.size() - 1 ; j >= 0; --j)
 915       unset_var_value(assignments[j]>>1);
 916     assignments.clear();
 917   }
 918   dlevel() = blevel - 1;
 919   if (dlevel() < 0 )
 920     dlevel() = 0;
 921   ++_stats.num_backtracks;
 922 }
 923
 924 int CSolver::deduce(void) {
 925   while (!_implication_queue.empty()) {
 926     const CImplication & imp = _implication_queue.front();
 927     int lit = imp.lit;
 928     int vid = lit>>1;
 929     ClauseIdx cl = imp.antecedent;
 930     _implication_queue.pop();
 931     CVariable & var = variable(vid);
 932     if (var.value() == UNKNOWN) {  // an implication
 933       set_var_value(vid, !(lit & 0x1), cl, dlevel());
 934     }
 935     else if (var.value() == (unsigned)(lit & 0x1)) {
 936       // a conflict
 937       // note: literal & 0x1 == 1 means the literal is in negative phase
 938       // when a conflict occure at not current dlevel, we need to backtrack
 939       // to resolve the problem.
 940       // conflict analysis will only work if the conflict occure at
 941       // the top level (current dlevel)
 942       _conflicts.push_back(cl);
 943       break;
 944     } else {
 945       // so the variable have been assigned before
 946       // update its antecedent with a shorter one
 947       if (var.antecedent() != NULL_CLAUSE &&
 948           clause(cl).num_lits() < clause(var.antecedent()).num_lits())
 949         var.antecedent() = cl;
 950       assert(var.dlevel() <= dlevel());
 951     }
 952   }
 953   // if loop exited because of a conflict, we need to clean implication queue
 954   while (!_implication_queue.empty())
 955     _implication_queue.pop();
 956   return (_conflicts.size() ? CONFLICT : NO_CONFLICT);
 957 }
 958
 959 void CSolver::verify_integrity(void) {
 960   for (unsigned i = 1; i < variables()->size(); ++i) {
 961     if (variable(i).value() != UNKNOWN) {
 962       int pos = variable(i).assgn_stack_pos();
 963       int value = variable(i).value();
 964       int dlevel = variable(i).dlevel();
 965       assert((*_assignment_stack[dlevel])[pos] == (int) (i+i+1-value));
 966     }
 967   }
 968   for (unsigned i = 0; i < clauses()->size(); ++i) {
 969     if (clause(i).status() == DELETED_CL)
 970       continue;
 971     CClause & cl = clause(i);
 972     int num_0 = 0;
 973     int num_1 = 0;
 974     int num_unknown = 0;
 975     int watched[2];
 976     int watch_index = 0;
 977     watched[1] = watched[0] = 0;
 978     for (unsigned j = 0; j < cl.num_lits(); ++j) {
 979       CLitPoolElement lit = cl.literal(j);
 980       int vid = lit.var_index();
 981       if (variable(vid).value() == UNKNOWN) {
 982         ++num_unknown;
 983       } else {
 984         if (literal_value(lit) == 0)
 985           ++num_0;
 986         else
 987           ++num_1;
 988       }
 989       if (lit.is_watched()) {
 990         watched[watch_index] = lit.s_var();
 991         ++watch_index;
 992       }
 993     }
 994     if (watch_index == 0) {
 995       assert(cl.num_lits() == 1);
 996       continue;
 997     }
 998     assert(watch_index == 2);
 999     for (unsigned j = 0; j < cl.num_lits(); ++j) {
1000       CLitPoolElement lit = cl.literal(j);
1001       int vid1 = (watched[0]>>1);
1002       if (variable(vid1).value() == (unsigned)(watched[0] & 0x1)) {
1003         if (!lit.is_watched()) {
1004           assert(literal_value(lit) == 0);
1005           assert(variable(lit.var_index()).dlevel() <=
1006                   variable(vid1).dlevel());
1007         }
1008       }
1009       int vid2 = (watched[1]>>1);
1010       if (variable(vid2).value() == (unsigned)(watched[1] & 0x1)) {
1011         if (!lit.is_watched()) {
1012           assert(literal_value(lit) == 0);
1013           assert(variable(lit.var_index()).dlevel() <=
1014                   variable(vid1).dlevel());
1015         }
1016       }
1017     }
1018   }
1019 }
1020
1021 void CSolver::mark_vars(ClauseIdx cl, int var_idx) {
1022   assert(_resolvents.empty() || var_idx != -1);
1023 #ifdef VERIFY_ON
1024   _resolvents.push_back(clause(cl).id());
1025 #endif
1026   for (CLitPoolElement* itr = clause(cl).literals(); (*itr).val() > 0; ++itr) {
1027     int v = (*itr).var_index();
1028     if (v == var_idx)
1029       continue;
1030     else if (variable(v).dlevel() == dlevel()) {
1031       if (!variable(v).is_marked()) {
1032         variable(v).set_marked();
1033         ++_num_marked;
1034         if (_mark_increase_score) {
1035           int tmp = itr->s_var();
1036           adjust_variable_order(&tmp, 1);
1037         }
1038       }
1039     } else {
1040       assert(variable(v).dlevel() < dlevel());
1041       if (variable(v).new_cl_phase() == UNKNOWN) {  // it's not in the new cl
1042         // We can remove the variable assigned at dlevel 0 if
1043         // we are nog going to use incremental SAT.
1044         // if(variable(v).dlevel()){
1045           ++_num_in_new_cl;
1046           variable(v).set_new_cl_phase((*itr).var_sign());
1047           _conflict_lits.push_back((*itr).s_var());
1048         // }
1049        } else {
1050          // if this variable is already in the new clause, it must
1051          // have the same phase
1052          assert(variable(v).new_cl_phase() == (*itr).var_sign());
1053        }
1054     }
1055   }
1056 }
1057
1058 int CSolver::analyze_conflicts(void) {
1059   assert(!_conflicts.empty());
1060   assert(_conflict_lits.size() == 0);
1061   assert(_implication_queue.empty());
1062   assert(_num_marked == 0);
1063   if (dlevel() == 0) {  // already at level 0. Conflict means unsat.
1064 #ifdef VERIFY_ON
1065     for (unsigned i = 1; i < variables()->size(); ++i) {
1066       if (variable(i).value() != UNKNOWN) {
1067         assert(variable(i).dlevel() <= 0);
1068         int ante = variable(i).antecedent();
1069         int ante_id = 0;
1070         if (ante >= 0) {
1071           ante_id = clause(ante).id();
1072           assert(clause(ante).status() != DELETED_CL);
1073           verify_out << "VAR: " << i
1074                      << " L: " << variable(i).assgn_stack_pos()
1075                      << " V: " << variable(i).value()
1076                      << " A: " << ante_id
1077                      << " Lits:";
1078           for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
1079             verify_out << " " << clause(ante).literal(j).s_var();
1080           verify_out << endl;
1081         }
1082       }
1083     }
1084     ClauseIdx shortest;
1085     shortest = _conflicts.back();
1086     unsigned len = clause(_conflicts.back()).num_lits();
1087     while (!_conflicts.empty()) {
1088       if (clause(_conflicts.back()).num_lits() < len) {
1089         shortest = _conflicts.back();
1090         len = clause(_conflicts.back()).num_lits();
1091       }
1092       _conflicts.pop_back();
1093     }
1094     verify_out << "CONF: " << clause(shortest).id() << " ==";
1095     for (unsigned i = 0; i < clause(shortest).num_lits(); ++i) {
1096       int svar = clause(shortest).literal(i).s_var();
1097       verify_out << " " << svar;
1098     }
1099     verify_out << endl;
1100 #endif
1101     _conflicts.clear();
1102     back_track(0);
1103     return -1;
1104   }
1105   return  conflict_analysis_firstUIP();
1106 }
1107
1108 // when all the literals involved are in _conflict_lits
1109 // call this function to finish the adding clause and backtrack
1110
1111 int CSolver::finish_add_conf_clause(int gflag) {
1112   ClauseIdx added_cl = add_conflict_clause(&(*_conflict_lits.begin()),
1113                                            _conflict_lits.size(), gflag);
1114   if (added_cl < 0) {  // memory out.
1115     _stats.is_mem_out = true;
1116     _conflicts.clear();
1117     assert(_implication_queue.empty());
1118     return 1;
1119   }
1120
1121   top_unsat_cls = clauses()->size() - 1;
1122
1123 #ifdef VERIFY_ON
1124   verify_out << "CL: " <<  clause(added_cl).id() << " <=";
1125   for (unsigned i = 0; i< _resolvents.size(); ++i)
1126         verify_out << " " <<  _resolvents[i];
1127     verify_out << endl;
1128     _resolvents.clear();
1129 #endif
1130
1131   adjust_variable_order(&(*_conflict_lits.begin()), _conflict_lits.size());
1132
1133   if (_params.shrinking.enable) {
1134     _shrinking_cls.clear();
1135     if (_stats.shrinking_cls_length != 0) {
1136       int benefit = _stats.shrinking_cls_length - _conflict_lits.size();
1137       _stats.shrinking_benefit += benefit;
1138       _stats.shrinking_cls_length = 0;
1139       _recent_shrinkings.push(benefit);
1140       if (_recent_shrinkings.size() > _params.shrinking.window_width) {
1141         _stats.shrinking_benefit -= _recent_shrinkings.front();
1142         _recent_shrinkings.pop();
1143       }
1144     }
1145     if (_conflict_lits.size() > _params.shrinking.size) {
1146       _shrinking_cls.clear();
1147       for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i) {
1148         _shrinking_cls.insert(pair<int, int>
1149                  (variable(_conflict_lits[i]>>1).dlevel(), _conflict_lits[i]));
1150       }
1151       int prev_dl = _shrinking_cls.begin()->first;
1152       multimap<int, int>::iterator itr, itr_del;
1153       int last_dl = _shrinking_cls.rbegin()->first;
1154
1155       bool found_gap = false;
1156       for (itr = _shrinking_cls.begin(); itr->first != last_dl;) {
1157         if (itr->first - prev_dl > 2) {
1158           found_gap = true;
1159           break;
1160         }
1161         prev_dl = itr->first;
1162         itr_del = itr;
1163         ++itr;
1164         _shrinking_cls.erase(itr_del);
1165       }
1166       if (found_gap && _shrinking_cls.size() > 0 && prev_dl < dlevel() - 1) {
1167         _stats.shrinking_cls_length = _conflict_lits.size();
1168         ++_stats.num_shrinkings;
1169         back_track(prev_dl + 1);
1170         _conflicts.clear();
1171 #ifdef VERIFY_ON
1172         _resolvents.clear();
1173 #endif
1174         _num_in_new_cl = 0;
1175         for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i)
1176           variable(_conflict_lits[i]>>1).set_new_cl_phase(UNKNOWN);
1177         _conflict_lits.clear();
1178         if (_stats.num_shrinkings %
1179             _params.shrinking.bound_update_frequency == 0 &&
1180             _recent_shrinkings.size() == _params.shrinking.window_width) {
1181           if (_stats.shrinking_benefit > _params.shrinking.upper_bound)
1182             _params.shrinking.size += _params.shrinking.upper_delta;
1183           else if (_stats.shrinking_benefit < _params.shrinking.lower_bound)
1184             _params.shrinking.size += _params.shrinking.lower_delta;
1185         }
1186         return prev_dl;
1187       }
1188     }
1189   }
1190   int back_dl = 0;
1191   int unit_lit = -1;
1192
1193   for (unsigned i = 0; i < clause(added_cl).num_lits(); ++i) {
1194     int vid = clause(added_cl).literal(i).var_index();
1195     int sign =clause(added_cl).literal(i).var_sign();
1196     assert(variable(vid).value() != UNKNOWN);
1197     assert(literal_value(clause(added_cl).literal(i)) == 0);
1198     int dl = variable(vid).dlevel();
1199     if (dl < dlevel()) {
1200       if (dl > back_dl)
1201         back_dl = dl;
1202     } else {
1203       assert(unit_lit == -1);
1204       unit_lit = vid + vid + sign;
1205     }
1206   }
1207   if (back_dl == 0) {
1208     _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
1209     _stats.next_cls_deletion = _stats.num_backtracks +
1210                                _params.cls_deletion.interval;
1211   }
1212
1213   back_track(back_dl + 1);
1214   queue_implication(unit_lit, added_cl);
1215
1216   // after resolve the first conflict, others must also be resolved
1217   // for (unsigned i = 1; i < _conflicts.size(); ++i)
1218   //   assert(!is_conflicting(_conflicts[i]));
1219
1220   _conflicts.clear();
1221
1222   while (!_conflict_lits.empty()) {
1223     int svar = _conflict_lits.back();
1224     _conflict_lits.pop_back();
1225     CVariable & var = variable(svar >> 1);
1226     assert(var.new_cl_phase() == (unsigned)(svar & 0x1));
1227     --_num_in_new_cl;
1228     var.set_new_cl_phase(UNKNOWN);
1229   }
1230   assert(_num_in_new_cl == 0);
1231   return back_dl;
1232 }
1233
1234 int CSolver::conflict_analysis_firstUIP(void) {
1235   int min_conf_id = _conflicts[0];
1236   int min_conf_length = -1;
1237   ClauseIdx cl;
1238   unsigned gflag;
1239   _mark_increase_score = false;
1240   if (_conflicts.size() > 1) {
1241     for (vector<ClauseIdx>::iterator ci = _conflicts.begin();
1242          ci != _conflicts.end(); ci++) {
1243       assert(_num_in_new_cl == 0);
1244       assert(dlevel() > 0);
1245       cl = *ci;
1246       mark_vars(cl, -1);
1247       // current dl must be the conflict cl.
1248       vector <int> & assignments = *_assignment_stack[dlevel()];
1249       // now add conflict lits, and unassign vars
1250       for (int i = assignments.size() - 1; i >= 0; --i) {
1251         int assigned = assignments[i];
1252         if (variable(assigned >> 1).is_marked()) {
1253           // this variable is involved in the conflict clause or its antecedent
1254           variable(assigned>>1).clear_marked();
1255           --_num_marked;
1256           ClauseIdx ante_cl = variable(assigned>>1).get_antecedent();
1257           if ( _num_marked == 0 ) {
1258             // the first UIP encountered, conclude add clause
1259             assert(variable(assigned>>1).new_cl_phase() == UNKNOWN);
1260             // add this assignment's reverse, e.g. UIP
1261             _conflict_lits.push_back(assigned ^ 0x1);
1262             ++_num_in_new_cl;
1263             variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
1264             break;
1265           } else {
1266             assert(ante_cl != NULL_CLAUSE);
1267             mark_vars(ante_cl, assigned >> 1);
1268           }
1269         }
1270       }
1271       if (min_conf_length == -1 ||
1272           (int)_conflict_lits.size() < min_conf_length) {
1273         min_conf_length = _conflict_lits.size();
1274         min_conf_id = cl;
1275       }
1276
1277       for (vector<int>::iterator vi = _conflict_lits.begin(); vi !=
1278            _conflict_lits.end(); ++vi) {
1279         int s_var = *vi;
1280         CVariable & var = variable(s_var >> 1);
1281         assert(var.new_cl_phase() == (unsigned)(s_var & 0x1));
1282         var.set_new_cl_phase(UNKNOWN);
1283       }
1284       _num_in_new_cl = 0;
1285       _conflict_lits.clear();
1286 #ifdef VERIFY_ON
1287       _resolvents.clear();
1288 #endif
1289     }
1290   }
1291
1292   assert(_num_marked == 0);
1293   cl = min_conf_id;
1294   clause(cl).activity() += 5;
1295   _mark_increase_score = true;
1296   mark_vars(cl, -1);
1297   gflag = clause(cl).gflag();
1298   vector <int> & assignments = *_assignment_stack[dlevel()];
1299   for (int i = assignments.size() - 1; i >= 0; --i) {
1300     int assigned = assignments[i];
1301     if (variable(assigned >> 1).is_marked()) {
1302       variable(assigned>>1).clear_marked();
1303       --_num_marked;
1304       ClauseIdx ante_cl = variable(assigned>>1).get_antecedent();
1305       if ( _num_marked == 0 ) {
1306         _conflict_lits.push_back(assigned ^ 0x1);
1307         ++_num_in_new_cl;
1308         variable(assigned >> 1).set_new_cl_phase((assigned ^ 0x1) & 0x1);
1309         break;
1310       } else {
1311         gflag |= clause(ante_cl).gflag();
1312         mark_vars(ante_cl, assigned >> 1);
1313         clause(ante_cl).activity() += 5;
1314       }
1315     }
1316   }
1317   return finish_add_conf_clause(gflag);
1318 }
1319
1320 void CSolver::print_cls(ostream & os) {
1321   for (unsigned i = 0; i < clauses()->size(); ++i) {
1322     CClause & cl = clause(i);
1323     if (cl.status() == DELETED_CL)
1324       continue;
1325     if (cl.status() == ORIGINAL_CL) {
1326       os <<"0 ";
1327     } else {
1328       assert(cl.status() == CONFLICT_CL);
1329       os << "A ";
1330     }
1331     for (unsigned j = 1; j < 33; ++j)
1332       os << (cl.gid(j) ? 1 : 0);
1333     os << "\t";
1334     for (unsigned j = 0; j < cl.num_lits(); ++j) {
1335       os << (cl.literal(j).var_sign() ? "-":"")
1336          << cl.literal(j).var_index() << " ";
1337     }
1338     os <<"0" <<  endl;
1339   }
1340 }
1341
1342 int CSolver::mem_usage(void) {
1343   int mem_dbase = CDatabase::mem_usage();
1344   int mem_assignment = 0;
1345   for (int i = 0; i < _stats.max_dlevel; ++i)
1346     mem_assignment += _assignment_stack[i]->capacity() * sizeof(int);
1347   mem_assignment += sizeof(vector<int>)* _assignment_stack.size();
1348   return mem_dbase + mem_assignment;
1349 }
1350
1351 void CSolver::clean_up_dbase(void) {
1352   assert(dlevel() == 0);
1353
1354   int mem_before = mem_usage();
1355   // 1. remove all the learned clauses
1356   for (vector<CClause>::iterator itr = clauses()->begin();
1357        itr != clauses()->end() - 1; ++itr) {
1358     CClause & cl = * itr;
1359     if (cl.status() != ORIGINAL_CL)
1360       mark_clause_deleted(cl);
1361   }
1362   // delete_unrelevant_clauses() is specialized using berkmin deletion strategy
1363
1364   // 2. free up the mem for the vectors if possible
1365   for (unsigned i = 0; i < variables()->size(); ++i) {
1366     for (unsigned j = 0; j < 2; ++j) {  // both phase
1367       vector<CLitPoolElement *> watched;
1368       vector<CLitPoolElement *> & old_watched = variable(i).watched(j);
1369       watched.reserve(old_watched.size());
1370       for (vector<CLitPoolElement *>::iterator itr = old_watched.begin();
1371            itr != old_watched.end(); ++itr)
1372         watched.push_back(*itr);
1373         // because watched is a temp mem allocation, it will get deleted
1374         // out of the scope, but by swap it with the old_watched, the
1375         // contents are reserved.
1376         old_watched.swap(watched);
1377 #ifdef KEEP_LIT_CLAUSES
1378         vector<int> lits_cls;
1379         vector<int> & old_lits_cls = variable(i).lit_clause(j);
1380         lits_cls.reserve(old_lits_cls.size());
1381         for (vector<int>::iterator itr1 = old_lits_cls.begin(); itr1 !=
1382             old_lits_cls.end(); ++itr1)
1383           lits_cls.push_back(*itr1);
1384         old_lits_cls.swap(lits_cls);
1385 #endif
1386     }
1387   }
1388
1389   int mem_after = mem_usage();
1390   if (_params.verbosity > 0) {
1391     cout << "Database Cleaned, releasing (approximately) "
1392          << mem_before - mem_after << " Bytes" << endl;
1393   }
1394 }
1395
1396 void CSolver::update_var_score(void) {
1397   for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
1398     _ordered_vars[i-1].first = & variable(i);
1399     _ordered_vars[i-1].second = variable(i).score();
1400   }
1401   ::stable_sort(_ordered_vars.begin(), _ordered_vars.end(), cmp_var_stat);
1402   for (unsigned i = 0, sz =  _ordered_vars.size(); i < sz; ++i)
1403     _ordered_vars[i].first->set_var_score_pos(i);
1404   _max_score_pos = 0;
1405 }
1406
1407 void CSolver::restart(void) {
1408   _stats.num_restarts += 1;
1409   if (_params.verbosity > 1 )
1410     cout << "Restarting ... " << endl;
1411   if (dlevel() > 0)
1412     back_track(1);
1413   assert(dlevel() == 0);
1414 }
1415
1416 // this function can be called within a solving process. i.e. not after
1417 // solve() terminate
1418 int CSolver::add_clause_incr(int * lits, int num_lits, int gid) {
1419   // Do not mess up with shrinking.
1420   assert(!_params.shrinking.enable || _shrinking_cls.empty());
1421   unsigned gflag;
1422   _stats.outcome = UNDETERMINED;
1423
1424   if (gid == PERMANENT_GID)
1425     gflag = 0;
1426   else if (gid == VOLATILE_GID) {
1427     gflag = ~0x0;
1428   } else {
1429     assert(gid <= WORD_WIDTH && gid > 0);
1430     gflag = (1 << (gid - 1));
1431   }
1432
1433   int cl = add_clause(lits, num_lits, gflag);
1434   if (cl < 0)
1435     return -1;
1436   clause(cl).set_status(ORIGINAL_CL);
1437
1438   if (clause(cl).num_lits() == 1) {
1439     int var_idx = clause(cl).literal(0).var_index();
1440     if (literal_value(clause(cl).literal(0)) == 0 &&
1441         variable(var_idx).dlevel() == 0) {
1442       back_track(0);
1443       if (preprocess() == CONFLICT)
1444         _stats.outcome = UNSATISFIABLE;
1445     } else {
1446       if (dlevel() > 0)
1447         back_track(1);
1448       queue_implication(clause(cl).literal(0).s_var(), cl);
1449     }
1450     return cl;
1451   }
1452
1453   for (unsigned i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {
1454     int var_idx = lits[i] >> 1;
1455     int value = variable(var_idx).value();
1456     if (value == UNKNOWN)
1457       continue;
1458     if (variable(var_idx).dlevel() == 0 &&
1459         variable(var_idx).antecedent() == -1 &&
1460         literal_value(clause(cl).literal(i)) == 0) {
1461       back_track(0);
1462       if (preprocess() == CONFLICT)
1463         _stats.outcome = UNSATISFIABLE;
1464       return cl;
1465     }
1466   }
1467
1468   int max_level = 0;
1469   int max_level2 = 0;
1470   int unit_lit = 0;
1471   int unknown_count = 0;
1472   int num_sat = 0;
1473   int sat_dlevel = -1, max_lit = 0;
1474   bool already_sat = false;
1475
1476   for (unsigned i = 0, sz = clause(cl).num_lits();
1477        unknown_count < 2 && i < sz; ++i) {
1478     int var_idx = lits[i] / 2;
1479     int value = variable(var_idx).value();
1480     if (value == UNKNOWN) {
1481       unit_lit = clause(cl).literal(i).s_var();
1482       ++unknown_count;
1483     } else {
1484       int dl = variable(var_idx).dlevel();
1485       if (dl >= max_level) {
1486         max_level2 = max_level;
1487         max_level = dl;
1488         max_lit = clause(cl).literal(i).s_var();
1489       }
1490       else if (dl > max_level2)
1491         max_level2 = dl;
1492       if (literal_value(clause(cl).literal(i)) == 1) {
1493         already_sat = true;
1494         ++num_sat;
1495         sat_dlevel = dl;
1496       }
1497     }
1498   }
1499   if (unknown_count == 0) {
1500     if (already_sat) {
1501       assert(sat_dlevel > -1);
1502       if (num_sat == 1 && sat_dlevel == max_level && max_level > max_level2) {
1503         back_track(max_level2 + 1);
1504         assert(max_lit > 1);
1505         queue_implication(max_lit, cl);
1506       }
1507     } else {
1508       assert(is_conflicting(cl));
1509       if (max_level > max_level2) {
1510         back_track(max_level2 + 1);
1511         assert(max_lit > 1);
1512         queue_implication(max_lit, cl);
1513       } else {
1514         back_track(max_level);
1515         if (max_level == 0 && preprocess() == CONFLICT)
1516           _stats.outcome = UNSATISFIABLE;
1517       }
1518     }
1519   }
1520   else if (unknown_count == 1) {
1521     if (!already_sat) {
1522       if (max_level < dlevel())
1523         back_track(max_level + 1);
1524       queue_implication(unit_lit, cl);
1525     }
1526   }
1527   return cl;
1528 }