zchaff64/zchaff_dbase.cpp

   1 // *********************************************************************
   2 // Copyright 2000-2004, Princeton University.  All rights reserved.
   3 // By using this software the USER indicates that he or she has read,
   4 // understood and will comply with the following:
   5 //
   6 // --- Princeton University hereby grants USER nonexclusive permission
   7 // to use, copy and/or modify this software for internal, noncommercial,
   8 // research purposes only. Any distribution, including commercial sale
   9 // or license, of this software, copies of the software, its associated
  10 // documentation and/or modifications of either is strictly prohibited
  11 // without the prior consent of Princeton University.  Title to copyright
  12 // to this software and its associated documentation shall at all times
  13 // remain with Princeton University.  Appropriate copyright notice shall
  14 // be placed on all software copies, and a complete copy of this notice
  15 // shall be included in all copies of the associated documentation.
  16 // No right is  granted to use in advertising, publicity or otherwise
  17 // any trademark,  service mark, or the name of Princeton University.
  18 //
  19 //
  20 // --- This software and any associated documentation is provided "as is"
  21 //
  22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 // PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 // Princeton University shall not be liable under any circumstances for
  29 // any direct, indirect, special, incidental, or consequential damages
  30 // with respect to any claim by USER or any third party on account of
  31 // or arising from the use, or inability to use, this software or its
  32 // associated documentation, even if Princeton University has been advised
  33 // of the possibility of those damages.
  34 // ********************************************************************/
  35
  36 #include <iostream>
  37 #include <vector>
  38 #include <set>
  39
  40 using namespace std;
  41
  42 #include "zchaff_dbase.h"
  43
  44 CDatabase::CDatabase(void) {
  45   _stats.mem_used_up                 = false;
  46   _stats.init_num_clauses            = 0;
  47   _stats.init_num_literals           = 0;
  48   _stats.num_added_clauses           = 0;
  49   _stats.num_added_literals          = 0;
  50   _stats.num_deleted_clauses         = 0;
  51   _stats.num_del_orig_cls            = 0;
  52   _stats.num_deleted_literals        = 0;
  53   _stats.num_enlarge                 = 0;
  54   _stats.num_compact                 = 0;
  55   _lit_pool_start = (CLitPoolElement *) malloc(sizeof(CLitPoolElement) *
  56                                                STARTUP_LIT_POOL_SIZE);
  57   _lit_pool_finish = _lit_pool_start;
  58   _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;
  59   lit_pool_push_back(0);  // set the first element as a dummy element
  60   _params.mem_limit = 1024 * 1024 * 1024;  // that's 1 G
  61   variables()->resize(1);                  // var_id == 0 is never used.
  62   _allocated_gid                    = 0;
  63 }
  64
  65 CDatabase::~CDatabase(void) {
  66   free(_lit_pool_start);
  67 }
  68
  69 unsigned CDatabase::estimate_mem_usage(void) {
  70   unsigned mem_lit_pool = sizeof(CLitPoolElement) * (lit_pool_size() +
  71                                                      lit_pool_free_space());
  72   unsigned mem_vars = sizeof(CVariable) * variables()->capacity();
  73   unsigned mem_cls = sizeof(CClause) * clauses()->capacity();
  74   unsigned mem_cls_queue = sizeof(int) * _unused_clause_idx.size();
  75   unsigned mem_watched = 2 * num_clauses() * sizeof(CLitPoolElement *);
  76   unsigned mem_lit_clauses = 0;
  77 #ifdef KEEP_LIT_CLAUSES
  78   mem_lit_clauses = num_literals() * sizeof(ClauseIdx);
  79 #endif
  80   return (mem_lit_pool + mem_vars + mem_cls +
  81           mem_cls_queue + mem_watched + mem_lit_clauses);
  82 }
  83
  84 unsigned CDatabase::mem_usage(void) {
  85   int mem_lit_pool = (lit_pool_size() + lit_pool_free_space()) *
  86                      sizeof(CLitPoolElement);
  87   int mem_vars = sizeof(CVariable) * variables()->capacity();
  88   int mem_cls = sizeof(CClause) * clauses()->capacity();
  89   int mem_cls_queue = sizeof(int) * _unused_clause_idx.size();
  90   int mem_watched = 0, mem_lit_clauses = 0;
  91   for (unsigned i = 0, sz = variables()->size(); i < sz ;  ++i) {
  92     CVariable & v = variable(i);
  93     mem_watched        += v.watched(0).capacity() + v.watched(1).capacity();
  94 #ifdef KEEP_LIT_CLAUSES
  95     mem_lit_clauses += v.lit_clause(0).capacity() + v.lit_clause(1).capacity();
  96 #endif
  97   }
  98   mem_watched *= sizeof(CLitPoolElement*);
  99   mem_lit_clauses *= sizeof(ClauseIdx);
 100   return (mem_lit_pool + mem_vars + mem_cls +
 101           mem_cls_queue + mem_watched + mem_lit_clauses);
 102 }
 103
 104 int CDatabase::alloc_gid(void) {
 105   for (unsigned i = 1; i <= WORD_WIDTH; ++i) {
 106     if (is_gid_allocated(i) == false) {
 107       _allocated_gid |= (1 << (i-1));
 108       return i;
 109     }
 110   }
 111   warning(_POSITION_, "Not enough GID");
 112   return VOLATILE_GID;
 113 }
 114
 115 void CDatabase::free_gid(int gid) {
 116   assert(gid > 0 && "Can't free volatile or permanent group");
 117   assert(gid <= WORD_WIDTH && "gid > WORD_WIDTH?");
 118   if (!is_gid_allocated(gid)) {
 119     fatal(_POSITION_, "Can't free unallocated GID");
 120   }
 121   _allocated_gid &= (~(1<< (gid-1)));
 122 }
 123
 124 bool CDatabase::is_gid_allocated(int gid) {
 125   if (gid == VOLATILE_GID || gid == PERMANENT_GID)
 126     return true;
 127   assert(gid <= WORD_WIDTH && gid > 0);
 128   if (_allocated_gid & (1 << (gid -1)))
 129     return true;
 130   return false;
 131 }
 132
 133 int CDatabase::merge_clause_group(int g2, int g1) {
 134   assert(g1 >0 && g2> 0 && "Can't merge with permanent or volatile group");
 135   assert(g1 != g2);
 136   assert(is_gid_allocated(g1) && is_gid_allocated(g2));
 137   for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) {
 138     if (clause(i).status() != DELETED_CL) {
 139       if (clause(i).gid(g1) == true) {
 140         clause(i).clear_gid(g1);
 141         clause(i).set_gid(g2);
 142       }
 143     }
 144   }
 145   free_gid(g1);
 146   return g2;
 147 }
 148
 149 void CDatabase::mark_clause_deleted(CClause & cl) {
 150   ++_stats.num_deleted_clauses;
 151   _stats.num_deleted_literals += cl.num_lits();
 152   CLAUSE_STATUS status = cl.status();
 153   if (status == ORIGINAL_CL)
 154      _stats.num_del_orig_cls++;
 155   cl.set_status(DELETED_CL);
 156   for (unsigned i = 0; i < cl.num_lits(); ++i) {
 157     CLitPoolElement & l = cl.literal(i);
 158     --variable(l.var_index()).lits_count(l.var_sign());
 159     l.val() = 0;
 160   }
 161   _unused_clause_idx.insert(&cl - &(*clauses()->begin()));
 162 }
 163
 164 bool CDatabase::is_conflicting(ClauseIdx cl) {
 165   CLitPoolElement * lits = clause(cl).literals();
 166   for (int i = 0, sz= clause(cl).num_lits(); i < sz;  ++i) {
 167     if (literal_value(lits[i]) != 0)
 168       return false;
 169   }
 170   return true;
 171 }
 172
 173 bool CDatabase::is_satisfied(ClauseIdx cl) {
 174   CLitPoolElement * lits = clause(cl).literals();
 175   for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {
 176     if (literal_value(lits[i]) == 1)
 177       return true;
 178   }
 179   return false;
 180 }
 181
 182 bool CDatabase::is_unit(ClauseIdx cl) {
 183   int num_unassigned = 0;
 184   CLitPoolElement * lits = clause(cl).literals();
 185   for (unsigned i = 0, sz= clause(cl).num_lits(); i < sz;  ++i) {
 186     int value = literal_value(lits[i]);
 187     if (value == 1)
 188       return false;
 189     else if (value != 0)
 190       ++num_unassigned;
 191   }
 192   return num_unassigned == 1;
 193 }
 194
 195 int CDatabase::find_unit_literal(ClauseIdx cl) {
 196   // will return 0 if not unit
 197   int unit_lit = 0;
 198   for (int i = 0, sz = clause(cl).num_lits(); i < sz;  ++i) {
 199     int value = literal_value(clause(cl).literal(i));
 200     if (value == 1)
 201       return 0;
 202     else if (value != 0) {
 203       if (unit_lit == 0)
 204         unit_lit = clause(cl).literals()[i].s_var();
 205       else
 206         return 0;
 207     }
 208   }
 209   return unit_lit;
 210 }
 211
 212 inline CLitPoolElement * CDatabase::lit_pool_begin(void) {
 213   return _lit_pool_start;
 214 }
 215
 216 inline CLitPoolElement * CDatabase::lit_pool_end(void) {
 217   return _lit_pool_finish;
 218 }
 219
 220 inline void CDatabase::lit_pool_incr_size(int size) {
 221   _lit_pool_finish += size;
 222   assert(_lit_pool_finish <= _lit_pool_end_storage);
 223 }
 224
 225 inline void CDatabase::lit_pool_push_back(int value) {
 226   assert(_lit_pool_finish <= _lit_pool_end_storage);
 227   _lit_pool_finish->val() = value;
 228   ++_lit_pool_finish;
 229 }
 230
 231 inline int CDatabase::lit_pool_size(void) {
 232   return _lit_pool_finish - _lit_pool_start;
 233 }
 234
 235 inline int CDatabase::lit_pool_free_space(void) {
 236   return _lit_pool_end_storage - _lit_pool_finish;
 237 }
 238
 239 inline double CDatabase::lit_pool_utilization(void) {
 240     // minus num_clauses() is because of spacing (i.e. clause indices)
 241   return (double)num_literals() / ((double) (lit_pool_size() - num_clauses())) ;
 242 }
 243
 244 inline CLitPoolElement & CDatabase::lit_pool(int i) {
 245   return _lit_pool_start[i];
 246 }
 247
 248 void CDatabase::compact_lit_pool(void) {
 249   unsigned i, sz;
 250   int new_index = 1;
 251   // first do the compaction for the lit pool
 252   for (i = 1, sz = lit_pool_size(); i < sz;  ++i) {
 253     // begin with 1 because 0 position is always 0
 254     if (!lit_pool(i).is_literal() && !lit_pool(i-1).is_literal()) {
 255       continue;
 256     } else {
 257       lit_pool(new_index) = lit_pool(i);
 258       ++new_index;
 259     }
 260   }
 261   _lit_pool_finish = lit_pool_begin() + new_index;
 262   // update all the pointers to the literals;
 263   // 1. clean up the watched pointers from variables
 264   for (i = 1, sz = variables()->size(); i < sz;  ++i) {
 265     variable(i).watched(0).clear();
 266     variable(i).watched(1).clear();
 267   }
 268   for (i = 1, sz = lit_pool_size(); i < sz;  ++i) {
 269     CLitPoolElement & lit = lit_pool(i);
 270     // 2. reinsert the watched pointers
 271     if (lit.is_literal()) {
 272       if (lit.is_watched()) {
 273          int var_idx = lit.var_index();
 274          int sign = lit.var_sign();
 275          variable(var_idx).watched(sign).push_back(& lit_pool(i));
 276        }
 277     } else {  // lit is not literal
 278     // 3. update the clauses' first literal pointer
 279       int cls_idx = lit.get_clause_index();
 280       clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
 281     }
 282   }
 283   ++_stats.num_compact;
 284 }
 285
 286 bool CDatabase::enlarge_lit_pool(void) {
 287   // will return true if successful, otherwise false.
 288   unsigned i, sz;
 289   // if memory efficiency < 2/3, we do a compaction
 290   if (lit_pool_utilization() < 0.67) {
 291     compact_lit_pool();
 292     return true;
 293   }
 294   // otherwise we have to enlarge it.
 295   // first, check if memory is running out
 296   int current_mem = estimate_mem_usage();
 297   float grow_ratio = 1;
 298   if (current_mem < _params.mem_limit / 4)
 299     grow_ratio = 2;
 300   else if (current_mem < _params.mem_limit /2 )
 301     grow_ratio = 1.5;
 302   else if (current_mem < _params.mem_limit * 0.8)
 303     grow_ratio = 1.2;
 304   if (grow_ratio < 1.2) {
 305     if (lit_pool_utilization() < 0.9) {  // still has some garbage
 306       compact_lit_pool();
 307       return true;
 308     }
 309     else
 310       return false;
 311   }
 312   // second, make room for new lit pool.
 313   CLitPoolElement * old_start = _lit_pool_start;
 314   CLitPoolElement * old_finish = _lit_pool_finish;
 315   int old_size = _lit_pool_end_storage - _lit_pool_start;
 316   int new_size = (int)(old_size * grow_ratio);
 317   _lit_pool_start = (CLitPoolElement *) realloc(_lit_pool_start,
 318                                                 sizeof(CLitPoolElement) *
 319                                                 new_size);
 320   _lit_pool_finish = _lit_pool_start + (old_finish - old_start);
 321   _lit_pool_end_storage = _lit_pool_start + new_size;
 322
 323   // update all the pointers
 324   long long displacement = _lit_pool_start - old_start;
 325   for (i = 0; i < clauses()->size(); ++i) {
 326     if (clause(i).status() != DELETED_CL)
 327       clause(i).first_lit() += displacement;
 328   }
 329   for (i = 0, sz = variables()->size(); i < sz ;  ++i) {
 330     CVariable & v = variable(i);
 331     for (int j = 0; j < 2 ; ++j) {
 332       int k, sz1;
 333       vector<CLitPoolElement *> & watched = v.watched(j);
 334       for (k = 0, sz1 = watched.size(); k < sz1 ; ++k) {
 335         watched[k] += displacement;
 336       }
 337     }
 338   }
 339   ++_stats.num_enlarge;
 340   return true;
 341 }
 342
 343 ClauseIdx CDatabase::get_free_clause_idx(void) {
 344   ClauseIdx new_cl;
 345   new_cl = _clauses.size();
 346   _clauses.resize(new_cl + 1);
 347   clause(new_cl).set_id(_stats.num_added_clauses);
 348   return new_cl;
 349 }
 350
 351 ClauseIdx CDatabase::add_clause(int * lits, int n_lits, int gflag) {
 352   int new_cl;
 353   // a. do we need to enlarge lits pool?
 354   while (lit_pool_free_space() <= n_lits + 1) {
 355     if (enlarge_lit_pool() == false)
 356       return -1;  // mem out, can't enlarge lit pool, because
 357       // ClauseIdx can't be -1, so it shows error.
 358   }
 359   // b. get a free cl index;
 360   new_cl = get_free_clause_idx();
 361   // c. add the clause lits to lits pool
 362   CClause & cl = clause(new_cl);
 363   cl.init(lit_pool_end(), n_lits, gflag);
 364   lit_pool_incr_size(n_lits + 1);
 365   if (n_lits == 2) {
 366     ++variable(lits[0]>>1).two_lits_count(lits[0] & 0x1);
 367     ++variable(lits[1]>>1).two_lits_count(lits[1] & 0x1);
 368   }
 369   for (int i = 0; i < n_lits; ++i) {
 370     int var_idx = lits[i] >> 1;
 371     assert((unsigned)var_idx < variables()->size());
 372     int var_sign = lits[i] & 0x1;
 373     cl.literal(i).set(var_idx, var_sign);
 374     ++variable(var_idx).lits_count(var_sign);
 375 #ifdef KEEP_LIT_CLAUSES
 376     variable(var_idx).lit_clause(var_sign).push_back(new_cl);
 377 #endif
 378   }
 379   // the element after the last one is the spacing element
 380   cl.literal(n_lits).set_clause_index(new_cl);
 381   // d. set the watched pointers
 382   if (cl.num_lits() > 1) {
 383     // add the watched literal. note: watched literal must be the last free var
 384     int max_idx = -1, max_dl = -1;
 385     int i, sz = cl.num_lits();
 386     // set the first watched literal
 387     for (i = 0; i < sz; ++i) {
 388       int v_idx = cl.literal(i).var_index();
 389       int v_sign = cl.literal(i).var_sign();
 390       CVariable & v = variable(v_idx);
 391       if (literal_value(cl.literal(i)) != 0) {
 392         v.watched(v_sign).push_back(&cl.literal(i));
 393         cl.literal(i).set_watch(1);
 394         break;
 395       } else {
 396         if (v.dlevel() > max_dl) {
 397           max_dl = v.dlevel();
 398           max_idx = i;
 399         }
 400       }
 401     }
 402     if (i >= sz) {  // no unassigned literal. so watch literal with max dlevel
 403       int v_idx = cl.literal(max_idx).var_index();
 404       int v_sign = cl.literal(max_idx).var_sign();
 405       variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx));
 406       cl.literal(max_idx).set_watch(1);
 407     }
 408
 409     // set the second watched literal
 410     max_idx = -1;
 411     max_dl = -1;
 412     for (i = sz-1; i >= 0; --i) {
 413       if (cl.literal(i).is_watched())
 414         continue;  // need to watch two different literals
 415       int v_idx = cl.literal(i).var_index();
 416       int v_sign = cl.literal(i).var_sign();
 417       CVariable & v = variable(v_idx);
 418       if (literal_value(cl.literal(i)) != 0) {
 419         v.watched(v_sign).push_back(&cl.literal(i));
 420         cl.literal(i).set_watch(-1);
 421         break;
 422       } else {
 423         if (v.dlevel() > max_dl) {
 424           max_dl = v.dlevel();
 425           max_idx = i;
 426         }
 427       }
 428     }
 429     if (i < 0) {
 430       int v_idx = cl.literal(max_idx).var_index();
 431       int v_sign = cl.literal(max_idx).var_sign();
 432       variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx));
 433       cl.literal(max_idx).set_watch(-1);
 434     }
 435   }
 436   // update some statistics
 437   ++_stats.num_added_clauses;
 438   _stats.num_added_literals += n_lits;
 439   return new_cl;
 440 }
 441
 442 void CDatabase::output_lit_pool_stats(void) {
 443   cout << "Lit_Pool Used " << lit_pool_size() << " Free "
 444        << lit_pool_free_space()
 445        << " Total " << lit_pool_size() + lit_pool_free_space()
 446        << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals()
 447        << " Efficiency " <<  lit_pool_utilization() << endl;
 448 }
 449
 450 void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os) {
 451   os << "CL : " << cl_idx;
 452   CClause & cl = clause(cl_idx);
 453   if (cl.status() == DELETED_CL)
 454     os << "\t\t\t======removed=====";
 455   char value;
 456   for (unsigned i = 0; i < cl.num_lits(); ++i) {
 457     if (literal_value(cl.literal(i)) == 0)
 458       value = '0';
 459     else if (literal_value(cl.literal(i)) == 1)
 460       value = '1';
 461     else
 462       value = 'X';
 463     os << cl.literal(i) << "(" << value << "@"
 464        << variable(cl.literal(i).var_index()).dlevel()<< ")  ";
 465   }
 466   os << endl;
 467 }
 468
 469 void CDatabase::dump(ostream & os) {
 470   unsigned i;
 471   os << "Dump Database: " << endl;
 472   for (i = 0; i < _clauses.size(); ++i)
 473     detail_dump_cl(i);
 474   for (i = 1; i < _variables.size(); ++i)
 475     os << "VID " << i << ":\t" << variable(i);
 476 }