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
CSolver(void)43 CSolver::CSolver(void)
44 {
45 dlevel()=0;
46 _params.time_limit = 3600 * 48; //2 days
47 _params.decision_strategy = 0;
48 _params.preprocess_strategy = 0;
49 _params.allow_clause_deletion = true ;
50 _params.clause_deletion_interval = 5000;
51 _params.max_unrelevance = 20;
52 _params.min_num_clause_lits_for_delete = 100;
53 _params.max_conflict_clause_length = 5000;
54 _params.bubble_init_step = 32;
55
56 _params.randomness = 0;
57 _params.verbosity = 0;
58
59 _params.back_track_complete = true;
60 _params.allow_multiple_conflict = false;
61 _params.allow_multiple_conflict_clause = false;
62
63 _params.allow_restart = true;
64 _params.next_restart_time = 50; //this set the first restart time (in seconds)
65 _params.restart_time_increment = 0;
66 _params.restart_time_incr_incr = 0;
67
68 _params.next_restart_backtrack= 0;
69 _params.restart_backtrack_incr= 40000;
70 _params.restart_backtrack_incr_incr = 100;
71
72 _params.restart_randomness = 0;
73 _params.base_randomness = 0;
74 _params.randomness = 0;
75
76 _stats.is_solver_started = false;
77 _stats.outcome = UNKNOWN;
78 _stats.is_mem_out = false;
79 _stats.start_cpu_time = 0;
80 _stats.finish_cpu_time = 0;
81 _stats.last_cpu_time = 0;
82
83 _stats.start_world_time = 0;
84 _stats.finish_world_time = 0;
85
86 _stats.num_decisions = 0;
87 _stats.num_backtracks = 0;
88 _stats.max_dlevel = 0;
89 _stats.num_implications = 0;
90
91 _num_marked = 0;
92 _dlevel = 0;
93 _stats.total_bubble_move = 0;
94
95 _dlevel_hook = NULL;
96 _decision_hook = NULL;
97 _assignment_hook = NULL;
98 _deduction_hook = NULL;
99 }
100
~CSolver()101 CSolver::~CSolver()
102 {
103 if (_stats.is_solver_started) {
104 for (unsigned i=0; i<variables().size(); ++i)
105 delete _assignment_stack[i];
106 }
107 }
108
run_periodic_functions(void)109 void CSolver::run_periodic_functions(void)
110 {
111 //a. clause deletion
112 if ( _params.allow_clause_deletion &&
113 _stats.num_backtracks % _params.clause_deletion_interval == 0)
114 delete_unrelevant_clauses();
115 //b. restart
116 if (_params.allow_restart && _stats.num_backtracks > _params.next_restart_backtrack) {
117 _params.next_restart_backtrack += _params.restart_backtrack_incr;
118 _params.restart_backtrack_incr += _params.restart_backtrack_incr_incr;
119 float current = current_cpu_time()/1000;
120 if (current > _params.next_restart_time) {
121 if (_params.verbosity > 1) cout << "restart..." << endl;
122 _params.next_restart_time = current + _params.restart_time_increment;
123 _params.restart_time_increment += _params.restart_time_incr_incr;
124 _params.randomness = _params.restart_randomness;
125 restart();
126 }
127 }
128 //c. update var stats for decision
129 if ((_stats.num_decisions % 0xff)==0)
130 update_var_stats();
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
init(void)142 void CSolver::init(void)
143 {
144 CDatabase::init();
145
146 _stats.is_solver_started = true;
147 _stats.start_cpu_time = current_cpu_time();
148 _stats.start_world_time = current_world_time();
149 _stats.num_free_variables = num_variables();
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
add_variables(int new_vars)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) ;
165 if (_stats.is_solver_started) {
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
add_clause(vector<long> & lits,bool addConflicts)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();
195 _unused_clause_idx_queue.pop();
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
281 ++CDatabase::_stats.num_added_clauses;
282 CDatabase::_stats.num_added_literals += n_lits;
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
set_var_value(int v,int value,ClauseIdx ante,int dl)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());
300 CHECK(verify_integrity());
301 CHECK (cout << "Setting\t" << (value>0?"+":"-") << v
302 << " at " << dl << " because " << ante<< endl;);
303 ++_stats.num_implications ;
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
set_var_value_with_current_dl(int v,vector<CLitPoolElement * > & ht_ptrs)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
set_var_value_not_current_dl(int v,vector<CLitPoolElement * > & ht_ptrs)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
unset_var_value(int v)433 void CSolver::unset_var_value(int v)
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
find_max_clause_dlevel(ClauseIdx cl)447 int CSolver::find_max_clause_dlevel(ClauseIdx cl)
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
dump_assignment_stack(ostream & os)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
is_conflict(ClauseIdx cl)479 bool CDatabase::is_conflict(ClauseIdx cl)
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
is_satisfied(ClauseIdx cl)488 bool CDatabase::is_satisfied(ClauseIdx cl)
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
find_unit_literal(ClauseIdx cl)497 int CDatabase::find_unit_literal(ClauseIdx cl)
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
delete_unrelevant_clauses(void)513 void CSolver::delete_unrelevant_clauses(void)
514 {
515 CHECK_FULL (dump());
516 int original_num_deleted = num_deleted_clauses();
517 if (CDatabase::_stats.mem_used_up) {
518 CDatabase::_stats.mem_used_up = false;
519 if (++CDatabase::_stats.mem_used_up_counts < 5) {
520 _params.max_unrelevance = (int) (_params.max_unrelevance * 0.8);
521 if (_params.max_unrelevance < 4)
522 _params.max_unrelevance = 4;
523 _params.min_num_clause_lits_for_delete = (int) (_params.min_num_clause_lits_for_delete* 0.8);
524 if (_params.min_num_clause_lits_for_delete < 10)
525 _params.min_num_clause_lits_for_delete = 10;
526 _params.max_conflict_clause_length = (int) (_params.max_conflict_clause_length*0.8);
527 if (_params.max_conflict_clause_length < 50 )
528 _params.max_conflict_clause_length = 50;
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) {
549 mark_clause_deleted(cl);
550 _unused_clause_idx_queue.push(itr - clauses().begin());
551 CHECK (cout << "Deleting Unrelevant clause: " << cl << endl;);
552 break;
553 }
554 if (cl.num_lits() > _params.max_conflict_clause_length &&
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
557 mark_clause_deleted(cl);
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 //============================================================================================
time_out(void)587 bool CSolver::time_out(void)
588 {
589 if ( (current_cpu_time() - _stats.start_cpu_time)/1000.0 > _params.time_limit )
590 return true;
591 return false;
592 }
593
compare_var_stat(const pair<int,int> & v1,const pair<int,int> & v2)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
update_var_stats(void)601 void CSolver::update_var_stats(void)
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
decide_next_branch(void)617 bool CSolver::decide_next_branch(void)
618 {
619 ++_stats.num_decisions;
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
642 if (--_params.randomness < _params.base_randomness)
643 _params.randomness = _params.base_randomness;
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 }
698 if (dlevel() > _stats.max_dlevel) _stats.max_dlevel = dlevel();
699 CHECK (cout << "**Decision at Level " << dlevel() ;
700 cout <<": " << s_var << "\te.g. " << (s_var&0x1?"-":" ") ;
701 cout <<(s_var>>1) << endl; );
702 queue_implication(s_var, NULL_CLAUSE);
703 return true;
704 }
705
preprocess(bool allowNewClauses)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.
735 queue_implication( i+i+1, NULL_CLAUSE);
736 uni_phased.push_back(-i);
737 }
738 else if (v.lits_count(1) == 0){ //no negative phased lits.
739 queue_implication( i+i, NULL_CLAUSE);
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
755 queue_implication(find_unit_literal(i), i);
756 }
757 }
758
759 if(deduce()==CONFLICT) return CONFLICT;
760 return NO_CONFLICT;
761 }
762
real_solve(void)763 void CSolver::real_solve(void)
764 {
765 while(1) {
766 run_periodic_functions();
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) {
772 _stats.outcome = UNSATISFIABLE;
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 {
790 _stats.outcome = SATISFIABLE;
791 return;
792 }
793 if (time_out()) {
794 _stats.outcome = TIME_OUT;
795 return;
796 }
797 if (_stats.is_mem_out) {
798 _stats.outcome = MEM_OUT;
799 return;
800 }
801 }
802 }
803
solve(bool allowNewClauses)804 int CSolver::solve(bool allowNewClauses)
805 {
806 init();
807 //preprocess
808 if(preprocess(allowNewClauses)==CONFLICT) {
809 _stats.outcome = UNSATISFIABLE;
810 }
811 else { //the real search
812 if (_dlevel_hook) {
813 (*_dlevel_hook)(_dlevel_hook_cookie, 1);
814 }
815 real_solve();
816 }
817 _stats.finish_cpu_time = current_cpu_time();
818 _stats.finish_world_time = current_world_time();
819 return _stats.outcome;
820 }
821
continueCheck()822 int CSolver::continueCheck()
823 {
824 real_solve();
825 _stats.finish_cpu_time = current_cpu_time();
826 _stats.finish_world_time = current_world_time();
827 return _stats.outcome;
828 }
829
back_track(int blevel)830 void CSolver::back_track(int blevel)
831 {
832 CHECK (cout << "Back track to " << blevel <<" ,currently in "<< dlevel() << " level" << endl;);
833 CHECK_FULL (dump());
834 CHECK(verify_integrity());
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;
847 ++_stats.num_backtracks;
848 CHECK_FULL (dump());
849 CHECK(verify_integrity());
850 }
851
deduce(void)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;
863 if (_params.back_track_complete)
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);
870 CHECK(verify_integrity());
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
verify_integrity(void)886 void CSolver::verify_integrity(void)
887 {
888 }
889
mark_vars_at_level(ClauseIdx cl,int var_idx,int dl)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
analyze_conflicts(void)912 int CSolver::analyze_conflicts(void) {
913 return conflict_analysis_zchaff();
914 }
915
conflict_analysis_zchaff(void)916 int CSolver::conflict_analysis_zchaff (void)
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
988 if (_params.back_track_complete) {
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 }
1015 CHECK( dump_assignment_stack(););
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
1036