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