projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Bump version
[yosys.git] / libs / minisat / Solver.cc
1 #ifndef __STDC_FORMAT_MACROS
2 #define __STDC_FORMAT_MACROS
3 #endif
4 #ifndef __STDC_LIMIT_MACROS
5 #define __STDC_LIMIT_MACROS
6 #endif
7 /***************************************************************************************[Solver.cc]
8 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
9 Copyright (c) 2007-2010, Niklas Sorensson
10
11 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
12 associated documentation files (the "Software"), to deal in the Software without restriction,
13 including without limitation the rights to use, copy, modify, merge, publish, distribute,
14 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
15 furnished to do so, subject to the following conditions:
16
17 The above copyright notice and this permission notice shall be included in all copies or
18 substantial portions of the Software.
19
20 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
21 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
22 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
23 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
24 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
25 **************************************************************************************************/
26
27 #include <math.h>
28
29 #include "Alg.h"
30 #include "Sort.h"
31 #include "System.h"
32 #include "Solver.h"
33
34 using namespace Minisat;
35
36 //=================================================================================================
37 // Options:
38
39
40 static const char* _cat = "CORE";
41
42 static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false));
43 static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false));
44 static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
45 static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false));
46 static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
47 static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
48 static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false);
49 static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true);
50 static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX));
51 static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
52 static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
53 static IntOption opt_min_learnts_lim (_cat, "min-learnts", "Minimum learnt clause limit", 0, IntRange(0, INT32_MAX));
54
55
56 //=================================================================================================
57 // Constructor/Destructor:
58
59
60 Solver::Solver() :
61
62 // Parameters (user settable):
63 //
64 verbosity (0)
65 , var_decay (opt_var_decay)
66 , clause_decay (opt_clause_decay)
67 , random_var_freq (opt_random_var_freq)
68 , random_seed (opt_random_seed)
69 , luby_restart (opt_luby_restart)
70 , ccmin_mode (opt_ccmin_mode)
71 , phase_saving (opt_phase_saving)
72 , rnd_pol (false)
73 , rnd_init_act (opt_rnd_init_act)
74 , garbage_frac (opt_garbage_frac)
75 , min_learnts_lim (opt_min_learnts_lim)
76 , restart_first (opt_restart_first)
77 , restart_inc (opt_restart_inc)
78
79 // Parameters (the rest):
80 //
81 , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
82
83 // Parameters (experimental):
84 //
85 , learntsize_adjust_start_confl (100)
86 , learntsize_adjust_inc (1.5)
87
88 // Statistics: (formerly in 'SolverStats')
89 //
90 , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
91 , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
92
93 , watches (WatcherDeleted(ca))
94 , order_heap (VarOrderLt(activity))
95 , ok (true)
96 , cla_inc (1)
97 , var_inc (1)
98 , qhead (0)
99 , simpDB_assigns (-1)
100 , simpDB_props (0)
101 , progress_estimate (0)
102 , remove_satisfied (true)
103 , next_var (0)
104
105 // Resource constraints:
106 //
107 , conflict_budget (-1)
108 , propagation_budget (-1)
109 , asynch_interrupt (false)
110 {}
111
112
113 Solver::~Solver()
114 {
115 }
116
117
118 //=================================================================================================
119 // Minor methods:
120
121
122 // Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
123 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
124 //
125 Var Solver::newVar(lbool upol, bool dvar)
126 {
127 Var v;
128 if (free_vars.size() > 0){
129 v = free_vars.last();
130 free_vars.pop();
131 }else
132 v = next_var++;
133
134 watches .init(mkLit(v, false));
135 watches .init(mkLit(v, true ));
136 assigns .insert(v, l_Undef);
137 vardata .insert(v, mkVarData(CRef_Undef, 0));
138 activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);
139 seen .insert(v, 0);
140 polarity .insert(v, true);
141 user_pol .insert(v, upol);
142 decision .reserve(v);
143 trail .capacity(v+1);
144 setDecisionVar(v, dvar);
145 return v;
146 }
147
148
149 // Note: at the moment, only unassigned variable will be released (this is to avoid duplicate
150 // releases of the same variable).
151 void Solver::releaseVar(Lit l)
152 {
153 if (value(l) == l_Undef){
154 addClause(l);
155 released_vars.push(var(l));
156 }
157 }
158
159
160 bool Solver::addClause_(vec<Lit>& ps)
161 {
162 assert(decisionLevel() == 0);
163 if (!ok) return false;
164
165 // Check if clause is satisfied and remove false/duplicate literals:
166 sort(ps);
167 Lit p; int i, j;
168 for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
169 if (value(ps[i]) == l_True || ps[i] == ~p)
170 return true;
171 else if (value(ps[i]) != l_False && ps[i] != p)
172 ps[j++] = p = ps[i];
173 ps.shrink(i - j);
174
175 if (ps.size() == 0)
176 return ok = false;
177 else if (ps.size() == 1){
178 uncheckedEnqueue(ps[0]);
179 return ok = (propagate() == CRef_Undef);
180 }else{
181 CRef cr = ca.alloc(ps, false);
182 clauses.push(cr);
183 attachClause(cr);
184 }
185
186 return true;
187 }
188
189
190 void Solver::attachClause(CRef cr){
191 const Clause& c = ca[cr];
192 assert(c.size() > 1);
193 watches[~c[0]].push(Watcher(cr, c[1]));
194 watches[~c[1]].push(Watcher(cr, c[0]));
195 if (c.learnt()) num_learnts++, learnts_literals += c.size();
196 else num_clauses++, clauses_literals += c.size();
197 }
198
199
200 void Solver::detachClause(CRef cr, bool strict){
201 const Clause& c = ca[cr];
202 assert(c.size() > 1);
203
204 // Strict or lazy detaching:
205 if (strict){
206 remove(watches[~c[0]], Watcher(cr, c[1]));
207 remove(watches[~c[1]], Watcher(cr, c[0]));
208 }else{
209 watches.smudge(~c[0]);
210 watches.smudge(~c[1]);
211 }
212
213 if (c.learnt()) num_learnts--, learnts_literals -= c.size();
214 else num_clauses--, clauses_literals -= c.size();
215 }
216
217
218 void Solver::removeClause(CRef cr) {
219 Clause& c = ca[cr];
220 detachClause(cr);
221 // Don't leave pointers to free'd memory!
222 if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
223 c.mark(1);
224 ca.free(cr);
225 }
226
227
228 bool Solver::satisfied(const Clause& c) const {
229 for (int i = 0; i < c.size(); i++)
230 if (value(c[i]) == l_True)
231 return true;
232 return false; }
233
234
235 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
236 //
237 void Solver::cancelUntil(int level) {
238 if (decisionLevel() > level){
239 for (int c = trail.size()-1; c >= trail_lim[level]; c--){
240 Var x = var(trail[c]);
241 assigns [x] = l_Undef;
242 if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))
243 polarity[x] = sign(trail[c]);
244 insertVarOrder(x); }
245 qhead = trail_lim[level];
246 trail.shrink(trail.size() - trail_lim[level]);
247 trail_lim.shrink(trail_lim.size() - level);
248 } }
249
250
251 //=================================================================================================
252 // Major methods:
253
254
255 Lit Solver::pickBranchLit()
256 {
257 Var next = var_Undef;
258
259 // Random decision:
260 if (drand(random_seed) < random_var_freq && !order_heap.empty()){
261 next = order_heap[irand(random_seed,order_heap.size())];
262 if (value(next) == l_Undef && decision[next])
263 rnd_decisions++; }
264
265 // Activity based decision:
266 while (next == var_Undef || value(next) != l_Undef || !decision[next])
267 if (order_heap.empty()){
268 next = var_Undef;
269 break;
270 }else
271 next = order_heap.removeMin();
272
273 // Choose polarity based on different polarity modes (global or per-variable):
274 if (next == var_Undef)
275 return lit_Undef;
276 else if (user_pol[next] != l_Undef)
277 return mkLit(next, user_pol[next] == l_True);
278 else if (rnd_pol)
279 return mkLit(next, drand(random_seed) < 0.5);
280 else
281 return mkLit(next, polarity[next]);
282 }
283
284
285 /*_________________________________________________________________________________________________
286 |
287 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
288 |
289 | Description:
290 | Analyze conflict and produce a reason clause.
291 |
292 | Pre-conditions:
293 | * 'out_learnt' is assumed to be cleared.
294 | * Current decision level must be greater than root level.
295 |
296 | Post-conditions:
297 | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
298 | * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
299 | rest of literals. There may be others from the same level though.
300 |
301 |________________________________________________________________________________________________@*/
302 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
303 {
304 int pathC = 0;
305 Lit p = lit_Undef;
306
307 // Generate conflict clause:
308 //
309 out_learnt.push(); // (leave room for the asserting literal)
310 int index = trail.size() - 1;
311
312 do{
313 assert(confl != CRef_Undef); // (otherwise should be UIP)
314 Clause& c = ca[confl];
315
316 if (c.learnt())
317 claBumpActivity(c);
318
319 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
320 Lit q = c[j];
321
322 if (!seen[var(q)] && level(var(q)) > 0){
323 varBumpActivity(var(q));
324 seen[var(q)] = 1;
325 if (level(var(q)) >= decisionLevel())
326 pathC++;
327 else
328 out_learnt.push(q);
329 }
330 }
331
332 // Select next clause to look at:
333 while (!seen[var(trail[index--])]);
334 p = trail[index+1];
335 confl = reason(var(p));
336 seen[var(p)] = 0;
337 pathC--;
338
339 }while (pathC > 0);
340 out_learnt[0] = ~p;
341
342 // Simplify conflict clause:
343 //
344 int i, j;
345 out_learnt.copyTo(analyze_toclear);
346 if (ccmin_mode == 2){
347 for (i = j = 1; i < out_learnt.size(); i++)
348 if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))
349 out_learnt[j++] = out_learnt[i];
350
351 }else if (ccmin_mode == 1){
352 for (i = j = 1; i < out_learnt.size(); i++){
353 Var x = var(out_learnt[i]);
354
355 if (reason(x) == CRef_Undef)
356 out_learnt[j++] = out_learnt[i];
357 else{
358 Clause& c = ca[reason(var(out_learnt[i]))];
359 for (int k = 1; k < c.size(); k++)
360 if (!seen[var(c[k])] && level(var(c[k])) > 0){
361 out_learnt[j++] = out_learnt[i];
362 break; }
363 }
364 }
365 }else
366 i = j = out_learnt.size();
367
368 max_literals += out_learnt.size();
369 out_learnt.shrink(i - j);
370 tot_literals += out_learnt.size();
371
372 // Find correct backtrack level:
373 //
374 if (out_learnt.size() == 1)
375 out_btlevel = 0;
376 else{
377 int max_i = 1;
378 // Find the first literal assigned at the next-highest level:
379 for (int i = 2; i < out_learnt.size(); i++)
380 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
381 max_i = i;
382 // Swap-in this literal at index 1:
383 Lit p = out_learnt[max_i];
384 out_learnt[max_i] = out_learnt[1];
385 out_learnt[1] = p;
386 out_btlevel = level(var(p));
387 }
388
389 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
390 }
391
392
393 // Check if 'p' can be removed from a conflict clause.
394 bool Solver::litRedundant(Lit p)
395 {
396 enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };
397 assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);
398 assert(reason(var(p)) != CRef_Undef);
399
400 Clause* c = &ca[reason(var(p))];
401 vec<ShrinkStackElem>& stack = analyze_stack;
402 stack.clear();
403
404 for (uint32_t i = 1; ; i++){
405 if (i < (uint32_t)c->size()){
406 // Checking 'p'-parents 'l':
407 Lit l = (*c)[i];
408
409 // Variable at level 0 or previously removable:
410 if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){
411 continue; }
412
413 // Check variable can not be removed for some local reason:
414 if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){
415 stack.push(ShrinkStackElem(0, p));
416 for (int i = 0; i < stack.size(); i++)
417 if (seen[var(stack[i].l)] == seen_undef){
418 seen[var(stack[i].l)] = seen_failed;
419 analyze_toclear.push(stack[i].l);
420 }
421
422 return false;
423 }
424
425 // Recursively check 'l':
426 stack.push(ShrinkStackElem(i, p));
427 i = 0;
428 p = l;
429 c = &ca[reason(var(p))];
430 }else{
431 // Finished with current element 'p' and reason 'c':
432 if (seen[var(p)] == seen_undef){
433 seen[var(p)] = seen_removable;
434 analyze_toclear.push(p);
435 }
436
437 // Terminate with success if stack is empty:
438 if (stack.size() == 0) break;
439
440 // Continue with top element on stack:
441 i = stack.last().i;
442 p = stack.last().l;
443 c = &ca[reason(var(p))];
444
445 stack.pop();
446 }
447 }
448
449 return true;
450 }
451
452
453 /*_________________________________________________________________________________________________
454 |
455 | analyzeFinal : (p : Lit) -> [void]
456 |
457 | Description:
458 | Specialized analysis procedure to express the final conflict in terms of assumptions.
459 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
460 | stores the result in 'out_conflict'.
461 |________________________________________________________________________________________________@*/
462 void Solver::analyzeFinal(Lit p, LSet& out_conflict)
463 {
464 out_conflict.clear();
465 out_conflict.insert(p);
466
467 if (decisionLevel() == 0)
468 return;
469
470 seen[var(p)] = 1;
471
472 for (int i = trail.size()-1; i >= trail_lim[0]; i--){
473 Var x = var(trail[i]);
474 if (seen[x]){
475 if (reason(x) == CRef_Undef){
476 assert(level(x) > 0);
477 out_conflict.insert(~trail[i]);
478 }else{
479 Clause& c = ca[reason(x)];
480 for (int j = 1; j < c.size(); j++)
481 if (level(var(c[j])) > 0)
482 seen[var(c[j])] = 1;
483 }
484 seen[x] = 0;
485 }
486 }
487
488 seen[var(p)] = 0;
489 }
490
491
492 void Solver::uncheckedEnqueue(Lit p, CRef from)
493 {
494 assert(value(p) == l_Undef);
495 assigns[var(p)] = lbool(!sign(p));
496 vardata[var(p)] = mkVarData(from, decisionLevel());
497 trail.push_(p);
498 }
499
500
501 /*_________________________________________________________________________________________________
502 |
503 | propagate : [void] -> [Clause*]
504 |
505 | Description:
506 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
507 | otherwise CRef_Undef.
508 |
509 | Post-conditions:
510 | * the propagation queue is empty, even if there was a conflict.
511 |________________________________________________________________________________________________@*/
512 CRef Solver::propagate()
513 {
514 CRef confl = CRef_Undef;
515 int num_props = 0;
516
517 while (qhead < trail.size()){
518 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
519 vec<Watcher>& ws = watches.lookup(p);
520 Watcher *i, *j, *end;
521 num_props++;
522
523 for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
524 // Try to avoid inspecting the clause:
525 Lit blocker = i->blocker;
526 if (value(blocker) == l_True){
527 *j++ = *i++; continue; }
528
529 // Make sure the false literal is data[1]:
530 CRef cr = i->cref;
531 Clause& c = ca[cr];
532 Lit false_lit = ~p;
533 if (c[0] == false_lit)
534 c[0] = c[1], c[1] = false_lit;
535 assert(c[1] == false_lit);
536 i++;
537
538 // If 0th watch is true, then clause is already satisfied.
539 Lit first = c[0];
540 Watcher w = Watcher(cr, first);
541 if (first != blocker && value(first) == l_True){
542 *j++ = w; continue; }
543
544 // Look for new watch:
545 for (int k = 2; k < c.size(); k++)
546 if (value(c[k]) != l_False){
547 c[1] = c[k]; c[k] = false_lit;
548 watches[~c[1]].push(w);
549 goto NextClause; }
550
551 // Did not find watch -- clause is unit under assignment:
552 *j++ = w;
553 if (value(first) == l_False){
554 confl = cr;
555 qhead = trail.size();
556 // Copy the remaining watches:
557 while (i < end)
558 *j++ = *i++;
559 }else
560 uncheckedEnqueue(first, cr);
561
562 NextClause:;
563 }
564 ws.shrink(i - j);
565 }
566 propagations += num_props;
567 simpDB_props -= num_props;
568
569 return confl;
570 }
571
572
573 /*_________________________________________________________________________________________________
574 |
575 | reduceDB : () -> [void]
576 |
577 | Description:
578 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
579 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
580 |________________________________________________________________________________________________@*/
581 struct reduceDB_lt {
582 ClauseAllocator& ca;
583 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
584 bool operator () (CRef x, CRef y) {
585 return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
586 };
587 void Solver::reduceDB()
588 {
589 int i, j;
590 double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity
591
592 sort(learnts, reduceDB_lt(ca));
593 // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
594 // and clauses with activity smaller than 'extra_lim':
595 for (i = j = 0; i < learnts.size(); i++){
596 Clause& c = ca[learnts[i]];
597 if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
598 removeClause(learnts[i]);
599 else
600 learnts[j++] = learnts[i];
601 }
602 learnts.shrink(i - j);
603 checkGarbage();
604 }
605
606
607 void Solver::removeSatisfied(vec<CRef>& cs)
608 {
609 int i, j;
610 for (i = j = 0; i < cs.size(); i++){
611 Clause& c = ca[cs[i]];
612 if (satisfied(c))
613 removeClause(cs[i]);
614 else{
615 // Trim clause:
616 assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);
617 for (int k = 2; k < c.size(); k++)
618 if (value(c[k]) == l_False){
619 c[k--] = c[c.size()-1];
620 c.pop();
621 }
622 cs[j++] = cs[i];
623 }
624 }
625 cs.shrink(i - j);
626 }
627
628
629 void Solver::rebuildOrderHeap()
630 {
631 vec<Var> vs;
632 for (Var v = 0; v < nVars(); v++)
633 if (decision[v] && value(v) == l_Undef)
634 vs.push(v);
635 order_heap.build(vs);
636 }
637
638
639 /*_________________________________________________________________________________________________
640 |
641 | simplify : [void] -> [bool]
642 |
643 | Description:
644 | Simplify the clause database according to the current top-level assigment. Currently, the only
645 | thing done here is the removal of satisfied clauses, but more things can be put here.
646 |________________________________________________________________________________________________@*/
647 bool Solver::simplify()
648 {
649 assert(decisionLevel() == 0);
650
651 if (!ok || propagate() != CRef_Undef)
652 return ok = false;
653
654 if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
655 return true;
656
657 // Remove satisfied clauses:
658 removeSatisfied(learnts);
659 if (remove_satisfied){ // Can be turned off.
660 removeSatisfied(clauses);
661
662 // TODO: what todo in if 'remove_satisfied' is false?
663
664 // Remove all released variables from the trail:
665 for (int i = 0; i < released_vars.size(); i++){
666 assert(seen[released_vars[i]] == 0);
667 seen[released_vars[i]] = 1;
668 }
669
670 int i, j;
671 for (i = j = 0; i < trail.size(); i++)
672 if (seen[var(trail[i])] == 0)
673 trail[j++] = trail[i];
674 trail.shrink(i - j);
675 //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
676 qhead = trail.size();
677
678 for (int i = 0; i < released_vars.size(); i++)
679 seen[released_vars[i]] = 0;
680
681 // Released variables are now ready to be reused:
682 append(released_vars, free_vars);
683 released_vars.clear();
684 }
685 checkGarbage();
686 rebuildOrderHeap();
687
688 simpDB_assigns = nAssigns();
689 simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
690
691 return true;
692 }
693
694
695 /*_________________________________________________________________________________________________
696 |
697 | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
698 |
699 | Description:
700 | Search for a model the specified number of conflicts.
701 | NOTE! Use negative value for 'nof_conflicts' indicate infinity.
702 |
703 | Output:
704 | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
705 | all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
706 | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
707 |________________________________________________________________________________________________@*/
708 lbool Solver::search(int nof_conflicts)
709 {
710 assert(ok);
711 int backtrack_level;
712 int conflictC = 0;
713 vec<Lit> learnt_clause;
714 starts++;
715
716 for (;;){
717 CRef confl = propagate();
718 if (confl != CRef_Undef){
719 // CONFLICT
720 conflicts++; conflictC++;
721 if (decisionLevel() == 0) return l_False;
722
723 learnt_clause.clear();
724 analyze(confl, learnt_clause, backtrack_level);
725 cancelUntil(backtrack_level);
726
727 if (learnt_clause.size() == 1){
728 uncheckedEnqueue(learnt_clause[0]);
729 }else{
730 CRef cr = ca.alloc(learnt_clause, true);
731 learnts.push(cr);
732 attachClause(cr);
733 claBumpActivity(ca[cr]);
734 uncheckedEnqueue(learnt_clause[0], cr);
735 }
736
737 varDecayActivity();
738 claDecayActivity();
739
740 if (--learntsize_adjust_cnt == 0){
741 learntsize_adjust_confl *= learntsize_adjust_inc;
742 learntsize_adjust_cnt = (int)learntsize_adjust_confl;
743 max_learnts *= learntsize_inc;
744
745 if (verbosity >= 1)
746 printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
747 (int)conflicts,
748 (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
749 (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
750 }
751
752 }else{
753 // NO CONFLICT
754 if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
755 // Reached bound on number of conflicts:
756 progress_estimate = progressEstimate();
757 cancelUntil(0);
758 return l_Undef; }
759
760 // Simplify the set of problem clauses:
761 if (decisionLevel() == 0 && !simplify())
762 return l_False;
763
764 if (learnts.size()-nAssigns() >= max_learnts)
765 // Reduce the set of learnt clauses:
766 reduceDB();
767
768 Lit next = lit_Undef;
769 while (decisionLevel() < assumptions.size()){
770 // Perform user provided assumption:
771 Lit p = assumptions[decisionLevel()];
772 if (value(p) == l_True){
773 // Dummy decision level:
774 newDecisionLevel();
775 }else if (value(p) == l_False){
776 analyzeFinal(~p, conflict);
777 return l_False;
778 }else{
779 next = p;
780 break;
781 }
782 }
783
784 if (next == lit_Undef){
785 // New variable decision:
786 decisions++;
787 next = pickBranchLit();
788
789 if (next == lit_Undef)
790 // Model found:
791 return l_True;
792 }
793
794 // Increase decision level and enqueue 'next'
795 newDecisionLevel();
796 uncheckedEnqueue(next);
797 }
798 }
799 }
800
801
802 double Solver::progressEstimate() const
803 {
804 double progress = 0;
805 double F = 1.0 / nVars();
806
807 for (int i = 0; i <= decisionLevel(); i++){
808 int beg = i == 0 ? 0 : trail_lim[i - 1];
809 int end = i == decisionLevel() ? trail.size() : trail_lim[i];
810 progress += pow(F, i) * (end - beg);
811 }
812
813 return progress / nVars();
814 }
815
816 /*
817 Finite subsequences of the Luby-sequence:
818
819 0: 1
820 1: 1 1 2
821 2: 1 1 2 1 1 2 4
822 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
823 ...
824
825
826 */
827
828 static double luby(double y, int x){
829
830 // Find the finite subsequence that contains index 'x', and the
831 // size of that subsequence:
832 int size, seq;
833 for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
834
835 while (size-1 != x){
836 size = (size-1)>>1;
837 seq--;
838 x = x % size;
839 }
840
841 return pow(y, seq);
842 }
843
844 // NOTE: assumptions passed in member-variable 'assumptions'.
845 lbool Solver::solve_()
846 {
847 model.clear();
848 conflict.clear();
849 if (!ok) return l_False;
850
851 solves++;
852
853 max_learnts = nClauses() * learntsize_factor;
854 if (max_learnts < min_learnts_lim)
855 max_learnts = min_learnts_lim;
856
857 learntsize_adjust_confl = learntsize_adjust_start_confl;
858 learntsize_adjust_cnt = (int)learntsize_adjust_confl;
859 lbool status = l_Undef;
860
861 if (verbosity >= 1){
862 printf("============================[ Search Statistics ]==============================\n");
863 printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
864 printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
865 printf("===============================================================================\n");
866 }
867
868 // Search:
869 int curr_restarts = 0;
870 while (status == l_Undef){
871 double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
872 status = search(rest_base * restart_first);
873 if (!withinBudget()) break;
874 curr_restarts++;
875 }
876
877 if (verbosity >= 1)
878 printf("===============================================================================\n");
879
880
881 if (status == l_True){
882 // Extend & copy model:
883 model.growTo(nVars());
884 for (int i = 0; i < nVars(); i++) model[i] = value(i);
885 }else if (status == l_False && conflict.size() == 0)
886 ok = false;
887
888 cancelUntil(0);
889 return status;
890 }
891
892
893 bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out)
894 {
895 trail_lim.push(trail.size());
896 for (int i = 0; i < assumps.size(); i++){
897 Lit a = assumps[i];
898
899 if (value(a) == l_False){
900 cancelUntil(0);
901 return false;
902 }else if (value(a) == l_Undef)
903 uncheckedEnqueue(a);
904 }
905
906 unsigned trail_before = trail.size();
907 bool ret = true;
908 if (propagate() == CRef_Undef){
909 out.clear();
910 for (int j = trail_before; j < trail.size(); j++)
911 out.push(trail[j]);
912 }else
913 ret = false;
914
915 cancelUntil(0);
916 return ret;
917 }
918
919 //=================================================================================================
920 // Writing CNF to DIMACS:
921 //
922 // FIXME: this needs to be rewritten completely.
923
924 static Var mapVar(Var x, vec<Var>& map, Var& max)
925 {
926 if (map.size() <= x || map[x] == -1){
927 map.growTo(x+1, -1);
928 map[x] = max++;
929 }
930 return map[x];
931 }
932
933
934 void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
935 {
936 if (satisfied(c)) return;
937
938 for (int i = 0; i < c.size(); i++)
939 if (value(c[i]) != l_False)
940 fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
941 fprintf(f, "0\n");
942 }
943
944
945 void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
946 {
947 FILE* f = fopen(file, "wr");
948 if (f == NULL)
949 fprintf(stderr, "could not open file %s\n", file), exit(1);
950 toDimacs(f, assumps);
951 fclose(f);
952 }
953
954
955 void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
956 {
957 // Handle case when solver is in contradictory state:
958 if (!ok){
959 fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
960 return; }
961
962 vec<Var> map; Var max = 0;
963
964 // Cannot use removeClauses here because it is not safe
965 // to deallocate them at this point. Could be improved.
966 int cnt = 0;
967 for (int i = 0; i < clauses.size(); i++)
968 if (!satisfied(ca[clauses[i]]))
969 cnt++;
970
971 for (int i = 0; i < clauses.size(); i++)
972 if (!satisfied(ca[clauses[i]])){
973 Clause& c = ca[clauses[i]];
974 for (int j = 0; j < c.size(); j++)
975 if (value(c[j]) != l_False)
976 mapVar(var(c[j]), map, max);
977 }
978
979 // Assumptions are added as unit clauses:
980 cnt += assumps.size();
981
982 fprintf(f, "p cnf %d %d\n", max, cnt);
983
984 for (int i = 0; i < assumps.size(); i++){
985 assert(value(assumps[i]) != l_False);
986 fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
987 }
988
989 for (int i = 0; i < clauses.size(); i++)
990 toDimacs(f, ca[clauses[i]], map, max);
991
992 if (verbosity > 0)
993 printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
994 }
995
996
997 void Solver::printStats() const
998 {
999 double cpu_time = cpuTime();
1000 double mem_used = memUsedPeak();
1001 printf("restarts : %" PRIu64 "\n", starts);
1002 printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time);
1003 printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
1004 printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time);
1005 printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
1006 if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
1007 printf("CPU time : %g s\n", cpu_time);
1008 }
1009
1010
1011 //=================================================================================================
1012 // Garbage Collection methods:
1013
1014 void Solver::relocAll(ClauseAllocator& to)
1015 {
1016 // All watchers:
1017 //
1018 watches.cleanAll();
1019 for (int v = 0; v < nVars(); v++)
1020 for (int s = 0; s < 2; s++){
1021 Lit p = mkLit(v, s);
1022 vec<Watcher>& ws = watches[p];
1023 for (int j = 0; j < ws.size(); j++)
1024 ca.reloc(ws[j].cref, to);
1025 }
1026
1027 // All reasons:
1028 //
1029 for (int i = 0; i < trail.size(); i++){
1030 Var v = var(trail[i]);
1031
1032 // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep
1033 // 'dangling' reasons here. It is safe and does not hurt.
1034 if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){
1035 assert(!isRemoved(reason(v)));
1036 ca.reloc(vardata[v].reason, to);
1037 }
1038 }
1039
1040 // All learnt:
1041 //
1042 int i, j;
1043 for (i = j = 0; i < learnts.size(); i++)
1044 if (!isRemoved(learnts[i])){
1045 ca.reloc(learnts[i], to);
1046 learnts[j++] = learnts[i];
1047 }
1048 learnts.shrink(i - j);
1049
1050 // All original:
1051 //
1052 for (i = j = 0; i < clauses.size(); i++)
1053 if (!isRemoved(clauses[i])){
1054 ca.reloc(clauses[i], to);
1055 clauses[j++] = clauses[i];
1056 }
1057 clauses.shrink(i - j);
1058 }
1059
1060
1061 void Solver::garbageCollect()
1062 {
1063 // Initialize the next region to a size corresponding to the estimated utilization degree. This
1064 // is not precise but should avoid some unnecessary reallocations for the new region:
1065 ClauseAllocator to(ca.size() - ca.wasted());
1066
1067 relocAll(to);
1068 if (verbosity >= 2)
1069 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
1070 ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
1071 to.moveTo(ca);
1072 }