1 /****************************************************************************************[Solver.C]
2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5 associated documentation files (the "Software"), to deal in the Software without restriction,
6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8 furnished to do so, subject to the following conditions:
10 The above copyright notice and this permission notice shall be included in all copies or
11 substantial portions of the Software.
13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
18 **************************************************************************************************/
25 //=================================================================================================
26 // Constructor/Destructor:
31 // Parameters: (formerly in 'SearchParams')
32 var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
33 , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
37 , expensive_ccmin (true)
38 , polarity_mode (polarity_false)
41 // Statistics: (formerly in 'SolverStats')
43 , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
44 , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
52 , order_heap (VarOrderLt(activity))
53 , random_seed (91648253)
54 , progress_estimate(0)
55 , remove_satisfied (true)
61 for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
62 for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
66 //=================================================================================================
70 // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
71 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
73 Var Solver::newVar(bool sign, bool dvar)
76 watches .push(); // (list for positive literal)
77 watches .push(); // (list for negative literal)
79 assigns .push(toInt(l_Undef));
84 polarity .push((char)sign);
85 decision_var.push((char)dvar);
92 bool Solver::addClause(vec<Lit>& ps)
94 assert(decisionLevel() == 0);
99 // Check if clause is satisfied and remove false/duplicate literals:
102 for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
103 if (value(ps[i]) == l_True || ps[i] == ~p)
105 else if (value(ps[i]) != l_False && ps[i] != p)
112 else if (ps.size() == 1){
113 assert(value(ps[0]) == l_Undef);
114 uncheckedEnqueue(ps[0]);
115 return ok = (propagate() == NULL);
117 Clause* c = Clause::Clause_new(ps, false);
126 void Solver::attachClause(Clause& c) {
127 assert(c.size() > 1);
128 watches[toInt(~c[0])].push(&c);
129 watches[toInt(~c[1])].push(&c);
130 if (c.learnt()) learnts_literals += c.size();
131 else clauses_literals += c.size(); }
134 void Solver::detachClause(Clause& c) {
135 assert(c.size() > 1);
136 assert(find(watches[toInt(~c[0])], &c));
137 assert(find(watches[toInt(~c[1])], &c));
138 remove(watches[toInt(~c[0])], &c);
139 remove(watches[toInt(~c[1])], &c);
140 if (c.learnt()) learnts_literals -= c.size();
141 else clauses_literals -= c.size(); }
144 void Solver::removeClause(Clause& c) {
149 bool Solver::satisfied(const Clause& c) const {
150 for (int i = 0; i < c.size(); i++)
151 if (value(c[i]) == l_True)
156 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
158 void Solver::cancelUntil(int level) {
159 if (decisionLevel() > level){
160 for (int c = trail.size()-1; c >= trail_lim[level]; c--){
161 Var x = var(trail[c]);
162 assigns[x] = toInt(l_Undef);
164 qhead = trail_lim[level];
165 trail.shrink(trail.size() - trail_lim[level]);
166 trail_lim.shrink(trail_lim.size() - level);
170 //=================================================================================================
174 Lit Solver::pickBranchLit(int polarity_mode, double random_var_freq)
176 Var next = var_Undef;
179 if (drand(random_seed) < random_var_freq && !order_heap.empty()){
180 next = order_heap[irand(random_seed,order_heap.size())];
181 if (toLbool(assigns[next]) == l_Undef && decision_var[next])
184 // Activity based decision:
185 while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next])
186 if (order_heap.empty()){
190 next = order_heap.removeMin();
193 switch (polarity_mode){
194 case polarity_true: sign = false; break;
195 case polarity_false: sign = true; break;
196 case polarity_user: sign = polarity[next]; break;
197 case polarity_rnd: sign = irand(random_seed, 2); break;
198 default: assert(false); }
200 return next == var_Undef ? lit_Undef : Lit(next, sign);
204 /*_________________________________________________________________________________________________
206 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
209 | Analyze conflict and produce a reason clause.
212 | * 'out_learnt' is assumed to be cleared.
213 | * Current decision level must be greater than root level.
216 | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
219 | Will undo part of the trail, upto but not beyond the assumption of the current decision level.
220 |________________________________________________________________________________________________@*/
221 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
226 // Generate conflict clause:
228 out_learnt.push(); // (leave room for the asserting literal)
229 int index = trail.size() - 1;
233 assert(confl != NULL); // (otherwise should be UIP)
239 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
242 if (!seen[var(q)] && level[var(q)] > 0){
243 varBumpActivity(var(q));
245 if (level[var(q)] >= decisionLevel())
249 if (level[var(q)] > out_btlevel)
250 out_btlevel = level[var(q)];
255 // Select next clause to look at:
256 while (!seen[var(trail[index--])]);
258 confl = reason[var(p)];
265 // Simplify conflict clause:
268 if (expensive_ccmin){
269 uint32_t abstract_level = 0;
270 for (i = 1; i < out_learnt.size(); i++)
271 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
273 out_learnt.copyTo(analyze_toclear);
274 for (i = j = 1; i < out_learnt.size(); i++)
275 if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level))
276 out_learnt[j++] = out_learnt[i];
278 out_learnt.copyTo(analyze_toclear);
279 for (i = j = 1; i < out_learnt.size(); i++){
280 Clause& c = *reason[var(out_learnt[i])];
281 for (int k = 1; k < c.size(); k++)
282 if (!seen[var(c[k])] && level[var(c[k])] > 0){
283 out_learnt[j++] = out_learnt[i];
287 max_literals += out_learnt.size();
288 out_learnt.shrink(i - j);
289 tot_literals += out_learnt.size();
291 // Find correct backtrack level:
293 if (out_learnt.size() == 1)
297 for (int i = 2; i < out_learnt.size(); i++)
298 if (level[var(out_learnt[i])] > level[var(out_learnt[max_i])])
300 Lit p = out_learnt[max_i];
301 out_learnt[max_i] = out_learnt[1];
303 out_btlevel = level[var(p)];
307 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
311 // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
312 // visiting literals at levels that cannot be removed later.
313 bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
315 analyze_stack.clear(); analyze_stack.push(p);
316 int top = analyze_toclear.size();
317 while (analyze_stack.size() > 0){
318 assert(reason[var(analyze_stack.last())] != NULL);
319 Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop();
321 for (int i = 1; i < c.size(); i++){
323 if (!seen[var(p)] && level[var(p)] > 0){
324 if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){
326 analyze_stack.push(p);
327 analyze_toclear.push(p);
329 for (int j = top; j < analyze_toclear.size(); j++)
330 seen[var(analyze_toclear[j])] = 0;
331 analyze_toclear.shrink(analyze_toclear.size() - top);
342 /*_________________________________________________________________________________________________
344 | analyzeFinal : (p : Lit) -> [void]
347 | Specialized analysis procedure to express the final conflict in terms of assumptions.
348 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
349 | stores the result in 'out_conflict'.
350 |________________________________________________________________________________________________@*/
351 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
353 out_conflict.clear();
354 out_conflict.push(p);
356 if (decisionLevel() == 0)
361 for (int i = trail.size()-1; i >= trail_lim[0]; i--){
362 Var x = var(trail[i]);
364 if (reason[x] == NULL){
365 assert(level[x] > 0);
366 out_conflict.push(~trail[i]);
368 Clause& c = *reason[x];
369 for (int j = 1; j < c.size(); j++)
370 if (level[var(c[j])] > 0)
381 void Solver::uncheckedEnqueue(Lit p, Clause* from)
383 assert(value(p) == l_Undef);
384 assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient
385 level [var(p)] = decisionLevel();
386 reason [var(p)] = from;
391 /*_________________________________________________________________________________________________
393 | propagate : [void] -> [Clause*]
396 | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
400 | * the propagation queue is empty, even if there was a conflict.
401 |________________________________________________________________________________________________@*/
402 Clause* Solver::propagate()
404 Clause* confl = NULL;
407 while (qhead < trail.size()){
408 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
409 vec<Clause*>& ws = watches[toInt(p)];
410 Clause **i, **j, **end;
413 for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){
416 // Make sure the false literal is data[1]:
418 if (c[0] == false_lit)
419 c[0] = c[1], c[1] = false_lit;
421 assert(c[1] == false_lit);
423 // If 0th watch is true, then clause is already satisfied.
425 if (value(first) == l_True){
428 // Look for new watch:
429 for (int k = 2; k < c.size(); k++)
430 if (value(c[k]) != l_False){
431 c[1] = c[k]; c[k] = false_lit;
432 watches[toInt(~c[1])].push(&c);
435 // Did not find watch -- clause is unit under assignment:
437 if (value(first) == l_False){
439 qhead = trail.size();
440 // Copy the remaining watches:
444 uncheckedEnqueue(first, &c);
450 propagations += num_props;
451 simpDB_props -= num_props;
456 /*_________________________________________________________________________________________________
458 | reduceDB : () -> [void]
461 | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
462 | clauses are clauses that are reason to some assignment. Binary clauses are never removed.
463 |________________________________________________________________________________________________@*/
464 struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
465 void Solver::reduceDB()
468 double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity
470 sort(learnts, reduceDB_lt());
471 for (i = j = 0; i < learnts.size() / 2; i++){
472 if (learnts[i]->size() > 2 && !locked(*learnts[i]))
473 removeClause(*learnts[i]);
475 learnts[j++] = learnts[i];
477 for (; i < learnts.size(); i++){
478 if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
479 removeClause(*learnts[i]);
481 learnts[j++] = learnts[i];
483 learnts.shrink(i - j);
487 void Solver::removeSatisfied(vec<Clause*>& cs)
490 for (i = j = 0; i < cs.size(); i++){
491 if (satisfied(*cs[i]))
492 removeClause(*cs[i]);
500 /*_________________________________________________________________________________________________
502 | simplify : [void] -> [bool]
505 | Simplify the clause database according to the current top-level assigment. Currently, the only
506 | thing done here is the removal of satisfied clauses, but more things can be put here.
507 |________________________________________________________________________________________________@*/
508 bool Solver::simplify()
510 assert(decisionLevel() == 0);
512 if (!ok || propagate() != NULL)
515 if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
518 // Remove satisfied clauses:
519 removeSatisfied(learnts);
520 if (remove_satisfied) // Can be turned off.
521 removeSatisfied(clauses);
523 // Remove fixed variables from the variable heap:
524 order_heap.filter(VarFilter(*this));
526 simpDB_assigns = nAssigns();
527 simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
533 /*_________________________________________________________________________________________________
535 | search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool]
538 | Search for a model the specified number of conflicts, keeping the number of learnt clauses
539 | below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
543 | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
544 | all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
545 | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
546 |________________________________________________________________________________________________@*/
547 lbool Solver::search(int nof_conflicts, int nof_learnts)
552 vec<Lit> learnt_clause;
559 Clause* confl = propagate();
562 conflicts++; conflictC++;
563 if (decisionLevel() == 0) return l_False;
567 learnt_clause.clear();
568 analyze(confl, learnt_clause, backtrack_level);
569 cancelUntil(backtrack_level);
570 assert(value(learnt_clause[0]) == l_Undef);
572 if (learnt_clause.size() == 1){
573 uncheckedEnqueue(learnt_clause[0]);
575 Clause* c = Clause::Clause_new(learnt_clause, true);
579 uncheckedEnqueue(learnt_clause[0], c);
588 if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
589 // Reached bound on number of conflicts:
590 progress_estimate = progressEstimate();
594 // Simplify the set of problem clauses:
595 if (decisionLevel() == 0 && !simplify())
598 if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
599 // Reduce the set of learnt clauses:
602 Lit next = lit_Undef;
603 while (decisionLevel() < assumptions.size()){
604 // Perform user provided assumption:
605 Lit p = assumptions[decisionLevel()];
606 if (value(p) == l_True){
607 // Dummy decision level:
609 }else if (value(p) == l_False){
610 analyzeFinal(~p, conflict);
618 if (next == lit_Undef){
619 // New variable decision:
621 next = pickBranchLit(polarity_mode, random_var_freq);
623 if (next == lit_Undef)
628 // Increase decision level and enqueue 'next'
629 assert(value(next) == l_Undef);
631 uncheckedEnqueue(next);
637 double Solver::progressEstimate() const
640 double F = 1.0 / nVars();
642 for (int i = 0; i <= decisionLevel(); i++){
643 int beg = i == 0 ? 0 : trail_lim[i - 1];
644 int end = i == decisionLevel() ? trail.size() : trail_lim[i];
645 progress += pow(F, i) * (end - beg);
648 return progress / nVars();
652 bool Solver::solve(const vec<Lit>& assumps)
657 if (!ok) return false;
659 assumps.copyTo(assumptions);
661 double nof_conflicts = restart_first;
662 double nof_learnts = nClauses() * learntsize_factor;
663 lbool status = l_Undef;
666 reportf("============================[ Search Statistics ]==============================\n");
667 reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
668 reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
669 reportf("===============================================================================\n");
673 while (status == l_Undef){
675 reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout);
676 status = search((int)nof_conflicts, (int)nof_learnts);
677 nof_conflicts *= restart_inc;
678 nof_learnts *= learntsize_inc;
682 reportf("===============================================================================\n");
685 if (status == l_True){
686 // Extend & copy model:
687 model.growTo(nVars());
688 for (int i = 0; i < nVars(); i++) model[i] = value(i);
693 assert(status == l_False);
694 if (conflict.size() == 0)
699 return status == l_True;
702 //=================================================================================================
706 void Solver::verifyModel()
709 for (int i = 0; i < clauses.size(); i++){
710 assert(clauses[i]->mark() == 0);
711 Clause& c = *clauses[i];
712 for (int j = 0; j < c.size(); j++)
713 if (modelValue(c[j]) == l_True)
716 reportf("unsatisfied clause: ");
717 printClause(*clauses[i]);
725 reportf("Verified %d original clauses.\n", clauses.size());
729 void Solver::checkLiteralCount()
731 // Check that sizes are calculated correctly:
733 for (int i = 0; i < clauses.size(); i++)
734 if (clauses[i]->mark() == 0)
735 cnt += clauses[i]->size();
737 if ((int)clauses_literals != cnt){
738 fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt);
739 assert((int)clauses_literals == cnt);