CVC3  2.4.1
xchaff_solver.cpp
Go to the documentation of this file.
1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
2 
3 /*********************************************************************
4  Copyright 2000-2001, Princeton University. All rights reserved.
5  By using this software the USER indicates that he or she has read,
6  understood and will comply with the following:
7 
8  --- Princeton University hereby grants USER nonexclusive permission
9  to use, copy and/or modify this software for internal, noncommercial,
10  research purposes only. Any distribution, including commercial sale
11  or license, of this software, copies of the software, its associated
12  documentation and/or modifications of either is strictly prohibited
13  without the prior consent of Princeton University. Title to copyright
14  to this software and its associated documentation shall at all times
15  remain with Princeton University. Appropriate copyright notice shall
16  be placed on all software copies, and a complete copy of this notice
17  shall be included in all copies of the associated documentation.
18  No right is granted to use in advertising, publicity or otherwise
19  any trademark, service mark, or the name of Princeton University.
20 
21 
22  --- This software and any associated documentation is provided "as is"
23 
24  PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
25  OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
26  PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
27  ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
28  TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
29 
30  Princeton University shall not be liable under any circumstances for
31  any direct, indirect, special, incidental, or consequential damages
32  with respect to any claim by USER or any third party on account of
33  or arising from the use, or inability to use, this software or its
34  associated documentation, even if Princeton University has been advised
35  of the possibility of those damages.
36 *********************************************************************/
37 
38 
39 #include "xchaff_solver.h"
40 #include <algorithm>
41 
42 
44 {
45  dlevel()=0;
46  _params.time_limit = 3600 * 48; //2 days
55 
56  _params.randomness = 0;
57  _params.verbosity = 0;
58 
62 
63  _params.allow_restart = true;
64  _params.next_restart_time = 50; //this set the first restart time (in seconds)
67 
71 
74  _params.randomness = 0;
75 
76  _stats.is_solver_started = false;
78  _stats.is_mem_out = false;
81  _stats.last_cpu_time = 0;
82 
85 
88  _stats.max_dlevel = 0;
90 
91  _num_marked = 0;
92  _dlevel = 0;
94 
95  _dlevel_hook = NULL;
96  _decision_hook = NULL;
97  _assignment_hook = NULL;
98  _deduction_hook = NULL;
99 }
100 
102 {
104  for (unsigned i=0; i<variables().size(); ++i)
105  delete _assignment_stack[i];
106  }
107 }
108 
110 {
111  //a. clause deletion
115  //b. restart
119  float current = current_cpu_time()/1000;
120  if (current > _params.next_restart_time) {
121  if (_params.verbosity > 1) cout << "restart..." << endl;
125  restart();
126  }
127  }
128  //c. update var stats for decision
129  if ((_stats.num_decisions % 0xff)==0)
131  //d. run hook functions
132  for (unsigned i=0; i< _hooks.size(); ++i) {
133  pair<int,pair<HookFunPtrT, int> > & hook = _hooks[i];
134  if (_stats.num_decisions >= hook.first) {
135  hook.first += hook.second.second;
136  hook.second.first((void *) this);
137  }
138  }
139 }
140 
141 
142 void CSolver::init(void)
143 {
144  CDatabase::init();
145 
146  _stats.is_solver_started = true;
150  for (unsigned i=0; i<variables().size(); ++i)
151  _assignment_stack.push_back(new vector<int>);
152 
153  _var_order.resize( num_variables());
154  _last_var_lits_count[0].resize(variables().size());
155  _last_var_lits_count[1].resize(variables().size());
156  CHECK(dump());
157 }
158 
159 
160 int CSolver::add_variables(int new_vars)
161 {
162  int old_num_vars = variables().size();
163  int num_vars = old_num_vars + new_vars;
164  variables().resize(num_vars) ;
166  _stats.num_free_variables += new_vars;
167 
168  for (int i=old_num_vars; i<num_vars; ++i) {
169  _assignment_stack.push_back(new vector<int>);
170  _var_order.push_back(pair<int, int>(i,0));
171  }
172  _last_var_lits_count[0].resize(num_vars);
173  _last_var_lits_count[1].resize(num_vars);
174  }
175  return old_num_vars;
176 }
177 
178 
179 ClauseIdx CSolver::add_clause(vector<long>& lits, bool addConflicts) {
180  int new_cl;
181  int n_lits = lits.size();
182  //a. do we need to enlarge lits pool?
183  while (lit_pool_free_space() <= n_lits + 1) {
184  if (enlarge_lit_pool()==false)
185  return -1; //mem out, can't enlarge lit pool, because
186  //ClauseIdx can't be -1, so it shows error.
187  }
188  //b. get a free cl index;
189  if (_unused_clause_idx_queue.empty()) {
190  new_cl = _clauses.size();
191  _clauses.resize(new_cl + 1);
192  }
193  else {
194  new_cl = _unused_clause_idx_queue.front();
196  }
197  //c. add the clause lits to lits pool
198  clause(new_cl).init(lit_pool_end(), n_lits);
199 
200  //I want to verify added clauses are either all free or all 0
201  bool satisfied = false, is_unit = false, is_conflict = false;
202  int num_unknown = 0;
203  for (int i=0; i< n_lits; ++i){
204  int var_idx = lits[i]>>1;
205  if ((unsigned)var_idx >= variables().size()) {
206  assert(false);
207  }
208  int var_sign = lits[i]&0x1;
209  lit_pool_push_back( ((var_idx<<1) + var_sign) << 2);
210  ++variable(var_idx).lits_count(var_sign);
211  int lit_value = literal_value(clause(new_cl).literal(i));
212 
213  if (lit_value == 1) {
214  satisfied = true;
215  }
216  else if (lit_value != 0) {
217  ++num_unknown;
218  }
219  }
220  is_conflict = !satisfied && (num_unknown == 0);
221  is_unit = !satisfied && (num_unknown == 1);
222  assert(_stats.is_solver_started || num_unknown == n_lits);
223  lit_pool_push_back(-new_cl); //push in the clause idx in the end
224  //d. set the head/tail pointers
225  if (clause(new_cl).num_lits() > 1) {
226  //add the ht. note: ht must be the last free var
227  int max_idx = -1, max_dl = -1;
228  CClause & cl = clause(new_cl);
229  int i, sz = cl.num_lits();
230  int other_ht_idx;
231  for (i=0; i< sz; ++i) {
232  int v_idx = cl.literals()[i].var_index();
233  if (variable(v_idx).value()==UNKNOWN) {
234  int v_sign = cl.literals()[i].var_sign();
235  variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[i]);
236  cl.literals()[i].set_ht(1);
237  other_ht_idx = i;
238  break;
239  }
240  else {
241  if (variable(v_idx).dlevel() > max_dl) {
242  max_dl = variable(v_idx).dlevel();
243  max_idx = i;
244  }
245  }
246  }
247  if (i >= sz) {
248  //no unknown literals. so use the max dl literal
249  int v_idx = cl.literals()[max_idx].var_index();
250  int v_sign = cl.literals()[max_idx].var_sign();
251  variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[max_idx]);
252  cl.literals()[max_idx].set_ht(1);
253  other_ht_idx = max_idx;
254  }
255  max_idx = -1; max_dl = -1;
256  for (i=sz-1; i>=0; --i) {
257  if (i==other_ht_idx ) continue;
258  int v_idx = cl.literals()[i].var_index();
259  if (variable(v_idx).value()==UNKNOWN) {
260  int v_sign = cl.literals()[i].var_sign();
261  variable(v_idx).ht_ptr(v_sign).push_back( & cl.literals()[i]);
262  cl.literals()[i].set_ht(-1);
263  break;
264  }
265  else {
266  if (variable(v_idx).dlevel() > max_dl) {
267  max_dl = variable(v_idx).dlevel();
268  max_idx = i;
269  }
270  }
271  }
272  if (i < 0) {
273  int v_idx = cl.literals()[max_idx].var_index();
274  int v_sign = cl.literals()[max_idx].var_sign();
275  CLitPoolElement * lit_ptr = & cl.literals()[max_idx];
276  variable(v_idx).ht_ptr(v_sign).push_back(lit_ptr);
277  cl.literals()[max_idx].set_ht(-1);
278  }
279  }
280  //update some statistics
283  if (is_unit && _stats.is_solver_started) {
284  if (n_lits == 1) _addedUnitClauses.push_back(new_cl);
285  int lit = find_unit_literal(new_cl);
286  assert(lit);
287  queue_implication(lit, new_cl);
288  }
289  else if (addConflicts && is_conflict) {
290  _conflicts.push_back(new_cl);
291  }
292  return new_cl;
293 }
294 
295 
296 void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl)
297 {
298  assert (value == 0 || value == 1);
299  CHECK_FULL(dump());
301  CHECK (cout << "Setting\t" << (value>0?"+":"-") << v
302  << " at " << dl << " because " << ante<< endl;);
304  --num_free_variables();
305  if (_assignment_hook) {
306  (*_assignment_hook)(_assignment_hook_cookie, v, value);
307  }
308  CVariable & var = _variables[v];
309  assert (var.value() == UNKNOWN);
310  var.dlevel() = dl;
311  var.value() = value;
312  var.set_antecedence(ante);
313  vector<CLitPoolElement *> & ht_ptrs = var.ht_ptr(value);
314  if (dl == dlevel())
315  set_var_value_with_current_dl(v, ht_ptrs);
316  else
317  set_var_value_not_current_dl(v, ht_ptrs);
318 }
319 
320 
321 void CSolver::set_var_value_with_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
322 {
323  ClauseIdx cl_idx;
324  CLitPoolElement * ht_ptr, * other_ht_ptr = NULL, * ptr;
325  int dir;
326  for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); itr != ht_ptrs.end(); ++itr) {
327  ht_ptr = *itr;
328  dir = ht_ptr->direction();
329  ptr = ht_ptr;
330  while(1) {
331  ptr += dir;
332  if (ptr->val() <= 0) {
333  if (dir == 1)
334  cl_idx = - ptr->val();
335  if (dir == ht_ptr->direction()) {
336  ptr = ht_ptr;
337  dir = -dir;
338  continue;
339  }
340  int the_value = literal_value (*other_ht_ptr);
341  if (the_value == 0) //a conflict
342  _conflicts.push_back(cl_idx);
343  else if ( the_value != 1) //e.g. unknown
344  queue_implication (other_ht_ptr->s_var(), cl_idx);
345  break;
346  }
347  if (ptr->is_ht()) {
348  other_ht_ptr = ptr;
349  continue;
350  }
351  if (literal_value(*ptr) == 0)
352  continue;
353  //now it's value is either 1 or unknown
354  int v1 = ptr->var_index();
355  int sign = ptr->var_sign();
356  variable(v1).ht_ptr(sign).push_back(ptr);
357  ht_ptr->unset_ht();
358  ptr->set_ht(dir);
359 
360  *itr = ht_ptrs.back();
361  ht_ptrs.pop_back();
362  --itr;
363  break;
364  }
365  }
366 }
367 
368 void CSolver::set_var_value_not_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
369 {
370  ClauseIdx cl_idx;
371  CLitPoolElement * ht_ptr, * other_ht_ptr = NULL, * ptr, * max_ptr = NULL;
372  int dir,max_dl;
373 
374  for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin();
375  itr != ht_ptrs.end(); ++itr) {
376  max_dl = -1;
377  ht_ptr = *itr;
378  dir = ht_ptr->direction();
379  ptr = ht_ptr;
380  while(1) {
381  ptr += dir;
382  if (ptr->val() <= 0) {
383  if (dir == 1)
384  cl_idx = - ptr->val();
385  if (dir == ht_ptr->direction()) {
386  ptr = ht_ptr;
387  dir = -dir;
388  continue;
389  }
390  if (variable(ht_ptr->var_index()).dlevel() < max_dl) {
391  int v1 = max_ptr->var_index();
392  int sign = max_ptr->var_sign();
393  variable(v1).ht_ptr(sign).push_back(max_ptr);
394  ht_ptr->unset_ht();
395  max_ptr->set_ht(dir);
396  *itr = ht_ptrs.back();
397  ht_ptrs.pop_back();
398  --itr;
399  }
400  int the_value = literal_value (*other_ht_ptr);
401  if (the_value == 0) //a conflict
402  _conflicts.push_back(cl_idx);
403  else if ( the_value != 1) //e.g. unknown
404  queue_implication (other_ht_ptr->s_var(), cl_idx);
405  break;
406  }
407  if (ptr->is_ht()) {
408  other_ht_ptr = ptr;
409  continue;
410  }
411  if (literal_value(*ptr) == 0) {
412  if (variable(ptr->var_index()).dlevel() > max_dl) {
413  max_dl = variable(ptr->var_index()).dlevel();
414  max_ptr = ptr;
415  }
416  continue;
417  }
418  //now it's value is either 1 or unknown
419  int v1 = ptr->var_index();
420  int sign = ptr->var_sign();
421  variable(v1).ht_ptr(sign).push_back(ptr);
422  ht_ptr->unset_ht();
423  ptr->set_ht(dir);
424 
425  *itr = ht_ptrs.back();
426  ht_ptrs.pop_back();
427  --itr;
428  break;
429  }
430  }
431 }
432 
434 {
435  CHECK(cout <<"Unset var " << (variable(v).value()?"+":"-") << v << endl;);
436  CVariable & var = variable(v);
437  if (var.var_score_pos() < _max_score_pos)
438  _max_score_pos = var.var_score_pos();
439  var.value() = UNKNOWN;
440  var.set_antecedence(NULL_CLAUSE);
441  var.dlevel() = -1;
442  if (_assignment_hook) {
443  (*_assignment_hook)(_assignment_hook_cookie, v, -1);
444  }
445 }
446 
448 {
449 //if cl has single literal, then dlevel should be 0
450  int max_level = 0;
451  if (cl == NULL_CLAUSE || cl == FLIPPED)
452  return dlevel();
453  for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) {
454  int var_idx =((clause(cl).literals())[i]).var_index();
455  if (_variables[var_idx].value() != UNKNOWN) {
456  if (max_level < _variables[var_idx].dlevel())
457  max_level = _variables[var_idx].dlevel();
458  }
459  }
460  return max_level;
461 }
462 
463 void CSolver::dump_assignment_stack(ostream & os) {
464  cout << "Assignment Stack: ";
465  for (int i=0; i<= dlevel(); ++i) {
466  if ((*_assignment_stack[i]).size() > 0)
467  if (variable( (*_assignment_stack[i])[0]>>1).get_antecedence()==FLIPPED)
468  cout << "*" ;
469  cout << "(" <<i << ":";
470  for (unsigned j=0; j<(*_assignment_stack[i]).size(); ++j )
471  cout << ((*_assignment_stack[i])[j]&0x1?"-":"+")
472  << ((*_assignment_stack[i])[j] >> 1) << " ";
473  cout << ") " << endl;
474  }
475  cout << endl;
476 }
477 
478 
480 {
481  CLitPoolElement * lits = clause(cl).literals();
482  for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i)
483  if (literal_value(lits[i]) != 0)
484  return false;
485  return true;
486 }
487 
489 {
490  CLitPoolElement * lits = clause(cl).literals();
491  for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i)
492  if (literal_value(lits[i]) == 1)
493  return true;
494  return false;
495 }
496 
498 {
499 //if it's not unit, return 0.
500  int unassigned = 0;
501  for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) {
502  int var_idx =((clause(cl).literals())[i]).var_index();
503  if (_variables[var_idx].value() == UNKNOWN) {
504  if (unassigned == 0)
505  unassigned = clause(cl).literals()[i].s_var();
506  else //more than one unassigned
507  return 0;
508  }
509  }
510  return unassigned;
511 }
512 
514 {
515  CHECK_FULL (dump());
516  int original_num_deleted = num_deleted_clauses();
517  if (CDatabase::_stats.mem_used_up) {
519  if (++CDatabase::_stats.mem_used_up_counts < 5) {
521  if (_params.max_unrelevance < 4)
529  CHECK(
530  cout << "Forced to reduce unrelevance in clause deletion. " << endl;
531  cout <<"MaxUnrel: " << _params.max_unrelevance
532  << " MinLenDel: " << _params.min_num_clause_lits_for_delete
533  << " MaxLenCL : " << _params.max_conflict_clause_length << endl;
534  );
535  }
536  }
537  //first find out the clause to delete and mark them
538  for (vector<CClause>::iterator itr = clauses().begin() + init_num_clauses();
539  itr != clauses().end(); ++itr) {
540  CClause & cl = * itr;
541  if (!cl.in_use() || cl.num_lits() < _params.min_num_clause_lits_for_delete ) continue;
542  int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
543  for (int i=0; i< cl.num_lits(); ++i) {
544  int lit_value = literal_value (cl.literal(i));
545  if (lit_value == 0 ) ++val_0_lits;
546  else if (lit_value == 1) ++val_1_lits;
547  else ++unknown_lits;
548  if (unknown_lits + val_1_lits > _params.max_unrelevance) {
550  _unused_clause_idx_queue.push(itr - clauses().begin());
551  CHECK (cout << "Deleting Unrelevant clause: " << cl << endl;);
552  break;
553  }
555  (unknown_lits+val_1_lits > 1) ) { //to make sure it's not generating an implication
556  //and it's not an antecedence for other var assignment
558  CHECK (cout << "Deleting too large clause: " << cl << endl;);
559  _unused_clause_idx_queue.push(itr - clauses().begin());
560  break;
561  }
562  }
563  }
564  //now delete the index from variables
565  if (original_num_deleted == num_deleted_clauses())
566  return ; //didn't delete anything
567  for (vector<CVariable>::iterator itr = variables().begin();
568  itr != variables().end(); ++ itr) {
569  for (int i=0; i<2; ++i) { //for each phase
570  //delete the h_t index from the vars
571  vector<CLitPoolElement *> & ht_ptr = (*itr).ht_ptr(i);
572  for (vector<CLitPoolElement *>::iterator my_itr = ht_ptr.begin();
573  my_itr != ht_ptr.end(); ++my_itr) {
574  if ( (*my_itr)->val() <= 0) {
575  *my_itr = ht_ptr.back();
576  ht_ptr.pop_back();
577  --my_itr;
578  }
579  }
580  }
581  }
582  CHECK(cout << "Deleting " << num_deleted_clauses() - original_num_deleted << " Clause ";
583  cout << " and " << num_deleted_literals() - original_del_lits << " Literals " << endl;);
584  CHECK_FULL (dump());
585 }
586 //============================================================================================
587 bool CSolver::time_out(void)
588 {
590  return true;
591  return false;
592 }
593 
594 inline bool compare_var_stat(const pair<int, int> & v1,
595  const pair<int, int> & v2)
596 {
597  if (v1.second > v2.second) return true;
598  return false;
599 }
600 
602 {
603  for(unsigned i=1; i< variables().size(); ++i) {
604  CVariable & var = variable(i);
605  var.score(0) = var.score(0)/2 + var.lits_count(0) - _last_var_lits_count[0][i];
606  var.score(1) = var.score(1)/2 + var.lits_count(1) - _last_var_lits_count[1][i];
607  _last_var_lits_count[0][i] = var.lits_count(0);
608  _last_var_lits_count[1][i] = var.lits_count(1);
609  _var_order[i-1] = pair<int, int>(i, var.score());
610  }
611  ::stable_sort(_var_order.begin(), _var_order.end(), compare_var_stat);
612  for (unsigned i=0; i<_var_order.size(); ++i)
613  variable(_var_order[i].first).var_score_pos() = i;
614  _max_score_pos = 0;
615 }
616 
618 {
620  if (!_implication_queue.empty()) {
621  //some hook function did a decision, so skip my own decision making.
622  //if the front of implication queue is 0, that means it's finished
623  //because var index start from 1, so 2 *vid + sign won't be 0.
624  //else it's a valid decision.
625  _max_score_pos = 0; //reset the max_score_position.
626  return _implication_queue.front().first;
627  }
628 
629  int s_var = 0, s_var2;
630  bool done = false;
631 
632  unsigned i, var_idx, sign;
633  CVariable * ptr;
634 
635  for (i=_max_score_pos; i<_var_order.size(); ++i) {
636  var_idx = _var_order[i].first;
637  ptr = &(variables()[var_idx]);
638  if (ptr->value()==UNKNOWN) {
639  //move th max score position pointer
640  _max_score_pos = i;
641  //make some randomness happen
644 
645  int randomness = _params.randomness;
646  if (randomness >= num_free_variables())
647  randomness = num_free_variables() - 1;
648  int skip =random()%(1+randomness);
649  int index = i;
650  while (skip > 0) {
651  ++index;
652  var_idx = _var_order[index].first;
653  ptr = &(variables()[var_idx]);
654  if (ptr->value()==UNKNOWN)
655  --skip;
656  }
657  assert (ptr->value() == UNKNOWN);
658  sign = ptr->score(0) > ptr->score(1) ? 0 : 1;
659  s_var = var_idx + var_idx + sign;
660  break;
661  }
662  }
663  if (s_var < 2) done = true;
664 
665  if (_decision_hook) {
666  decide:
667  s_var2 = (*_decision_hook)(_decision_hook_cookie, &done);
668  if (done) {
669  if (s_var2 == -1) {
670  // No more decisions
671  return false;
672  }
673  else {
674  // check for more work
675  if (!_implication_queue.empty() ||
676  _conflicts.size() != 0)
677  return false;
678  else goto decide;
679  }
680  }
681  else {
682  if (s_var2 == -1) {
683  // use SAT choice
684  }
685  else {
686  // use decision
687  s_var = s_var2;
688  }
689  }
690  }
691 
692  if (s_var<2) //no more free vars, solution found, quit
693  return false;
694  ++dlevel();
695  if (_dlevel_hook) {
696  (*_dlevel_hook)(_dlevel_hook_cookie, 1);
697  }
699  CHECK (cout << "**Decision at Level " << dlevel() ;
700  cout <<": " << s_var << "\te.g. " << (s_var&0x1?"-":" ") ;
701  cout <<(s_var>>1) << endl; );
703  return true;
704 }
705 
706 int CSolver::preprocess(bool allowNewClauses)
707 {
708  //1. detect all the unused variables
709  if (!allowNewClauses) {
710  vector<int> un_used;
711  for (int i=1, sz=variables().size(); i<sz; ++i) {
712  CVariable & v = variable(i);
713  if (v.lits_count(0) == 0 && v.lits_count(1) == 0) {
714  un_used.push_back(i);
715  v.value() = 1;
716  v.dlevel() = -1;
717  }
718  }
719  num_free_variables() -= un_used.size();
720  if (_params.verbosity>1 && un_used.size() > 0) {
721  cout << un_used.size()<< " Variables are defined but not used " << endl;
722  if (_params.verbosity > 2) {
723  for (unsigned i=0; i< un_used.size(); ++i)
724  cout << un_used[i] << " ";
725  cout << endl;
726  }
727  }
728  //2. detect all variables with only one phase occuring
729  vector<int> uni_phased;
730  for (int i=1, sz=variables().size(); i<sz; ++i) {
731  CVariable & v = variable(i);
732  if (v.value() != UNKNOWN)
733  continue;
734  if (v.lits_count(0) == 0){ //no positive phased lits.
736  uni_phased.push_back(-i);
737  }
738  else if (v.lits_count(1) == 0){ //no negative phased lits.
740  uni_phased.push_back(i);
741  }
742  }
743  if (_params.verbosity>1 && uni_phased.size() > 0) {
744  cout << uni_phased.size()<< " Variables only appear in one phase." << endl;
745  if (_params.verbosity > 2) {
746  for (unsigned i=0; i< uni_phased.size(); ++i)
747  cout << uni_phased[i] << " ";
748  cout <<endl;
749  }
750  }
751  }
752  //3. detect all the unit clauses
753  for (ClauseIdx i=0, sz=clauses().size(); i<sz; ++i) {
754  if (clause(i).num_lits() == 1){ //unit clause
756  }
757  }
758 
759  if(deduce()==CONFLICT) return CONFLICT;
760  return NO_CONFLICT;
761 }
762 
764 {
765  while(1) {
767  if (decide_next_branch() || !_implication_queue.empty() ||
768  _conflicts.size() != 0) {
769  while (deduce()==CONFLICT) {
770  int blevel = analyze_conflicts();
771  if (blevel <= 0) {
773  return;
774  }
775  else if (_addedUnitClauses.size()) {
776  // reassert added unit clauses
777  unsigned idx = _addedUnitClauses.size()-1;
778  ClauseIdx cl = _addedUnitClauses.back();
779  int lit = find_unit_literal(cl);
780  while (lit != 0) {
781  queue_implication(lit, cl);
782  if (idx == 0) break;
783  cl = _addedUnitClauses[--idx];
784  lit = find_unit_literal(cl);
785  }
786  }
787  }
788  }
789  else {
791  return;
792  }
793  if (time_out()) {
795  return;
796  }
797  if (_stats.is_mem_out) {
799  return;
800  }
801  }
802 }
803 
804 int CSolver::solve(bool allowNewClauses)
805 {
806  init();
807  //preprocess
808  if(preprocess(allowNewClauses)==CONFLICT) {
810  }
811  else { //the real search
812  if (_dlevel_hook) {
813  (*_dlevel_hook)(_dlevel_hook_cookie, 1);
814  }
815  real_solve();
816  }
819  return _stats.outcome;
820 }
821 
823 {
824  real_solve();
827  return _stats.outcome;
828 }
829 
830 void CSolver::back_track(int blevel)
831 {
832  CHECK (cout << "Back track to " << blevel <<" ,currently in "<< dlevel() << " level" << endl;);
833  CHECK_FULL (dump());
835  assert(blevel <= dlevel());
836  for (int i=dlevel(); i>= blevel; --i) {
837  vector<int> & assignments = *_assignment_stack[i];
838  for (int j=assignments.size()-1 ; j>=0; --j)
839  unset_var_value(assignments[j]>>1);
840  num_free_variables() += assignments.size();
841  assignments.clear();
842  if (_dlevel_hook) {
843  (*_dlevel_hook)(_dlevel_hook_cookie, -1);
844  }
845  }
846  dlevel() = blevel - 1;
848  CHECK_FULL (dump());
850 }
851 
852 int CSolver::deduce(void)
853 {
854 restart:
855  while (!_implication_queue.empty() && _conflicts.size()==0) {
856  int literal = _implication_queue.front().first;
857  int variable_index = literal>>1;
858  ClauseIdx cl = _implication_queue.front().second;
859  _implication_queue.pop();
860  CVariable * the_var = &(variables()[variable_index]);
861  if ( the_var->value() == UNKNOWN) { // an implication
862  int dl;
864  dl = dlevel();
865  else
866  dl = find_max_clause_dlevel(cl);
867  set_var_value(variable_index, !(literal&0x1), cl, dl);
868  the_var = &(variables()[variable_index]);
869  _assignment_stack[dl]->push_back(literal);
871  }
872  else if (the_var->value() == (literal&0x1) ) { //a conflict
873  //note: literal & 0x1 == 1 means the literal is in negative phase
874  _conflicts.push_back(cl);
875  }
876  }
877  if (!_conflicts.size() && _deduction_hook) {
878  (*_deduction_hook)(_deduction_hook_cookie);
879  if (!_implication_queue.empty()) goto restart;
880  }
881  while(!_implication_queue.empty()) _implication_queue.pop();
882  return (_conflicts.size()?CONFLICT:NO_CONFLICT);
883 }
884 
885 
887 {
888 }
889 
890 void CSolver::mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
891 {
892  for (CLitPoolElement * itr = clause(cl).literals(); (*itr).val() > 0 ; ++ itr) {
893  int v = (*itr).var_index();
894  if (v == var_idx)
895  continue;
896  else if (variable(v).dlevel() == dl) {
897  if (!variable(v).is_marked()) {
898  variable(v).set_marked();
899  ++ _num_marked;
900  }
901  }
902  else {
903  assert (variable(v).dlevel() < dl);
904  if (variable(v).in_new_cl() == -1){ //it's not in the new cl
905  variable(v).set_in_new_cl((*itr).var_sign());
906  _conflict_lits.push_back((*itr).s_var());
907  }
908  }
909  }
910 }
911 
913  return conflict_analysis_zchaff();
914 }
915 
917 {
918  assert (_conflicts.size());
919  assert (_implication_queue.empty());
920  assert (_num_marked == 0);
921  int back_level = 0;
922  ClauseIdx conflict_cl;
923  vector<ClauseIdx> added_conflict_clauses;
924  for (int i=0, sz=_conflicts.size(); i<sz; ++i) {
925  ClauseIdx cl = _conflicts[i];
926 
927  if (!is_conflict(cl)) continue;
928 
929  back_level = 0; // reset it
930  while (_conflict_lits.size()) {
931  CVariable & var = variable(_conflict_lits.back() >> 1);
932  _conflict_lits.pop_back();
933  assert (var.in_new_cl() != -1);
934  var.set_in_new_cl(-1);
935  }
936  int max_dlevel = find_max_clause_dlevel(cl); // find the max level, which is the back track level
937  bool first_time = true; //its the beginning
938  bool prev_is_uip = false;
939  mark_vars_at_level (cl, -1 /*var*/, max_dlevel);
940 
941  vector <int> & assignments = *_assignment_stack[max_dlevel];
942  for (int j = assignments.size() - 1; j >= 0; --j ) { //now add conflict lits, and unassign vars
943  int assigned = assignments[j];
944  if (variable(assigned>>1).is_marked()) {
945  variable(assigned>>1).clear_marked();
946  -- _num_marked;
947  ClauseIdx ante_cl = variables()[assigned>>1].get_antecedence();
948 
949  if ( (_num_marked == 0 &&
950  (!first_time) &&
951  (prev_is_uip == false))
952  || ante_cl==NULL_CLAUSE) { //conclude add clause
953  assert (variable(assigned>>1).in_new_cl()==-1);
954  _conflict_lits.push_back(assigned^0x1); // add this assignment's reverse, e.g. UIP
955  int conflict_cl = add_clause(_conflict_lits, false);
956  if (conflict_cl < 0 ) {
957  _stats.is_mem_out = true;
958  _conflicts.clear();
959  assert (_implication_queue.empty());
960  return 1;
961  }
962  _conflict_lits.pop_back(); // remove for continue use of _conflict_lits
963  added_conflict_clauses.push_back(conflict_cl);
964 
965  CHECK(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;
966  cout << "**Add Clause " <<conflict_cl<< " : "<<clause(conflict_cl) << endl;
967  );
968 
969  prev_is_uip = true;
970  break; //if do this, only one clause will be added.
971  }
972  else prev_is_uip = false;
973 
974  if ( ante_cl != NULL_CLAUSE )
975  mark_vars_at_level(ante_cl, assigned>>1/*var*/, max_dlevel);
976  else
977  assert (j == 0);
978  first_time = false;
979  }
980  }
981  back_level = max_dlevel;
982  back_track(max_dlevel);
983  }
984  assert (_num_marked == 0);
985  if (back_level==0) //there are nothing to be done
986  return back_level;
987 
989  for (unsigned i=0; i< added_conflict_clauses.size(); ++i) {
990  ClauseIdx cl = added_conflict_clauses[i];
991  if (find_unit_literal(cl)) { //i.e. if it's a unit clause
992  int dl = find_max_clause_dlevel(cl);
993  if (dl < dlevel()) { //thus make sure implied vars are at current dl.
994  back_track(dl+1);
995  }
996  }
997  }
998  }
999  for (int i=0, sz=added_conflict_clauses.size(); i<sz; ++i) {
1000  conflict_cl = added_conflict_clauses[i];
1001  int lit = find_unit_literal(conflict_cl);
1002  if (lit) {
1003  queue_implication(lit, conflict_cl);
1004  }
1005  }
1006 
1007  _conflicts.clear();
1008 
1009  while (_conflict_lits.size()) {
1010  CVariable & var = variable(_conflict_lits.back() >> 1);
1011  _conflict_lits.pop_back();
1012  assert (var.in_new_cl() != -1);
1013  var.set_in_new_cl(-1);
1014  }
1016  CHECK(cout << "Conflict Analasis: conflict at level: " << back_level;
1017  cout << " Assertion Clause is " << conflict_cl<< endl; );
1018  return back_level;
1019 }
1020 
1021 
1022 
1023 
1024 
1025 
1026 
1027 
1028 
1029 
1030 
1031 
1032 
1033 
1034 
1035 
float restart_time_incr_incr
Definition: xchaff_solver.h:96
int find_unit_literal(ClauseIdx cl)
int literal_value(CLitPoolElement l)
Definition: xchaff_dbase.h:239
short & value(void)
Definition: xchaff_base.h:264
void set_antecedence(ClauseIdx ante)
Definition: xchaff_base.h:293
int _max_score_pos
int lit_pool_free_space(void)
Definition: xchaff_dbase.h:158
void set_var_value_not_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
void mark_clause_deleted(CClause &cl)
Definition: xchaff_dbase.h:221
void delete_unrelevant_clauses(void)
int & score(int i)
Definition: xchaff_base.h:249
void verify_integrity(void)
int min_num_clause_lits_for_delete
Definition: xchaff_solver.h:86
vector< CClause > _clauses
Definition: xchaff_dbase.h:101
vector< CClause > & clauses(void)
Definition: xchaff_dbase.h:120
int & num_lits(void)
Definition: xchaff_base.h:189
void(* _assignment_hook)(void *, int, int)
int analyze_conflicts(void)
#define FLIPPED
Definition: xchaff_base.h:52
void(* _deduction_hook)(void *)
CSolverStats _stats
void unset_var_value(int var)
int & dlevel()
vector< ClauseIdx > _addedUnitClauses
bool is_conflict(ClauseIdx cl)
int & lits_count(int i)
Definition: xchaff_base.h:276
void set_ht(int dir)
Definition: xchaff_base.h:120
int find_max_clause_dlevel(ClauseIdx cl)
void set_in_new_cl(int phase)
Definition: xchaff_base.h:273
void lit_pool_push_back(int value)
Definition: xchaff_dbase.h:150
bool & in_use(void)
Definition: xchaff_base.h:192
CLitPoolElement & literal(int idx)
Definition: xchaff_base.h:195
float restart_time_increment
Definition: xchaff_solver.h:95
void init(void)
vector< CVariable > & variables(void)
Definition: xchaff_dbase.h:117
void back_track(int level)
short & dlevel(void)
Definition: xchaff_base.h:267
void init(CLitPoolElement *head, int num_lits)
Definition: xchaff_base.h:177
void unset_ht(void)
Definition: xchaff_base.h:117
void run_periodic_functions(void)
CSolverParameters _params
#define NULL_CLAUSE
Definition: xchaff_base.h:51
CDatabaseStats _stats
Definition: xchaff_dbase.h:93
int & var_score_pos(void)
Definition: xchaff_base.h:251
queue< ClauseIdx > _unused_clause_idx_queue
Definition: xchaff_dbase.h:102
void * _decision_hook_cookie
CVariable & variable(int idx)
Definition: xchaff_dbase.h:123
int num_free_variables
CLitPoolElement * lit_pool_end(void)
Definition: xchaff_dbase.h:147
vector< CLitPoolElement * > & ht_ptr(int i)
Definition: xchaff_base.h:297
void dump_assignment_stack(ostream &os=cout)
int var_index(void)
Definition: xchaff_base.h:98
int & val(void)
Definition: xchaff_base.h:92
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int(* _decision_hook)(void *, bool *)
int num_added_literals
Definition: xchaff_dbase.h:75
void * _deduction_hook_cookie
int ClauseIdx
Definition: xchaff_base.h:54
bool var_sign(void)
Definition: xchaff_base.h:101
void restart(void)
ClauseIdx get_antecedence(void)
Definition: xchaff_base.h:290
int preprocess(bool allowNewClauses)
void(* _dlevel_hook)(void *, int)
vector< ClauseIdx > _conflicts
void * _assignment_hook_cookie
int s_var(void)
Definition: xchaff_base.h:95
queue< pair< int, ClauseIdx > > _implication_queue
int & num_free_variables()
int & num_deleted_literals()
Definition: xchaff_dbase.h:141
int deduce(void)
CLitPoolElement * literals(void)
Definition: xchaff_base.h:183
void clear_marked(void)
Definition: xchaff_base.h:286
vector< pair< int, int > > _var_order
bool compare_var_stat(const pair< int, int > &v1, const pair< int, int > &v2)
ClauseIdx add_clause(vector< long > &lits, bool addConflicts=true)
bool enlarge_lit_pool(void)
int _num_marked
void dump(ostream &os=cout)
int max_dlevel()
long start_world_time
vector< long > _conflict_lits
int max_conflict_clause_length
Definition: xchaff_solver.h:87
bool decide_next_branch(void)
void real_solve(void)
int restart_backtrack_incr_incr
Definition: xchaff_solver.h:99
bool time_out(void)
#define CHECK_FULL(x)
Definition: xchaff_utils.h:43
void set_var_value_with_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
bool is_solver_started
void mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
vector< pair< int, pair< HookFunPtrT, int > > > _hooks
int direction(void)
Definition: xchaff_base.h:111
bool allow_multiple_conflict_clause
vector< vector< int > * > _assignment_stack
int add_variables(int new_vars)
int & init_num_clauses()
Definition: xchaff_dbase.h:136
long finish_world_time
int conflict_analysis_zchaff(void)
bool is_marked(void)
Definition: xchaff_base.h:280
int current_cpu_time(void)
int current_world_time(void)
long total_bubble_move
int in_new_cl(void)
Definition: xchaff_base.h:270
void * _dlevel_hook_cookie
long finish_cpu_time
void init(void)
Definition: xchaff_dbase.h:112
bool is_satisfied(ClauseIdx cl)
int num_variables(void)
Definition: xchaff_dbase.h:210
#define CHECK(x)
Definition: xchaff_utils.h:42
void set_var_value(int var, int value, ClauseIdx ante, int dl)
void update_var_stats(void)
vector< int > _last_var_lits_count[2]
CClause & clause(ClauseIdx idx)
Definition: xchaff_dbase.h:126
int continueCheck()
int solve(bool allowNewClauses)
vector< CVariable > _variables
Definition: xchaff_dbase.h:100
void queue_implication(int lit, ClauseIdx ante_clause)
int & num_deleted_clauses()
Definition: xchaff_dbase.h:140
void set_marked(void)
Definition: xchaff_base.h:283