xchaff_solver.cpp

Go to the documentation of this file.
00001 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
00002 
00003 /*********************************************************************
00004  Copyright 2000-2001, Princeton University.  All rights reserved. 
00005  By using this software the USER indicates that he or she has read, 
00006  understood and will comply with the following:
00007 
00008  --- Princeton University hereby grants USER nonexclusive permission 
00009  to use, copy and/or modify this software for internal, noncommercial,
00010  research purposes only. Any distribution, including commercial sale 
00011  or license, of this software, copies of the software, its associated 
00012  documentation and/or modifications of either is strictly prohibited 
00013  without the prior consent of Princeton University.  Title to copyright
00014  to this software and its associated documentation shall at all times 
00015  remain with Princeton University.  Appropriate copyright notice shall 
00016  be placed on all software copies, and a complete copy of this notice 
00017  shall be included in all copies of the associated documentation.  
00018  No right is  granted to use in advertising, publicity or otherwise 
00019  any trademark, service mark, or the name of Princeton University. 
00020 
00021 
00022  --- This software and any associated documentation is provided "as is" 
00023 
00024  PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 
00025  OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 
00026  PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR 
00027  ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 
00028  TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.  
00029 
00030  Princeton University shall not be liable under any circumstances for 
00031  any direct, indirect, special, incidental, or consequential damages 
00032  with respect to any claim by USER or any third party on account of 
00033  or arising from the use, or inability to use, this software or its 
00034  associated documentation, even if Princeton University has been advised
00035  of the possibility of those damages.
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;    //2 days
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;   //this set the first restart time (in seconds)
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     //a. clause deletion
00112     if ( _params.allow_clause_deletion &&
00113    _stats.num_backtracks % _params.clause_deletion_interval == 0)
00114         delete_unrelevant_clauses(); 
00115     //b. restart
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     //c. update var stats for decision
00129     if ((_stats.num_decisions % 0xff)==0) 
00130       update_var_stats();
00131     //d. run hook functions
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     //a. do we need to enlarge lits pool?
00183     while (lit_pool_free_space() <= n_lits + 1) { 
00184   if (enlarge_lit_pool()==false) 
00185       return -1; //mem out, can't enlarge lit pool, because 
00186                  //ClauseIdx can't be -1, so it shows error.
00187     } 
00188     //b. get a free cl index;
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     //c. add the clause lits to lits pool
00198     clause(new_cl).init(lit_pool_end(), n_lits);
00199 
00200     //I want to verify added clauses are either all free or all 0
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); //push in the clause idx in the end
00224     //d. set the head/tail pointers
00225     if (clause(new_cl).num_lits() > 1) {
00226   //add the ht. note: ht must be the last free var
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       //no unknown literals. so use the max dl literal
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     //update some statistics
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) //a conflict
00342         _conflicts.push_back(cl_idx);
00343     else if ( the_value != 1) //e.g. unknown
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       //now it's value is either 1 or unknown
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) //a conflict
00402         _conflicts.push_back(cl_idx);
00403     else if ( the_value != 1) //e.g. unknown
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       //now it's value is either 1 or unknown
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 //if cl has single literal, then dlevel should be 0 
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 //if it's not unit, return 0.
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 //more than one unassigned
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     //first find out the clause to delete and mark them
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) ) { //to make sure it's not generating an implication
00556                                       //and it's not an antecedence for other var assignment
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     //now delete the index from variables
00565     if (original_num_deleted == num_deleted_clauses()) 
00566   return ; //didn't delete anything
00567     for (vector<CVariable>::iterator itr = variables().begin(); 
00568    itr != variables().end(); ++ itr) {
00569   for (int i=0; i<2; ++i) { //for each phase
00570       //delete the h_t index from the vars
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   //some hook function did a decision, so skip my own decision making.
00622   //if the front of implication queue is 0, that means it's finished
00623   //because var index start from 1, so 2 *vid + sign won't be 0. 
00624   //else it's a valid decision.
00625   _max_score_pos = 0; //reset the max_score_position.
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         //move th max score position pointer
00640         _max_score_pos = i;
00641         //make some randomness happen
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) //no more free vars, solution found,  quit
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     //1. detect all the unused variables
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     //2. detect all variables with only one phase occuring
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){ //no positive phased lits.
00714       queue_implication( i+i+1, NULL_CLAUSE);
00715       uni_phased.push_back(-i);
00716   }
00717   else if (v.lits_count(1) == 0){ //no negative phased lits.
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     //3. detect all the unit clauses
00732     for (ClauseIdx i=0, sz=clauses().size(); i<sz; ++i) {
00733   if (clause(i).num_lits() == 1){ //unit clause
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                   // reassert added unit clauses
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     //preprocess 
00787     if(preprocess(allowNewClauses)==CONFLICT) {
00788   _stats.outcome = UNSATISFIABLE;
00789     }
00790     else { //the real search
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) { // an implication
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) ) { //a conflict
00852       //note: literal & 0x1 == 1 means the literal is in negative phase
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){ //it's not in the new cl
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; // reset it
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); // find the max level, which is the back track level
00916   bool first_time = true; //its the beginning
00917   bool prev_is_uip = false;
00918   mark_vars_at_level (cl, -1 /*var*/, max_dlevel);
00919 
00920   vector <int> & assignments = *_assignment_stack[max_dlevel];
00921   for (int j = assignments.size() - 1; j >= 0; --j ) { //now add conflict lits, and unassign vars
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) { //conclude add clause
00932         assert (variable(assigned>>1).in_new_cl()==-1);
00933         _conflict_lits.push_back(assigned^0x1);  // add this assignment's reverse, e.g. UIP
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();  // remove for continue use of _conflict_lits
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; //if do this, only one clause will be added.
00950     }
00951     else prev_is_uip = false;
00952 
00953     if ( ante_cl != NULL_CLAUSE ) 
00954         mark_vars_at_level(ante_cl, assigned>>1/*var*/, 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) //there are nothing to be done
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)) { //i.e. if it's a unit clause
00971       int dl = find_max_clause_dlevel(cl);
00972       if (dl < dlevel()) { //thus make sure implied vars are at current dl.
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 

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1