00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039 #include "xchaff_solver.h"
00040 #include <algorithm>
00041
00042
00043 CSolver::CSolver(void)
00044 {
00045 dlevel()=0;
00046 _params.time_limit = 3600 * 48;
00047 _params.decision_strategy = 0;
00048 _params.preprocess_strategy = 0;
00049 _params.allow_clause_deletion = true ;
00050 _params.clause_deletion_interval = 5000;
00051 _params.max_unrelevance = 20;
00052 _params.min_num_clause_lits_for_delete = 100;
00053 _params.max_conflict_clause_length = 5000;
00054 _params.bubble_init_step = 32;
00055
00056 _params.randomness = 0;
00057 _params.verbosity = 0;
00058
00059 _params.back_track_complete = true;
00060 _params.allow_multiple_conflict = false;
00061 _params.allow_multiple_conflict_clause = false;
00062
00063 _params.allow_restart = true;
00064 _params.next_restart_time = 50;
00065 _params.restart_time_increment = 0;
00066 _params.restart_time_incr_incr = 0;
00067
00068 _params.next_restart_backtrack= 0;
00069 _params.restart_backtrack_incr= 40000;
00070 _params.restart_backtrack_incr_incr = 100;
00071
00072 _params.restart_randomness = 0;
00073 _params.base_randomness = 0;
00074 _params.randomness = 0;
00075
00076 _stats.is_solver_started = false;
00077 _stats.outcome = UNKNOWN;
00078 _stats.is_mem_out = false;
00079 _stats.start_cpu_time = 0;
00080 _stats.finish_cpu_time = 0;
00081 _stats.last_cpu_time = 0;
00082
00083 _stats.start_world_time = 0;
00084 _stats.finish_world_time = 0;
00085
00086 _stats.num_decisions = 0;
00087 _stats.num_backtracks = 0;
00088 _stats.max_dlevel = 0;
00089 _stats.num_implications = 0;
00090
00091 _num_marked = 0;
00092 _dlevel = 0;
00093 _stats.total_bubble_move = 0;
00094
00095 _dlevel_hook = NULL;
00096 _decision_hook = NULL;
00097 _assignment_hook = NULL;
00098 _deduction_hook = NULL;
00099 }
00100
00101 CSolver::~CSolver()
00102 {
00103 if (_stats.is_solver_started) {
00104 for (unsigned i=0; i<variables().size(); ++i)
00105 delete _assignment_stack[i];
00106 }
00107 }
00108
00109 void CSolver::run_periodic_functions(void)
00110 {
00111
00112 if ( _params.allow_clause_deletion &&
00113 _stats.num_backtracks % _params.clause_deletion_interval == 0)
00114 delete_unrelevant_clauses();
00115
00116 if (_params.allow_restart && _stats.num_backtracks > _params.next_restart_backtrack) {
00117 _params.next_restart_backtrack += _params.restart_backtrack_incr;
00118 _params.restart_backtrack_incr += _params.restart_backtrack_incr_incr;
00119 float current = current_cpu_time()/1000;
00120 if (current > _params.next_restart_time) {
00121 if (_params.verbosity > 1) cout << "restart..." << endl;
00122 _params.next_restart_time = current + _params.restart_time_increment;
00123 _params.restart_time_increment += _params.restart_time_incr_incr;
00124 _params.randomness = _params.restart_randomness;
00125 restart();
00126 }
00127 }
00128
00129 if ((_stats.num_decisions % 0xff)==0)
00130 update_var_stats();
00131
00132 for (unsigned i=0; i< _hooks.size(); ++i) {
00133 pair<int,pair<HookFunPtrT, int> > & hook = _hooks[i];
00134 if (_stats.num_decisions >= hook.first) {
00135 hook.first += hook.second.second;
00136 hook.second.first((void *) this);
00137 }
00138 }
00139 }
00140
00141
00142 void CSolver::init(void)
00143 {
00144 CDatabase::init();
00145
00146 _stats.is_solver_started = true;
00147 _stats.start_cpu_time = current_cpu_time();
00148 _stats.start_world_time = current_world_time();
00149 _stats.num_free_variables = num_variables();
00150 for (unsigned i=0; i<variables().size(); ++i)
00151 _assignment_stack.push_back(new vector<int>);
00152
00153 _var_order.resize( num_variables());
00154 _last_var_lits_count[0].resize(variables().size());
00155 _last_var_lits_count[1].resize(variables().size());
00156 CHECK(dump());
00157 }
00158
00159
00160 int CSolver::add_variables(int new_vars)
00161 {
00162 int old_num_vars = variables().size();
00163 int num_vars = old_num_vars + new_vars;
00164 variables().resize(num_vars) ;
00165 if (_stats.is_solver_started) {
00166 _stats.num_free_variables += new_vars;
00167
00168 for (int i=old_num_vars; i<num_vars; ++i) {
00169 _assignment_stack.push_back(new vector<int>);
00170 _var_order.push_back(pair<int, int>(i,0));
00171 }
00172 _last_var_lits_count[0].resize(num_vars);
00173 _last_var_lits_count[1].resize(num_vars);
00174 }
00175 return old_num_vars;
00176 }
00177
00178
00179 ClauseIdx CSolver::add_clause(vector<long>& lits, bool addConflicts) {
00180 int new_cl;
00181 int n_lits = lits.size();
00182
00183 while (lit_pool_free_space() <= n_lits + 1) {
00184 if (enlarge_lit_pool()==false)
00185 return -1;
00186
00187 }
00188
00189 if (_unused_clause_idx_queue.empty()) {
00190 new_cl = _clauses.size();
00191 _clauses.resize(new_cl + 1);
00192 }
00193 else {
00194 new_cl = _unused_clause_idx_queue.front();
00195 _unused_clause_idx_queue.pop();
00196 }
00197
00198 clause(new_cl).init(lit_pool_end(), n_lits);
00199
00200
00201 bool satisfied = false, is_unit = false, is_conflict = false;
00202 int num_unknown = 0;
00203 for (int i=0; i< n_lits; ++i){
00204 int var_idx = lits[i]>>1;
00205 if ((unsigned)var_idx >= variables().size()) {
00206 assert(false);
00207 }
00208 int var_sign = lits[i]&0x1;
00209 lit_pool_push_back( ((var_idx<<1) + var_sign) << 2);
00210 ++variable(var_idx).lits_count(var_sign);
00211 int lit_value = literal_value(clause(new_cl).literal(i));
00212
00213 if (lit_value == 1) {
00214 satisfied = true;
00215 }
00216 else if (lit_value != 0) {
00217 ++num_unknown;
00218 }
00219 }
00220 is_conflict = !satisfied && (num_unknown == 0);
00221 is_unit = !satisfied && (num_unknown == 1);
00222 assert(_stats.is_solver_started || num_unknown == n_lits);
00223 lit_pool_push_back(-new_cl);
00224
00225 if (clause(new_cl).num_lits() > 1) {
00226
00227 int max_idx = -1, max_dl = -1;
00228 CClause & cl = clause(new_cl);
00229 int i, sz = cl.num_lits();
00230 int other_ht_idx;
00231 for (i=0; i< sz; ++i) {
00232 int v_idx = cl.literals()[i].var_index();
00233 if (variable(v_idx).value()==UNKNOWN) {
00234 int v_sign = cl.literals()[i].var_sign();
00235 variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[i]);
00236 cl.literals()[i].set_ht(1);
00237 other_ht_idx = i;
00238 break;
00239 }
00240 else {
00241 if (variable(v_idx).dlevel() > max_dl) {
00242 max_dl = variable(v_idx).dlevel();
00243 max_idx = i;
00244 }
00245 }
00246 }
00247 if (i >= sz) {
00248
00249 int v_idx = cl.literals()[max_idx].var_index();
00250 int v_sign = cl.literals()[max_idx].var_sign();
00251 variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[max_idx]);
00252 cl.literals()[max_idx].set_ht(1);
00253 other_ht_idx = max_idx;
00254 }
00255 max_idx = -1; max_dl = -1;
00256 for (i=sz-1; i>=0; --i) {
00257 if (i==other_ht_idx ) continue;
00258 int v_idx = cl.literals()[i].var_index();
00259 if (variable(v_idx).value()==UNKNOWN) {
00260 int v_sign = cl.literals()[i].var_sign();
00261 variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[i]);
00262 cl.literals()[i].set_ht(-1);
00263 break;
00264 }
00265 else {
00266 if (variable(v_idx).dlevel() > max_dl) {
00267 max_dl = variable(v_idx).dlevel();
00268 max_idx = i;
00269 }
00270 }
00271 }
00272 if (i < 0) {
00273 int v_idx = cl.literals()[max_idx].var_index();
00274 int v_sign = cl.literals()[max_idx].var_sign();
00275 CLitPoolElement * lit_ptr = & cl.literals()[max_idx];
00276 variable(v_idx).ht_ptr(v_sign).push_back(lit_ptr);
00277 cl.literals()[max_idx].set_ht(-1);
00278 }
00279 }
00280
00281 ++CDatabase::_stats.num_added_clauses;
00282 CDatabase::_stats.num_added_literals += n_lits;
00283 if (is_unit && _stats.is_solver_started) {
00284 if (n_lits == 1) _addedUnitClauses.push_back(new_cl);
00285 int lit = find_unit_literal(new_cl);
00286 assert(lit);
00287 queue_implication(lit, new_cl);
00288 }
00289 else if (addConflicts && is_conflict) {
00290 _conflicts.push_back(new_cl);
00291 }
00292 return new_cl;
00293 }
00294
00295
00296 void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl)
00297 {
00298 assert (value == 0 || value == 1);
00299 CHECK_FULL(dump());
00300 CHECK(verify_integrity());
00301 CHECK (cout << "Setting\t" << (value>0?"+":"-") << v
00302 << " at " << dl << " because " << ante<< endl;);
00303 ++_stats.num_implications ;
00304 --num_free_variables();
00305 if (_assignment_hook) {
00306 (*_assignment_hook)(_assignment_hook_cookie, v, value);
00307 }
00308 CVariable & var = _variables[v];
00309 assert (var.value() == UNKNOWN);
00310 var.dlevel() = dl;
00311 var.value() = value;
00312 var.set_antecedence(ante);
00313 vector<CLitPoolElement *> & ht_ptrs = var.ht_ptr(value);
00314 if (dl == dlevel())
00315 set_var_value_with_current_dl(v, ht_ptrs);
00316 else
00317 set_var_value_not_current_dl(v, ht_ptrs);
00318 }
00319
00320
00321 void CSolver::set_var_value_with_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
00322 {
00323 ClauseIdx cl_idx;
00324 CLitPoolElement * ht_ptr, * other_ht_ptr = NULL, * ptr;
00325 int dir;
00326 for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); itr != ht_ptrs.end(); ++itr) {
00327 ht_ptr = *itr;
00328 dir = ht_ptr->direction();
00329 ptr = ht_ptr;
00330 while(1) {
00331 ptr += dir;
00332 if (ptr->val() <= 0) {
00333 if (dir == 1)
00334 cl_idx = - ptr->val();
00335 if (dir == ht_ptr->direction()) {
00336 ptr = ht_ptr;
00337 dir = -dir;
00338 continue;
00339 }
00340 int the_value = literal_value (*other_ht_ptr);
00341 if (the_value == 0)
00342 _conflicts.push_back(cl_idx);
00343 else if ( the_value != 1)
00344 queue_implication (other_ht_ptr->s_var(), cl_idx);
00345 break;
00346 }
00347 if (ptr->is_ht()) {
00348 other_ht_ptr = ptr;
00349 continue;
00350 }
00351 if (literal_value(*ptr) == 0)
00352 continue;
00353
00354 int v1 = ptr->var_index();
00355 int sign = ptr->var_sign();
00356 variable(v1).ht_ptr(sign).push_back(ptr);
00357 ht_ptr->unset_ht();
00358 ptr->set_ht(dir);
00359
00360 *itr = ht_ptrs.back();
00361 ht_ptrs.pop_back();
00362 --itr;
00363 break;
00364 }
00365 }
00366 }
00367
00368 void CSolver::set_var_value_not_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
00369 {
00370 ClauseIdx cl_idx;
00371 CLitPoolElement * ht_ptr, * other_ht_ptr = NULL, * ptr, * max_ptr = NULL;
00372 int dir,max_dl;
00373
00374 for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin();
00375 itr != ht_ptrs.end(); ++itr) {
00376 max_dl = -1;
00377 ht_ptr = *itr;
00378 dir = ht_ptr->direction();
00379 ptr = ht_ptr;
00380 while(1) {
00381 ptr += dir;
00382 if (ptr->val() <= 0) {
00383 if (dir == 1)
00384 cl_idx = - ptr->val();
00385 if (dir == ht_ptr->direction()) {
00386 ptr = ht_ptr;
00387 dir = -dir;
00388 continue;
00389 }
00390 if (variable(ht_ptr->var_index()).dlevel() < max_dl) {
00391 int v1 = max_ptr->var_index();
00392 int sign = max_ptr->var_sign();
00393 variable(v1).ht_ptr(sign).push_back(max_ptr);
00394 ht_ptr->unset_ht();
00395 max_ptr->set_ht(dir);
00396 *itr = ht_ptrs.back();
00397 ht_ptrs.pop_back();
00398 --itr;
00399 }
00400 int the_value = literal_value (*other_ht_ptr);
00401 if (the_value == 0)
00402 _conflicts.push_back(cl_idx);
00403 else if ( the_value != 1)
00404 queue_implication (other_ht_ptr->s_var(), cl_idx);
00405 break;
00406 }
00407 if (ptr->is_ht()) {
00408 other_ht_ptr = ptr;
00409 continue;
00410 }
00411 if (literal_value(*ptr) == 0) {
00412 if (variable(ptr->var_index()).dlevel() > max_dl) {
00413 max_dl = variable(ptr->var_index()).dlevel();
00414 max_ptr = ptr;
00415 }
00416 continue;
00417 }
00418
00419 int v1 = ptr->var_index();
00420 int sign = ptr->var_sign();
00421 variable(v1).ht_ptr(sign).push_back(ptr);
00422 ht_ptr->unset_ht();
00423 ptr->set_ht(dir);
00424
00425 *itr = ht_ptrs.back();
00426 ht_ptrs.pop_back();
00427 --itr;
00428 break;
00429 }
00430 }
00431 }
00432
00433 void CSolver::unset_var_value(int v)
00434 {
00435 CHECK(cout <<"Unset var " << (variable(v).value()?"+":"-") << v << endl;);
00436 CVariable & var = variable(v);
00437 if (var.var_score_pos() < _max_score_pos)
00438 _max_score_pos = var.var_score_pos();
00439 var.value() = UNKNOWN;
00440 var.set_antecedence(NULL_CLAUSE);
00441 var.dlevel() = -1;
00442 if (_assignment_hook) {
00443 (*_assignment_hook)(_assignment_hook_cookie, v, -1);
00444 }
00445 }
00446
00447 int CSolver::find_max_clause_dlevel(ClauseIdx cl)
00448 {
00449
00450 int max_level = 0;
00451 if (cl == NULL_CLAUSE || cl == FLIPPED)
00452 return dlevel();
00453 for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) {
00454 int var_idx =((clause(cl).literals())[i]).var_index();
00455 if (_variables[var_idx].value() != UNKNOWN) {
00456 if (max_level < _variables[var_idx].dlevel())
00457 max_level = _variables[var_idx].dlevel();
00458 }
00459 }
00460 return max_level;
00461 }
00462
00463 void CSolver::dump_assignment_stack(ostream & os) {
00464 cout << "Assignment Stack: ";
00465 for (int i=0; i<= dlevel(); ++i) {
00466 if ((*_assignment_stack[i]).size() > 0)
00467 if (variable( (*_assignment_stack[i])[0]>>1).get_antecedence()==FLIPPED)
00468 cout << "*" ;
00469 cout << "(" <<i << ":";
00470 for (unsigned j=0; j<(*_assignment_stack[i]).size(); ++j )
00471 cout << ((*_assignment_stack[i])[j]&0x1?"-":"+")
00472 << ((*_assignment_stack[i])[j] >> 1) << " ";
00473 cout << ") " << endl;
00474 }
00475 cout << endl;
00476 }
00477
00478
00479 bool CDatabase::is_conflict(ClauseIdx cl)
00480 {
00481 CLitPoolElement * lits = clause(cl).literals();
00482 for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i)
00483 if (literal_value(lits[i]) != 0)
00484 return false;
00485 return true;
00486 }
00487
00488 bool CDatabase::is_satisfied(ClauseIdx cl)
00489 {
00490 CLitPoolElement * lits = clause(cl).literals();
00491 for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i)
00492 if (literal_value(lits[i]) == 1)
00493 return true;
00494 return false;
00495 }
00496
00497 int CDatabase::find_unit_literal(ClauseIdx cl)
00498 {
00499
00500 int unassigned = 0;
00501 for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) {
00502 int var_idx =((clause(cl).literals())[i]).var_index();
00503 if (_variables[var_idx].value() == UNKNOWN) {
00504 if (unassigned == 0)
00505 unassigned = clause(cl).literals()[i].s_var();
00506 else
00507 return 0;
00508 }
00509 }
00510 return unassigned;
00511 }
00512
00513 void CSolver::delete_unrelevant_clauses(void)
00514 {
00515 CHECK_FULL (dump());
00516 int original_num_deleted = num_deleted_clauses();
00517 if (CDatabase::_stats.mem_used_up) {
00518 CDatabase::_stats.mem_used_up = false;
00519 if (++CDatabase::_stats.mem_used_up_counts < 5) {
00520 _params.max_unrelevance = (int) (_params.max_unrelevance * 0.8);
00521 if (_params.max_unrelevance < 4)
00522 _params.max_unrelevance = 4;
00523 _params.min_num_clause_lits_for_delete = (int) (_params.min_num_clause_lits_for_delete* 0.8);
00524 if (_params.min_num_clause_lits_for_delete < 10)
00525 _params.min_num_clause_lits_for_delete = 10;
00526 _params.max_conflict_clause_length = (int) (_params.max_conflict_clause_length*0.8);
00527 if (_params.max_conflict_clause_length < 50 )
00528 _params.max_conflict_clause_length = 50;
00529 CHECK(
00530 cout << "Forced to reduce unrelevance in clause deletion. " << endl;
00531 cout <<"MaxUnrel: " << _params.max_unrelevance
00532 << " MinLenDel: " << _params.min_num_clause_lits_for_delete
00533 << " MaxLenCL : " << _params.max_conflict_clause_length << endl;
00534 );
00535 }
00536 }
00537
00538 for (vector<CClause>::iterator itr = clauses().begin() + init_num_clauses();
00539 itr != clauses().end(); ++itr) {
00540 CClause & cl = * itr;
00541 if (!cl.in_use() || cl.num_lits() < _params.min_num_clause_lits_for_delete ) continue;
00542 int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
00543 for (int i=0; i< cl.num_lits(); ++i) {
00544 int lit_value = literal_value (cl.literal(i));
00545 if (lit_value == 0 ) ++val_0_lits;
00546 else if (lit_value == 1) ++val_1_lits;
00547 else ++unknown_lits;
00548 if (unknown_lits + val_1_lits > _params.max_unrelevance) {
00549 mark_clause_deleted(cl);
00550 _unused_clause_idx_queue.push(itr - clauses().begin());
00551 CHECK (cout << "Deleting Unrelevant clause: " << cl << endl;);
00552 break;
00553 }
00554 if (cl.num_lits() > _params.max_conflict_clause_length &&
00555 (unknown_lits+val_1_lits > 1) ) {
00556
00557 mark_clause_deleted(cl);
00558 CHECK (cout << "Deleting too large clause: " << cl << endl;);
00559 _unused_clause_idx_queue.push(itr - clauses().begin());
00560 break;
00561 }
00562 }
00563 }
00564
00565 if (original_num_deleted == num_deleted_clauses())
00566 return ;
00567 for (vector<CVariable>::iterator itr = variables().begin();
00568 itr != variables().end(); ++ itr) {
00569 for (int i=0; i<2; ++i) {
00570
00571 vector<CLitPoolElement *> & ht_ptr = (*itr).ht_ptr(i);
00572 for (vector<CLitPoolElement *>::iterator my_itr = ht_ptr.begin();
00573 my_itr != ht_ptr.end(); ++my_itr) {
00574 if ( (*my_itr)->val() <= 0) {
00575 *my_itr = ht_ptr.back();
00576 ht_ptr.pop_back();
00577 --my_itr;
00578 }
00579 }
00580 }
00581 }
00582 CHECK(cout << "Deleting " << num_deleted_clauses() - original_num_deleted << " Clause ";
00583 cout << " and " << num_deleted_literals() - original_del_lits << " Literals " << endl;);
00584 CHECK_FULL (dump());
00585 }
00586
00587 bool CSolver::time_out(void)
00588 {
00589 if ( (current_cpu_time() - _stats.start_cpu_time)/1000.0 > _params.time_limit )
00590 return true;
00591 return false;
00592 }
00593
00594 inline bool compare_var_stat(const pair<int, int> & v1,
00595 const pair<int, int> & v2)
00596 {
00597 if (v1.second > v2.second) return true;
00598 return false;
00599 }
00600
00601 void CSolver::update_var_stats(void)
00602 {
00603 for(unsigned i=1; i< variables().size(); ++i) {
00604 CVariable & var = variable(i);
00605 var.score(0) = var.score(0)/2 + var.lits_count(0) - _last_var_lits_count[0][i];
00606 var.score(1) = var.score(1)/2 + var.lits_count(1) - _last_var_lits_count[1][i];
00607 _last_var_lits_count[0][i] = var.lits_count(0);
00608 _last_var_lits_count[1][i] = var.lits_count(1);
00609 _var_order[i-1] = pair<int, int>(i, var.score());
00610 }
00611 ::stable_sort(_var_order.begin(), _var_order.end(), compare_var_stat);
00612 for (unsigned i=0; i<_var_order.size(); ++i)
00613 variable(_var_order[i].first).var_score_pos() = i;
00614 _max_score_pos = 0;
00615 }
00616
00617 bool CSolver::decide_next_branch(void)
00618 {
00619 ++_stats.num_decisions;
00620 if (!_implication_queue.empty()) {
00621
00622
00623
00624
00625 _max_score_pos = 0;
00626 return _implication_queue.front().first;
00627 }
00628
00629 int s_var = 0, s_var2;
00630 bool done = false;
00631
00632 unsigned i, var_idx, sign;
00633 CVariable * ptr;
00634
00635 for (i=_max_score_pos; i<_var_order.size(); ++i) {
00636 var_idx = _var_order[i].first;
00637 ptr = &(variables()[var_idx]);
00638 if (ptr->value()==UNKNOWN) {
00639
00640 _max_score_pos = i;
00641
00642 if (--_params.randomness < _params.base_randomness)
00643 _params.randomness = _params.base_randomness;
00644
00645 int randomness = _params.randomness;
00646 if (randomness >= num_free_variables())
00647 randomness = num_free_variables() - 1;
00648 int skip =random()%(1+randomness);
00649 int index = i;
00650 while (skip > 0) {
00651 ++index;
00652 var_idx = _var_order[index].first;
00653 ptr = &(variables()[var_idx]);
00654 if (ptr->value()==UNKNOWN)
00655 --skip;
00656 }
00657 assert (ptr->value() == UNKNOWN);
00658 sign = ptr->score(0) > ptr->score(1) ? 0 : 1;
00659 s_var = var_idx + var_idx + sign;
00660 break;
00661 }
00662 }
00663 if (s_var < 2) done = true;
00664
00665 if (_decision_hook) {
00666 s_var2 = (*_decision_hook)(_decision_hook_cookie, &done);
00667 if (done || s_var2 >= 2)
00668 s_var = s_var2;
00669 }
00670
00671 if (s_var<2)
00672 return false;
00673 ++dlevel();
00674 if (_dlevel_hook) {
00675 (*_dlevel_hook)(_dlevel_hook_cookie, 1);
00676 }
00677 if (dlevel() > _stats.max_dlevel) _stats.max_dlevel = dlevel();
00678 CHECK (cout << "**Decision at Level " << dlevel() ;
00679 cout <<": " << s_var << "\te.g. " << (s_var&0x1?"-":" ") ;
00680 cout <<(s_var>>1) << endl; );
00681 queue_implication(s_var, NULL_CLAUSE);
00682 return true;
00683 }
00684
00685 int CSolver::preprocess(bool allowNewClauses)
00686 {
00687
00688 if (!allowNewClauses) {
00689 vector<int> un_used;
00690 for (int i=1, sz=variables().size(); i<sz; ++i) {
00691 CVariable & v = variable(i);
00692 if (v.lits_count(0) == 0 && v.lits_count(1) == 0) {
00693 un_used.push_back(i);
00694 v.value() = 1;
00695 v.dlevel() = -1;
00696 }
00697 }
00698 num_free_variables() -= un_used.size();
00699 if (_params.verbosity>1 && un_used.size() > 0) {
00700 cout << un_used.size()<< " Variables are defined but not used " << endl;
00701 if (_params.verbosity > 2) {
00702 for (unsigned i=0; i< un_used.size(); ++i)
00703 cout << un_used[i] << " ";
00704 cout << endl;
00705 }
00706 }
00707
00708 vector<int> uni_phased;
00709 for (int i=1, sz=variables().size(); i<sz; ++i) {
00710 CVariable & v = variable(i);
00711 if (v.value() != UNKNOWN)
00712 continue;
00713 if (v.lits_count(0) == 0){
00714 queue_implication( i+i+1, NULL_CLAUSE);
00715 uni_phased.push_back(-i);
00716 }
00717 else if (v.lits_count(1) == 0){
00718 queue_implication( i+i, NULL_CLAUSE);
00719 uni_phased.push_back(i);
00720 }
00721 }
00722 if (_params.verbosity>1 && uni_phased.size() > 0) {
00723 cout << uni_phased.size()<< " Variables only appear in one phase." << endl;
00724 if (_params.verbosity > 2) {
00725 for (unsigned i=0; i< uni_phased.size(); ++i)
00726 cout << uni_phased[i] << " ";
00727 cout <<endl;
00728 }
00729 }
00730 }
00731
00732 for (ClauseIdx i=0, sz=clauses().size(); i<sz; ++i) {
00733 if (clause(i).num_lits() == 1){
00734 queue_implication(find_unit_literal(i), i);
00735 }
00736 }
00737
00738 if(deduce()==CONFLICT) return CONFLICT;
00739 return NO_CONFLICT;
00740 }
00741
00742 void CSolver::real_solve(void)
00743 {
00744 while(1) {
00745 run_periodic_functions();
00746 if (decide_next_branch() || !_implication_queue.empty() ||
00747 _conflicts.size() != 0) {
00748 while (deduce()==CONFLICT) {
00749 int blevel = analyze_conflicts();
00750 if (blevel <= 0) {
00751 _stats.outcome = UNSATISFIABLE;
00752 return;
00753 }
00754 else if (_addedUnitClauses.size()) {
00755
00756 unsigned idx = _addedUnitClauses.size()-1;
00757 ClauseIdx cl = _addedUnitClauses.back();
00758 int lit = find_unit_literal(cl);
00759 while (lit != 0) {
00760 queue_implication(lit, cl);
00761 if (idx == 0) break;
00762 cl = _addedUnitClauses[--idx];
00763 lit = find_unit_literal(cl);
00764 }
00765 }
00766 }
00767 }
00768 else {
00769 _stats.outcome = SATISFIABLE;
00770 return;
00771 }
00772 if (time_out()) {
00773 _stats.outcome = TIME_OUT;
00774 return;
00775 }
00776 if (_stats.is_mem_out) {
00777 _stats.outcome = MEM_OUT;
00778 return;
00779 }
00780 }
00781 }
00782
00783 int CSolver::solve(bool allowNewClauses)
00784 {
00785 init();
00786
00787 if(preprocess(allowNewClauses)==CONFLICT) {
00788 _stats.outcome = UNSATISFIABLE;
00789 }
00790 else {
00791 if (_dlevel_hook) {
00792 (*_dlevel_hook)(_dlevel_hook_cookie, 1);
00793 }
00794 real_solve();
00795 }
00796 _stats.finish_cpu_time = current_cpu_time();
00797 _stats.finish_world_time = current_world_time();
00798 return _stats.outcome;
00799 }
00800
00801 int CSolver::continueCheck()
00802 {
00803 real_solve();
00804 _stats.finish_cpu_time = current_cpu_time();
00805 _stats.finish_world_time = current_world_time();
00806 return _stats.outcome;
00807 }
00808
00809 void CSolver::back_track(int blevel)
00810 {
00811 CHECK (cout << "Back track to " << blevel <<" ,currently in "<< dlevel() << " level" << endl;);
00812 CHECK_FULL (dump());
00813 CHECK(verify_integrity());
00814 assert(blevel <= dlevel());
00815 for (int i=dlevel(); i>= blevel; --i) {
00816 vector<int> & assignments = *_assignment_stack[i];
00817 for (int j=assignments.size()-1 ; j>=0; --j)
00818 unset_var_value(assignments[j]>>1);
00819 num_free_variables() += assignments.size();
00820 assignments.clear();
00821 if (_dlevel_hook) {
00822 (*_dlevel_hook)(_dlevel_hook_cookie, -1);
00823 }
00824 }
00825 dlevel() = blevel - 1;
00826 ++_stats.num_backtracks;
00827 CHECK_FULL (dump());
00828 CHECK(verify_integrity());
00829 }
00830
00831 int CSolver::deduce(void)
00832 {
00833 restart:
00834 while (!_implication_queue.empty() && _conflicts.size()==0) {
00835 int literal = _implication_queue.front().first;
00836 int variable_index = literal>>1;
00837 ClauseIdx cl = _implication_queue.front().second;
00838 _implication_queue.pop();
00839 CVariable * the_var = &(variables()[variable_index]);
00840 if ( the_var->value() == UNKNOWN) {
00841 int dl;
00842 if (_params.back_track_complete)
00843 dl = dlevel();
00844 else
00845 dl = find_max_clause_dlevel(cl);
00846 set_var_value(variable_index, !(literal&0x1), cl, dl);
00847 the_var = &(variables()[variable_index]);
00848 _assignment_stack[dl]->push_back(literal);
00849 CHECK(verify_integrity());
00850 }
00851 else if (the_var->value() == (literal&0x1) ) {
00852
00853 _conflicts.push_back(cl);
00854 }
00855 }
00856 if (!_conflicts.size() && _deduction_hook) {
00857 (*_deduction_hook)(_deduction_hook_cookie);
00858 if (!_implication_queue.empty()) goto restart;
00859 }
00860 while(!_implication_queue.empty()) _implication_queue.pop();
00861 return (_conflicts.size()?CONFLICT:NO_CONFLICT);
00862 }
00863
00864
00865 void CSolver::verify_integrity(void)
00866 {
00867 }
00868
00869 void CSolver::mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
00870 {
00871 for (CLitPoolElement * itr = clause(cl).literals(); (*itr).val() > 0 ; ++ itr) {
00872 int v = (*itr).var_index();
00873 if (v == var_idx)
00874 continue;
00875 else if (variable(v).dlevel() == dl) {
00876 if (!variable(v).is_marked()) {
00877 variable(v).set_marked();
00878 ++ _num_marked;
00879 }
00880 }
00881 else {
00882 assert (variable(v).dlevel() < dl);
00883 if (variable(v).in_new_cl() == -1){
00884 variable(v).set_in_new_cl((*itr).var_sign());
00885 _conflict_lits.push_back((*itr).s_var());
00886 }
00887 }
00888 }
00889 }
00890
00891 int CSolver::analyze_conflicts(void) {
00892 return conflict_analysis_zchaff();
00893 }
00894
00895 int CSolver::conflict_analysis_zchaff (void)
00896 {
00897 assert (_conflicts.size());
00898 assert (_implication_queue.empty());
00899 assert (_num_marked == 0);
00900 int back_level = 0;
00901 ClauseIdx conflict_cl;
00902 vector<ClauseIdx> added_conflict_clauses;
00903 for (int i=0, sz=_conflicts.size(); i<sz; ++i) {
00904 ClauseIdx cl = _conflicts[i];
00905
00906 if (!is_conflict(cl)) continue;
00907
00908 back_level = 0;
00909 while (_conflict_lits.size()) {
00910 CVariable & var = variable(_conflict_lits.back() >> 1);
00911 _conflict_lits.pop_back();
00912 assert (var.in_new_cl() != -1);
00913 var.set_in_new_cl(-1);
00914 }
00915 int max_dlevel = find_max_clause_dlevel(cl);
00916 bool first_time = true;
00917 bool prev_is_uip = false;
00918 mark_vars_at_level (cl, -1 , max_dlevel);
00919
00920 vector <int> & assignments = *_assignment_stack[max_dlevel];
00921 for (int j = assignments.size() - 1; j >= 0; --j ) {
00922 int assigned = assignments[j];
00923 if (variable(assigned>>1).is_marked()) {
00924 variable(assigned>>1).clear_marked();
00925 -- _num_marked;
00926 ClauseIdx ante_cl = variables()[assigned>>1].get_antecedence();
00927
00928 if ( (_num_marked == 0 &&
00929 (!first_time) &&
00930 (prev_is_uip == false))
00931 || ante_cl==NULL_CLAUSE) {
00932 assert (variable(assigned>>1).in_new_cl()==-1);
00933 _conflict_lits.push_back(assigned^0x1);
00934 int conflict_cl = add_clause(_conflict_lits, false);
00935 if (conflict_cl < 0 ) {
00936 _stats.is_mem_out = true;
00937 _conflicts.clear();
00938 assert (_implication_queue.empty());
00939 return 1;
00940 }
00941 _conflict_lits.pop_back();
00942 added_conflict_clauses.push_back(conflict_cl);
00943
00944 CHECK(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;
00945 cout << "**Add Clause " <<conflict_cl<< " : "<<clause(conflict_cl) << endl;
00946 );
00947
00948 prev_is_uip = true;
00949 break;
00950 }
00951 else prev_is_uip = false;
00952
00953 if ( ante_cl != NULL_CLAUSE )
00954 mark_vars_at_level(ante_cl, assigned>>1, max_dlevel);
00955 else
00956 assert (j == 0);
00957 first_time = false;
00958 }
00959 }
00960 back_level = max_dlevel;
00961 back_track(max_dlevel);
00962 }
00963 assert (_num_marked == 0);
00964 if (back_level==0)
00965 return back_level;
00966
00967 if (_params.back_track_complete) {
00968 for (unsigned i=0; i< added_conflict_clauses.size(); ++i) {
00969 ClauseIdx cl = added_conflict_clauses[i];
00970 if (find_unit_literal(cl)) {
00971 int dl = find_max_clause_dlevel(cl);
00972 if (dl < dlevel()) {
00973 back_track(dl+1);
00974 }
00975 }
00976 }
00977 }
00978 for (int i=0, sz=added_conflict_clauses.size(); i<sz; ++i) {
00979 conflict_cl = added_conflict_clauses[i];
00980 int lit = find_unit_literal(conflict_cl);
00981 if (lit) {
00982 queue_implication(lit, conflict_cl);
00983 }
00984 }
00985
00986 _conflicts.clear();
00987
00988 while (_conflict_lits.size()) {
00989 CVariable & var = variable(_conflict_lits.back() >> 1);
00990 _conflict_lits.pop_back();
00991 assert (var.in_new_cl() != -1);
00992 var.set_in_new_cl(-1);
00993 }
00994 CHECK( dump_assignment_stack(););
00995 CHECK(cout << "Conflict Analasis: conflict at level: " << back_level;
00996 cout << " Assertion Clause is " << conflict_cl<< endl; );
00997 return back_level;
00998 }
00999
01000
01001
01002
01003
01004
01005
01006
01007
01008
01009
01010
01011
01012
01013
01014