source: vis_dev/zchaff/zchaff_solver.cpp @ 78

Last change on this file since 78 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 47.9 KB
Line 
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
44using namespace std;
45
46#include "zchaff_solver.h"
47
48// #define VERIFY_ON
49
50#ifdef VERIFY_ON
51ofstream verify_out("resolve_trace");
52#endif
53
54void 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
79void 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
87void 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
117CSolver::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
129CSolver::~CSolver(void) {
130  while (!_assignment_stack.empty()) {
131    delete _assignment_stack.back();
132    _assignment_stack.pop_back();
133  }
134}
135
136void CSolver::set_time_limit(float t) {
137  _params.time_limit = t;
138}
139
140float CSolver::elapsed_cpu_time(void) {
141  return get_cpu_time() - _stats.start_cpu_time;
142}
143
144float CSolver::cpu_run_time(void) {
145  return (_stats.finish_cpu_time - _stats.start_cpu_time);
146}
147
148void 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
157int 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
166void CSolver::set_mem_limit(int s) {
167  CDatabase::set_mem_limit(s);
168}
169
170void CSolver::set_randomness(int n) {
171  _params.decision.base_randomness = n;
172}
173
174void CSolver::set_random_seed(int seed) {
175  srand(seed);
176}
177
178void CSolver::enable_cls_deletion(bool allow) {
179  _params.cls_deletion.enable = allow;
180}
181
182void 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
187void 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
218void 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
246void 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
264void 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
312void 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
328void 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
341void CSolver::dump_implication_queue(ostream & os) {
342  _implication_queue.dump(os);
343}
344
345void 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
392void 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
406void 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
528bool CSolver::time_out(void) {
529  return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit);
530}
531
532void 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
569void 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
581bool 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
712int 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
804void 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
812void 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
824ClauseIdx 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
833ClauseIdx 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
851ClauseIdx 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
863void 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
896int 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
910void 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
924int 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
959void 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
1021void 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
1058int 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
1111int 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
1234int 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
1320void 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
1342int 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
1351void 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
1396void 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
1407void 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
1418int 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}
Note: See TracBrowser for help on using the repository browser.