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:
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.
20 // --- This software and any associated documentation is provided "as is"
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.
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 // ********************************************************************
46 #include "zchaff_solver.h"
51 ofstream verify_out("resolve_trace");
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;
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;
79 void CSolver::init_stats(void) {
82 _stats.been_reset = true;
83 _stats.num_free_variables = 0;
84 _stats.num_free_branch_vars = 0;
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;
99 _params.decision.base_randomness = 0;
100 _params.decision.decay_period = 40;
101 _params.decision.bubble_init_step = 0x400;
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;
111 _params.restart.enable = true;
112 _params.restart.interval = 700;
113 _params.restart.first_restart = 7000;
114 _params.restart.backtrack_incr = 700;
117 CSolver::CSolver(void) {
121 _force_terminate = false;
125 _outside_constraint_hook = NULL;
129 CSolver::~CSolver(void) {
130 while (!_assignment_stack.empty()) {
131 delete _assignment_stack.back();
132 _assignment_stack.pop_back();
136 void CSolver::set_time_limit(float t) {
137 _params.time_limit = t;
140 float CSolver::elapsed_cpu_time(void) {
141 return get_cpu_time() - _stats.start_cpu_time;
144 float CSolver::cpu_run_time(void) {
145 return (_stats.finish_cpu_time - _stats.start_cpu_time);
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);
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);
166 void CSolver::set_mem_limit(int s) {
167 CDatabase::set_mem_limit(s);
170 void CSolver::set_randomness(int n) {
171 _params.decision.base_randomness = n;
174 void CSolver::set_random_seed(int seed) {
178 void CSolver::enable_cls_deletion(bool allow) {
179 _params.cls_deletion.enable = allow;
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));
187 void CSolver::run_periodic_functions(void) {
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();
194 if (_stats.num_restarts % 5 == 1)
196 cout << "\rDecision: " << _assignment_stack[0]->size() << "/"
197 <<num_variables() << "\tTime: " << get_cpu_time() -
198 _stats.start_cpu_time << "/" << _params.time_limit << flush;
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();
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);
218 void CSolver::init_solve(void) {
219 CDatabase::init_stats();
221 _stats.been_reset = false;
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);
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);
234 _ordered_vars.resize(num_variables());
237 set_random_seed(_stats.random_seed);
239 top_unsat_cls = clauses()->size() - 1;
241 _stats.shrinking_benefit = 0;
242 _shrinking_cls.clear();
243 _stats.shrinking_cls_length = 0;
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());
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);
259 ++_stats.num_implications ;
260 if (var.is_branchable())
261 --num_free_variables();
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) {
269 CLitPoolElement * other_watched = *itr;
270 CLitPoolElement * watched = *itr;
271 int dir = watched->direction();
272 CLitPoolElement * ptr = watched;
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.
280 dir = -dir; // change direction, go the other way
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);
291 if (ptr->is_watched()) { // literal is the other watched lit, skip it.
295 if (literal_value(*ptr) == 0) // literal value is 0, keep going
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);
302 // remove the original watched literal from watched list
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
312 void CSolver::unset_var_value(int v) {
315 CVariable & var = variable(v);
316 var.set_value(UNKNOWN);
317 var.set_antecedent(NULL_CLAUSE);
319 var.assgn_stack_pos() = -1;
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();
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) << " ";
341 void CSolver::dump_implication_queue(ostream & os) {
342 _implication_queue.dump(os);
345 void CSolver::delete_clause_group(int gid) {
346 assert(is_gid_allocated(gid));
348 if (_stats.been_reset == false)
349 reset(); // if delete some clause, then implication queue are invalidated
351 for (vector<CClause>::iterator itr = clauses()->begin();
352 itr != clauses()->end(); ++itr) {
354 if (cl.status() != DELETED_CL) {
355 if (cl.gid(gid) == true) {
356 mark_clause_deleted(cl);
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();
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();
392 void CSolver::reset(void) {
393 if (_stats.been_reset)
395 if (num_variables() == 0)
399 while (!_implication_queue.empty())
400 _implication_queue.pop();
402 _stats.outcome = UNDETERMINED;
403 _stats.been_reset = true;
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;
411 for (vector<CClause>::iterator itr = clauses()->begin();
412 itr != clauses()->end() - 1; ++itr) {
414 if (cl.status() != CONFLICT_CL) {
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;
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));
433 if (lit_value == UNKNOWN)
435 if (unknown_lits + val_1_lits > 1) {
436 mark_clause_deleted(cl);
444 int max_activity = _params.cls_deletion.head_activity -
445 (_params.cls_deletion.head_activity -
446 _params.cls_deletion.tail_activity) *
448 int max_conf_cls_size;
450 if (head_count > 0) {
451 max_conf_cls_size = _params.cls_deletion.head_num_lits;
454 max_conf_cls_size = _params.cls_deletion.tail_num_lits;
457 if (cl.activity() > max_activity)
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));
465 else if (lit_value == 1)
469 if ((unknown_lits > max_conf_cls_size)) {
470 mark_clause_deleted(cl);
476 // if none were recently marked for deletion...
477 if (original_del_cls == num_deleted_clauses())
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();
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();
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);
516 else if (variable(i).lits_count(1) == 0 &&
517 variable(i).value() == UNKNOWN) {
518 queue_implication(i * 2, NULL_CLAUSE);
521 variable(i).score(0) = 0;
522 variable(i).score(1) = 0;
528 bool CSolver::time_out(void) {
529 return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit);
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)
543 int pos = var.var_score_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)
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)
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;
569 void CSolver::decay_variable_score(void) {
571 for (i = 1, sz = variables()->size(); i < sz; ++i) {
572 CVariable & var = variable(i);
576 for (i = 0, sz = _ordered_vars.size(); i < sz; ++i) {
577 _ordered_vars[i].second = _ordered_vars[i].first->score();
581 bool CSolver::decide_next_branch(void) {
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);
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++;
600 queue_implication(s_var ^ 0x1, NULL_CLAUSE);
606 if (_outside_constraint_hook != NULL)
607 _outside_constraint_hook(this);
609 if (!_implication_queue.empty())
610 return (_implication_queue.front().lit != 0);
612 ++_stats.num_decisions;
613 if (num_free_variables() == 0) // no more free vars
617 int i, sz, var_idx, score, max_score = -1;
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)
624 if (cl.sat_lit_idx() < (int)cl.num_lits() &&
625 literal_value(cl.literal(cl.sat_lit_idx())) == 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) {
633 cl.sat_lit_idx() = i;
636 else if (variable(var_idx).value() == UNKNOWN) {
637 score = variable(var_idx).score();
638 if (score > max_score) {
648 if (!cls_sat && max_score != -1) {
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))
655 else if (v.score(0) == v.score(1)) {
656 if (v.two_lits_count(0) > v.two_lits_count(1))
658 else if (v.two_lits_count(0) == v.two_lits_count(1))
662 queue_implication(s_var, NULL_CLAUSE);
663 ++_stats.num_decisions_stack_conf;
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
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);
682 if (_ordered_vars[index].first->value() == UNKNOWN &&
683 _ordered_vars[index].first->is_branchable())
686 CVariable * ptr = _ordered_vars[index].first;
687 assert(ptr->value() == UNKNOWN && ptr->is_branchable());
689 if (ptr->score(0) < ptr->score(1))
691 else if (ptr->score(0) == ptr->score(1)) {
692 if (ptr->two_lits_count(0) > ptr->two_lits_count(1))
694 else if (ptr->two_lits_count(0) == ptr->two_lits_count(1))
697 int var_idx = ptr - &(*variables()->begin());
698 s_var = var_idx + var_idx + sign;
702 assert(s_var >= 2); // there must be a free var somewhere
704 if (dlevel() > _stats.max_dlevel)
705 _stats.max_dlevel = dlevel();
706 ++_stats.num_decisions_vsids;
708 queue_implication(s_var, NULL_CLAUSE);
712 int CSolver::preprocess(void) {
713 assert(dlevel() == 0);
715 // 1. detect all the unused variables
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);
723 assert(r == NO_CONFLICT);
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] << " ";
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)
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);
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);
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] << " ";
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);
767 if (deduce() == CONFLICT) {
768 cout << " CONFLICT during preprocess " <<endl;
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();
776 ante_id = clause(ante).id();
777 verify_out << "VAR: " << i
778 << " L: " << variable(i).assgn_stack_pos()
779 << " V: " << variable(i).value()
782 for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
783 verify_out <<" " << clause(ante).literal(j).s_var();
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;
797 if (_params.verbosity > 1) {
798 cout << _assignment_stack[0]->size() << " vars set during preprocess; "
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();
812 void CSolver::mark_var_branchable(int vid) {
813 CVariable & var = variable(vid);
814 if (!var.is_branchable()) {
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();
824 ClauseIdx CSolver::add_orig_clause(int * lits, int n_lits, int gid) {
825 int cid = add_clause_with_gid(lits, n_lits, gid);
827 clause(cid).set_status(ORIGINAL_CL);
828 clause(cid).activity() = 0;
833 ClauseIdx CSolver::add_clause_with_gid(int * lits, int n_lits, int gid) {
835 if (gid == PERMANENT_GID )
837 else if (gid == VOLATILE_GID) {
840 assert(gid <= WORD_WIDTH && gid > 0);
841 gflag = (1 << (gid- 1));
843 ClauseIdx cid = add_clause(lits, n_lits, gflag);
845 _stats.is_mem_out = true;
846 _stats.outcome = MEM_OUT;
851 ClauseIdx CSolver::add_conflict_clause(int * lits, int n_lits, int gflag) {
852 ClauseIdx cid = add_clause(lits, n_lits, gflag);
854 clause(cid).set_status(CONFLICT_CL);
855 clause(cid).activity() = 0;
857 _stats.is_mem_out = true;
858 _stats.outcome = MEM_OUT;
863 void CSolver::real_solve(void) {
864 while (_stats.outcome == UNDETERMINED) {
865 run_periodic_functions();
866 if (decide_next_branch()) {
867 while (deduce() == CONFLICT) {
869 blevel = analyze_conflicts();
871 _stats.outcome = UNSATISFIABLE;
876 if (_sat_hook != NULL && _sat_hook(this))
878 _stats.outcome = SATISFIABLE;
882 _stats.outcome = TIME_OUT;
885 if (_force_terminate) {
886 _stats.outcome = ABORTED;
889 if (_stats.is_mem_out) {
890 _stats.outcome = MEM_OUT;
896 int CSolver::solve(void) {
897 if (_stats.outcome == UNDETERMINED) {
900 if (preprocess() == CONFLICT)
901 _stats.outcome = UNSATISFIABLE;
902 else // the real search
905 _stats.finish_cpu_time = get_cpu_time();
907 return _stats.outcome;
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);
918 dlevel() = blevel - 1;
921 ++_stats.num_backtracks;
924 int CSolver::deduce(void) {
925 while (!_implication_queue.empty()) {
926 const CImplication & imp = _implication_queue.front();
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());
935 else if (var.value() == (unsigned)(lit & 0x1)) {
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);
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());
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);
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));
968 for (unsigned i = 0; i < clauses()->size(); ++i) {
969 if (clause(i).status() == DELETED_CL)
971 CClause & cl = clause(i);
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) {
984 if (literal_value(lit) == 0)
989 if (lit.is_watched()) {
990 watched[watch_index] = lit.s_var();
994 if (watch_index == 0) {
995 assert(cl.num_lits() == 1);
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());
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());
1021 void CSolver::mark_vars(ClauseIdx cl, int var_idx) {
1022 assert(_resolvents.empty() || var_idx != -1);
1024 _resolvents.push_back(clause(cl).id());
1026 for (CLitPoolElement* itr = clause(cl).literals(); (*itr).val() > 0; ++itr) {
1027 int v = (*itr).var_index();
1030 else if (variable(v).dlevel() == dlevel()) {
1031 if (!variable(v).is_marked()) {
1032 variable(v).set_marked();
1034 if (_mark_increase_score) {
1035 int tmp = itr->s_var();
1036 adjust_variable_order(&tmp, 1);
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()){
1046 variable(v).set_new_cl_phase((*itr).var_sign());
1047 _conflict_lits.push_back((*itr).s_var());
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());
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.
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();
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
1078 for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
1079 verify_out << " " << clause(ante).literal(j).s_var();
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();
1092 _conflicts.pop_back();
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;
1105 return conflict_analysis_firstUIP();
1108 // when all the literals involved are in _conflict_lits
1109 // call this function to finish the adding clause and backtrack
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;
1117 assert(_implication_queue.empty());
1121 top_unsat_cls = clauses()->size() - 1;
1124 verify_out << "CL: " << clause(added_cl).id() << " <=";
1125 for (unsigned i = 0; i< _resolvents.size(); ++i)
1126 verify_out << " " << _resolvents[i];
1128 _resolvents.clear();
1131 adjust_variable_order(&(*_conflict_lits.begin()), _conflict_lits.size());
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();
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]));
1151 int prev_dl = _shrinking_cls.begin()->first;
1152 multimap<int, int>::iterator itr, itr_del;
1153 int last_dl = _shrinking_cls.rbegin()->first;
1155 bool found_gap = false;
1156 for (itr = _shrinking_cls.begin(); itr->first != last_dl;) {
1157 if (itr->first - prev_dl > 2) {
1161 prev_dl = itr->first;
1164 _shrinking_cls.erase(itr_del);
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);
1172 _resolvents.clear();
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;
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()) {
1203 assert(unit_lit == -1);
1204 unit_lit = vid + vid + sign;
1208 _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
1209 _stats.next_cls_deletion = _stats.num_backtracks +
1210 _params.cls_deletion.interval;
1213 back_track(back_dl + 1);
1214 queue_implication(unit_lit, added_cl);
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]));
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));
1228 var.set_new_cl_phase(UNKNOWN);
1230 assert(_num_in_new_cl == 0);
1234 int CSolver::conflict_analysis_firstUIP(void) {
1235 int min_conf_id = _conflicts[0];
1236 int min_conf_length = -1;
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);
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();
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);
1263 variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
1266 assert(ante_cl != NULL_CLAUSE);
1267 mark_vars(ante_cl, assigned >> 1);
1271 if (min_conf_length == -1 ||
1272 (int)_conflict_lits.size() < min_conf_length) {
1273 min_conf_length = _conflict_lits.size();
1277 for (vector<int>::iterator vi = _conflict_lits.begin(); vi !=
1278 _conflict_lits.end(); ++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);
1285 _conflict_lits.clear();
1287 _resolvents.clear();
1292 assert(_num_marked == 0);
1294 clause(cl).activity() += 5;
1295 _mark_increase_score = true;
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();
1304 ClauseIdx ante_cl = variable(assigned>>1).get_antecedent();
1305 if ( _num_marked == 0 ) {
1306 _conflict_lits.push_back(assigned ^ 0x1);
1308 variable(assigned >> 1).set_new_cl_phase((assigned ^ 0x1) & 0x1);
1311 gflag |= clause(ante_cl).gflag();
1312 mark_vars(ante_cl, assigned >> 1);
1313 clause(ante_cl).activity() += 5;
1317 return finish_add_conf_clause(gflag);
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)
1325 if (cl.status() == ORIGINAL_CL) {
1328 assert(cl.status() == CONFLICT_CL);
1331 for (unsigned j = 1; j < 33; ++j)
1332 os << (cl.gid(j) ? 1 : 0);
1334 for (unsigned j = 0; j < cl.num_lits(); ++j) {
1335 os << (cl.literal(j).var_sign() ? "-":"")
1336 << cl.literal(j).var_index() << " ";
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;
1351 void CSolver::clean_up_dbase(void) {
1352 assert(dlevel() == 0);
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);
1362 // delete_unrelevant_clauses() is specialized using berkmin deletion strategy
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);
1389 int mem_after = mem_usage();
1390 if (_params.verbosity > 0) {
1391 cout << "Database Cleaned, releasing (approximately) "
1392 << mem_before - mem_after << " Bytes" << endl;
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();
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);
1407 void CSolver::restart(void) {
1408 _stats.num_restarts += 1;
1409 if (_params.verbosity > 1 )
1410 cout << "Restarting ... " << endl;
1413 assert(dlevel() == 0);
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());
1422 _stats.outcome = UNDETERMINED;
1424 if (gid == PERMANENT_GID)
1426 else if (gid == VOLATILE_GID) {
1429 assert(gid <= WORD_WIDTH && gid > 0);
1430 gflag = (1 << (gid - 1));
1433 int cl = add_clause(lits, num_lits, gflag);
1436 clause(cl).set_status(ORIGINAL_CL);
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) {
1443 if (preprocess() == CONFLICT)
1444 _stats.outcome = UNSATISFIABLE;
1448 queue_implication(clause(cl).literal(0).s_var(), cl);
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)
1458 if (variable(var_idx).dlevel() == 0 &&
1459 variable(var_idx).antecedent() == -1 &&
1460 literal_value(clause(cl).literal(i)) == 0) {
1462 if (preprocess() == CONFLICT)
1463 _stats.outcome = UNSATISFIABLE;
1471 int unknown_count = 0;
1473 int sat_dlevel = -1, max_lit = 0;
1474 bool already_sat = false;
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();
1484 int dl = variable(var_idx).dlevel();
1485 if (dl >= max_level) {
1486 max_level2 = max_level;
1488 max_lit = clause(cl).literal(i).s_var();
1490 else if (dl > max_level2)
1492 if (literal_value(clause(cl).literal(i)) == 1) {
1499 if (unknown_count == 0) {
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);
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);
1514 back_track(max_level);
1515 if (max_level == 0 && preprocess() == CONFLICT)
1516 _stats.outcome = UNSATISFIABLE;
1520 else if (unknown_count == 1) {
1522 if (max_level < dlevel())
1523 back_track(max_level + 1);
1524 queue_implication(unit_lit, cl);