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
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:
13 The above copyright notice and this permission notice shall be included in all copies or
14 substantial portions of the Software.
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 **************************************************************************************************/
25 #include "libs/minisat/Alg.h"
26 #include "libs/minisat/Sort.h"
27 #include "libs/minisat/System.h"
28 #include "libs/minisat/Solver.h"
30 using namespace Minisat
;
32 //=================================================================================================
36 static const char* _cat
= "CORE";
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
));
52 //=================================================================================================
53 // Constructor/Destructor:
58 // Parameters (user settable):
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
)
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
)
75 // Parameters (the rest):
77 , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
79 // Parameters (experimental):
81 , learntsize_adjust_start_confl (100)
82 , learntsize_adjust_inc (1.5)
84 // Statistics: (formerly in 'SolverStats')
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)
89 , watches (WatcherDeleted(ca
))
90 , order_heap (VarOrderLt(activity
))
97 , progress_estimate (0)
98 , remove_satisfied (true)
101 // Resource constraints:
103 , conflict_budget (-1)
104 , propagation_budget (-1)
105 , asynch_interrupt (false)
114 //=================================================================================================
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).
121 Var
Solver::newVar(lbool upol
, bool dvar
)
124 if (free_vars
.size() > 0){
125 v
= free_vars
.last();
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);
136 polarity
.insert(v
, true);
137 user_pol
.insert(v
, upol
);
138 decision
.reserve(v
);
139 trail
.capacity(v
+1);
140 setDecisionVar(v
, dvar
);
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
)
149 if (value(l
) == l_Undef
){
151 released_vars
.push(var(l
));
156 bool Solver::addClause_(vec
<Lit
>& ps
)
158 assert(decisionLevel() == 0);
159 if (!ok
) return false;
161 // Check if clause is satisfied and remove false/duplicate literals:
164 for (i
= j
= 0, p
= lit_Undef
; i
< ps
.size(); i
++)
165 if (value(ps
[i
]) == l_True
|| ps
[i
] == ~p
)
167 else if (value(ps
[i
]) != l_False
&& ps
[i
] != p
)
173 else if (ps
.size() == 1){
174 uncheckedEnqueue(ps
[0]);
175 return ok
= (propagate() == CRef_Undef
);
177 CRef cr
= ca
.alloc(ps
, false);
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();
196 void Solver::detachClause(CRef cr
, bool strict
){
197 const Clause
& c
= ca
[cr
];
198 assert(c
.size() > 1);
200 // Strict or lazy detaching:
202 remove(watches
[~c
[0]], Watcher(cr
, c
[1]));
203 remove(watches
[~c
[1]], Watcher(cr
, c
[0]));
205 watches
.smudge(~c
[0]);
206 watches
.smudge(~c
[1]);
209 if (c
.learnt()) num_learnts
--, learnts_literals
-= c
.size();
210 else num_clauses
--, clauses_literals
-= c
.size();
214 void Solver::removeClause(CRef cr
) {
217 // Don't leave pointers to free'd memory!
218 if (locked(c
)) vardata
[var(c
[0])].reason
= CRef_Undef
;
224 bool Solver::satisfied(const Clause
& c
) const {
225 for (int i
= 0; i
< c
.size(); i
++)
226 if (value(c
[i
]) == l_True
)
231 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
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
]);
241 qhead
= trail_lim
[level
];
242 trail
.shrink(trail
.size() - trail_lim
[level
]);
243 trail_lim
.shrink(trail_lim
.size() - level
);
247 //=================================================================================================
251 Lit
Solver::pickBranchLit()
253 Var next
= var_Undef
;
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
])
261 // Activity based decision:
262 while (next
== var_Undef
|| value(next
) != l_Undef
|| !decision
[next
])
263 if (order_heap
.empty()){
267 next
= order_heap
.removeMin();
269 // Choose polarity based on different polarity modes (global or per-variable):
270 if (next
== var_Undef
)
272 else if (user_pol
[next
] != l_Undef
)
273 return mkLit(next
, user_pol
[next
] == l_True
);
275 return mkLit(next
, drand(random_seed
) < 0.5);
277 return mkLit(next
, polarity
[next
]);
281 /*_________________________________________________________________________________________________
283 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
286 | Analyze conflict and produce a reason clause.
289 | * 'out_learnt' is assumed to be cleared.
290 | * Current decision level must be greater than root level.
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.
297 |________________________________________________________________________________________________@*/
298 void Solver::analyze(CRef confl
, vec
<Lit
>& out_learnt
, int& out_btlevel
)
303 // Generate conflict clause:
305 out_learnt
.push(); // (leave room for the asserting literal)
306 int index
= trail
.size() - 1;
309 assert(confl
!= CRef_Undef
); // (otherwise should be UIP)
310 Clause
& c
= ca
[confl
];
315 for (int j
= (p
== lit_Undef
) ? 0 : 1; j
< c
.size(); j
++){
318 if (!seen
[var(q
)] && level(var(q
)) > 0){
319 varBumpActivity(var(q
));
321 if (level(var(q
)) >= decisionLevel())
328 // Select next clause to look at:
329 while (!seen
[var(trail
[index
--])]);
331 confl
= reason(var(p
));
338 // Simplify conflict clause:
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
];
347 }else if (ccmin_mode
== 1){
348 for (i
= j
= 1; i
< out_learnt
.size(); i
++){
349 Var x
= var(out_learnt
[i
]);
351 if (reason(x
) == CRef_Undef
)
352 out_learnt
[j
++] = out_learnt
[i
];
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
];
362 i
= j
= out_learnt
.size();
364 max_literals
+= out_learnt
.size();
365 out_learnt
.shrink(i
- j
);
366 tot_literals
+= out_learnt
.size();
368 // Find correct backtrack level:
370 if (out_learnt
.size() == 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
])))
378 // Swap-in this literal at index 1:
379 Lit p
= out_learnt
[max_i
];
380 out_learnt
[max_i
] = out_learnt
[1];
382 out_btlevel
= level(var(p
));
385 for (int j
= 0; j
< analyze_toclear
.size(); j
++) seen
[var(analyze_toclear
[j
])] = 0; // ('seen[]' is now cleared)
389 // Check if 'p' can be removed from a conflict clause.
390 bool Solver::litRedundant(Lit p
)
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
);
396 Clause
* c
= &ca
[reason(var(p
))];
397 vec
<ShrinkStackElem
>& stack
= analyze_stack
;
400 for (uint32_t i
= 1; ; i
++){
401 if (i
< (uint32_t)c
->size()){
402 // Checking 'p'-parents 'l':
405 // Variable at level 0 or previously removable:
406 if (level(var(l
)) == 0 || seen
[var(l
)] == seen_source
|| seen
[var(l
)] == seen_removable
){
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
);
421 // Recursively check 'l':
422 stack
.push(ShrinkStackElem(i
, p
));
425 c
= &ca
[reason(var(p
))];
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
);
433 // Terminate with success if stack is empty:
434 if (stack
.size() == 0) break;
436 // Continue with top element on stack:
439 c
= &ca
[reason(var(p
))];
449 /*_________________________________________________________________________________________________
451 | analyzeFinal : (p : Lit) -> [void]
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
)
460 out_conflict
.clear();
461 out_conflict
.insert(p
);
463 if (decisionLevel() == 0)
468 for (int i
= trail
.size()-1; i
>= trail_lim
[0]; i
--){
469 Var x
= var(trail
[i
]);
471 if (reason(x
) == CRef_Undef
){
472 assert(level(x
) > 0);
473 out_conflict
.insert(~trail
[i
]);
475 Clause
& c
= ca
[reason(x
)];
476 for (int j
= 1; j
< c
.size(); j
++)
477 if (level(var(c
[j
])) > 0)
488 void Solver::uncheckedEnqueue(Lit p
, CRef from
)
490 assert(value(p
) == l_Undef
);
491 assigns
[var(p
)] = lbool(!sign(p
));
492 vardata
[var(p
)] = mkVarData(from
, decisionLevel());
497 /*_________________________________________________________________________________________________
499 | propagate : [void] -> [Clause*]
502 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
503 | otherwise CRef_Undef.
506 | * the propagation queue is empty, even if there was a conflict.
507 |________________________________________________________________________________________________@*/
508 CRef
Solver::propagate()
510 CRef confl
= CRef_Undef
;
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
;
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; }
525 // Make sure the false literal is data[1]:
529 if (c
[0] == false_lit
)
530 c
[0] = c
[1], c
[1] = false_lit
;
531 assert(c
[1] == false_lit
);
534 // If 0th watch is true, then clause is already satisfied.
536 Watcher w
= Watcher(cr
, first
);
537 if (first
!= blocker
&& value(first
) == l_True
){
538 *j
++ = w
; continue; }
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
);
547 // Did not find watch -- clause is unit under assignment:
549 if (value(first
) == l_False
){
551 qhead
= trail
.size();
552 // Copy the remaining watches:
556 uncheckedEnqueue(first
, cr
);
562 propagations
+= num_props
;
563 simpDB_props
-= num_props
;
569 /*_________________________________________________________________________________________________
571 | reduceDB : () -> [void]
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 |________________________________________________________________________________________________@*/
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()); }
583 void Solver::reduceDB()
586 double extra_lim
= cla_inc
/ learnts
.size(); // Remove any clause below this activity
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
]);
596 learnts
[j
++] = learnts
[i
];
598 learnts
.shrink(i
- j
);
603 void Solver::removeSatisfied(vec
<CRef
>& cs
)
606 for (i
= j
= 0; i
< cs
.size(); i
++){
607 Clause
& c
= ca
[cs
[i
]];
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];
625 void Solver::rebuildOrderHeap()
628 for (Var v
= 0; v
< nVars(); v
++)
629 if (decision
[v
] && value(v
) == l_Undef
)
631 order_heap
.build(vs
);
635 /*_________________________________________________________________________________________________
637 | simplify : [void] -> [bool]
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()
645 assert(decisionLevel() == 0);
647 if (!ok
|| propagate() != CRef_Undef
)
650 if (nAssigns() == simpDB_assigns
|| (simpDB_props
> 0))
653 // Remove satisfied clauses:
654 removeSatisfied(learnts
);
655 if (remove_satisfied
){ // Can be turned off.
656 removeSatisfied(clauses
);
658 // TODO: what todo in if 'remove_satisfied' is false?
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;
667 for (i
= j
= 0; i
< trail
.size(); i
++)
668 if (seen
[var(trail
[i
])] == 0)
669 trail
[j
++] = trail
[i
];
671 //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
672 qhead
= trail
.size();
674 for (int i
= 0; i
< released_vars
.size(); i
++)
675 seen
[released_vars
[i
]] = 0;
677 // Released variables are now ready to be reused:
678 append(released_vars
, free_vars
);
679 released_vars
.clear();
684 simpDB_assigns
= nAssigns();
685 simpDB_props
= clauses_literals
+ learnts_literals
; // (shouldn't depend on stats really, but it will do for now)
691 /*_________________________________________________________________________________________________
693 | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
696 | Search for a model the specified number of conflicts.
697 | NOTE! Use negative value for 'nof_conflicts' indicate infinity.
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
)
709 vec
<Lit
> learnt_clause
;
713 CRef confl
= propagate();
714 if (confl
!= CRef_Undef
){
716 conflicts
++; conflictC
++;
717 if (decisionLevel() == 0) return l_False
;
719 learnt_clause
.clear();
720 analyze(confl
, learnt_clause
, backtrack_level
);
721 cancelUntil(backtrack_level
);
723 if (learnt_clause
.size() == 1){
724 uncheckedEnqueue(learnt_clause
[0]);
726 CRef cr
= ca
.alloc(learnt_clause
, true);
729 claBumpActivity(ca
[cr
]);
730 uncheckedEnqueue(learnt_clause
[0], cr
);
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
;
742 printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
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);
750 if ((nof_conflicts
>= 0 && conflictC
>= nof_conflicts
) || !withinBudget()){
751 // Reached bound on number of conflicts:
752 progress_estimate
= progressEstimate();
756 // Simplify the set of problem clauses:
757 if (decisionLevel() == 0 && !simplify())
760 if (learnts
.size()-nAssigns() >= max_learnts
)
761 // Reduce the set of learnt clauses:
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:
771 }else if (value(p
) == l_False
){
772 analyzeFinal(~p
, conflict
);
780 if (next
== lit_Undef
){
781 // New variable decision:
783 next
= pickBranchLit();
785 if (next
== lit_Undef
)
790 // Increase decision level and enqueue 'next'
792 uncheckedEnqueue(next
);
798 double Solver::progressEstimate() const
801 double F
= 1.0 / nVars();
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
);
809 return progress
/ nVars();
813 Finite subsequences of the Luby-sequence:
818 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
824 static double luby(double y
, int x
){
826 // Find the finite subsequence that contains index 'x', and the
827 // size of that subsequence:
829 for (size
= 1, seq
= 0; size
< x
+1; seq
++, size
= 2*size
+1);
840 // NOTE: assumptions passed in member-variable 'assumptions'.
841 lbool
Solver::solve_()
845 if (!ok
) return l_False
;
849 max_learnts
= nClauses() * learntsize_factor
;
850 if (max_learnts
< min_learnts_lim
)
851 max_learnts
= min_learnts_lim
;
853 learntsize_adjust_confl
= learntsize_adjust_start_confl
;
854 learntsize_adjust_cnt
= (int)learntsize_adjust_confl
;
855 lbool status
= l_Undef
;
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");
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;
874 printf("===============================================================================\n");
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)
889 bool Solver::implies(const vec
<Lit
>& assumps
, vec
<Lit
>& out
)
891 trail_lim
.push(trail
.size());
892 for (int i
= 0; i
< assumps
.size(); i
++){
895 if (value(a
) == l_False
){
898 }else if (value(a
) == l_Undef
)
902 unsigned trail_before
= trail
.size();
904 if (propagate() == CRef_Undef
){
906 for (int j
= trail_before
; j
< trail
.size(); j
++)
915 //=================================================================================================
916 // Writing CNF to DIMACS:
918 // FIXME: this needs to be rewritten completely.
920 static Var
mapVar(Var x
, vec
<Var
>& map
, Var
& max
)
922 if (map
.size() <= x
|| map
[x
] == -1){
930 void Solver::toDimacs(FILE* f
, Clause
& c
, vec
<Var
>& map
, Var
& max
)
932 if (satisfied(c
)) return;
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);
941 void Solver::toDimacs(const char *file
, const vec
<Lit
>& assumps
)
943 FILE* f
= fopen(file
, "wr");
945 fprintf(stderr
, "could not open file %s\n", file
), exit(1);
946 toDimacs(f
, assumps
);
951 void Solver::toDimacs(FILE* f
, const vec
<Lit
>& assumps
)
953 // Handle case when solver is in contradictory state:
955 fprintf(f
, "p cnf 1 2\n1 0\n-1 0\n");
958 vec
<Var
> map
; Var max
= 0;
960 // Cannot use removeClauses here because it is not safe
961 // to deallocate them at this point. Could be improved.
963 for (int i
= 0; i
< clauses
.size(); i
++)
964 if (!satisfied(ca
[clauses
[i
]]))
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
);
975 // Assumptions are added as unit clauses:
976 cnt
+= assumps
.size();
978 fprintf(f
, "p cnf %d %d\n", max
, cnt
);
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);
985 for (int i
= 0; i
< clauses
.size(); i
++)
986 toDimacs(f
, ca
[clauses
[i
]], map
, max
);
989 printf("Wrote DIMACS with %d variables and %d clauses.\n", max
, cnt
);
993 void Solver::printStats() const
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
);
1007 //=================================================================================================
1008 // Garbage Collection methods:
1010 void Solver::relocAll(ClauseAllocator
& to
)
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
);
1025 for (int i
= 0; i
< trail
.size(); i
++){
1026 Var v
= var(trail
[i
]);
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
);
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
];
1044 learnts
.shrink(i
- j
);
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
];
1053 clauses
.shrink(i
- j
);
1057 void Solver::garbageCollect()
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());
1065 printf("| Garbage collection: %12d bytes => %12d bytes |\n",
1066 ca
.size()*ClauseAllocator::Unit_Size
, to
.size()*ClauseAllocator::Unit_Size
);