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