| #ifndef __STDC_FORMAT_MACROS | |
| #define __STDC_FORMAT_MACROS | |
| #endif | |
| #ifndef __STDC_LIMIT_MACROS | |
| #define __STDC_LIMIT_MACROS | |
| #endif | |
| /***************************************************************************************[Solver.cc] | |
| Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson | |
| Copyright (c) 2007-2010, Niklas Sorensson | |
| Permission is hereby granted, free of charge, to any person obtaining a copy of this software and | |
| associated documentation files (the "Software"), to deal in the Software without restriction, | |
| including without limitation the rights to use, copy, modify, merge, publish, distribute, | |
| sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is | |
| furnished to do so, subject to the following conditions: | |
| The above copyright notice and this permission notice shall be included in all copies or | |
| substantial portions of the Software. | |
| THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT | |
| NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND | |
| NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, | |
| DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT | |
| OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. | |
| **************************************************************************************************/ | |
| #include <math.h> | |
| #include "Alg.h" | |
| #include "Sort.h" | |
| #include "System.h" | |
| #include "Solver.h" | |
| using namespace Minisat; | |
| //================================================================================================= | |
| // Options: | |
| static const char* _cat = "CORE"; | |
| static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); | |
| static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); | |
| 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)); | |
| static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); | |
| static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2)); | |
| static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); | |
| static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); | |
| static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); | |
| static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); | |
| static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false)); | |
| 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)); | |
| static IntOption opt_min_learnts_lim (_cat, "min-learnts", "Minimum learnt clause limit", 0, IntRange(0, INT32_MAX)); | |
| //================================================================================================= | |
| // Constructor/Destructor: | |
| Solver::Solver() : | |
| // Parameters (user settable): | |
| // | |
| verbosity (0) | |
| , var_decay (opt_var_decay) | |
| , clause_decay (opt_clause_decay) | |
| , random_var_freq (opt_random_var_freq) | |
| , random_seed (opt_random_seed) | |
| , luby_restart (opt_luby_restart) | |
| , ccmin_mode (opt_ccmin_mode) | |
| , phase_saving (opt_phase_saving) | |
| , rnd_pol (false) | |
| , rnd_init_act (opt_rnd_init_act) | |
| , garbage_frac (opt_garbage_frac) | |
| , min_learnts_lim (opt_min_learnts_lim) | |
| , restart_first (opt_restart_first) | |
| , restart_inc (opt_restart_inc) | |
| // Parameters (the rest): | |
| // | |
| , learntsize_factor((double)1/(double)3), learntsize_inc(1.1) | |
| // Parameters (experimental): | |
| // | |
| , learntsize_adjust_start_confl (100) | |
| , learntsize_adjust_inc (1.5) | |
| // Statistics: (formerly in 'SolverStats') | |
| // | |
| , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) | |
| , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) | |
| , watches (WatcherDeleted(ca)) | |
| , order_heap (VarOrderLt(activity)) | |
| , ok (true) | |
| , cla_inc (1) | |
| , var_inc (1) | |
| , qhead (0) | |
| , simpDB_assigns (-1) | |
| , simpDB_props (0) | |
| , progress_estimate (0) | |
| , remove_satisfied (true) | |
| , next_var (0) | |
| // Resource constraints: | |
| // | |
| , conflict_budget (-1) | |
| , propagation_budget (-1) | |
| , asynch_interrupt (false) | |
| {} | |
| Solver::~Solver() | |
| { | |
| } | |
| //================================================================================================= | |
| // Minor methods: | |
| // Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be | |
| // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). | |
| // | |
| Var Solver::newVar(lbool upol, bool dvar) | |
| { | |
| Var v; | |
| if (free_vars.size() > 0){ | |
| v = free_vars.last(); | |
| free_vars.pop(); | |
| }else | |
| v = next_var++; | |
| watches .init(mkLit(v, false)); | |
| watches .init(mkLit(v, true )); | |
| assigns .insert(v, l_Undef); | |
| vardata .insert(v, mkVarData(CRef_Undef, 0)); | |
| activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0); | |
| seen .insert(v, 0); | |
| polarity .insert(v, true); | |
| user_pol .insert(v, upol); | |
| decision .reserve(v); | |
| trail .capacity(v+1); | |
| setDecisionVar(v, dvar); | |
| return v; | |
| } | |
| // Note: at the moment, only unassigned variable will be released (this is to avoid duplicate | |
| // releases of the same variable). | |
| void Solver::releaseVar(Lit l) | |
| { | |
| if (value(l) == l_Undef){ | |
| addClause(l); | |
| released_vars.push(var(l)); | |
| } | |
| } | |
| bool Solver::addClause_(vec<Lit>& ps) | |
| { | |
| assert(decisionLevel() == 0); | |
| if (!ok) return false; | |
| // Check if clause is satisfied and remove false/duplicate literals: | |
| sort(ps); | |
| Lit p; int i, j; | |
| for (i = j = 0, p = lit_Undef; i < ps.size(); i++) | |
| if (value(ps[i]) == l_True || ps[i] == ~p) | |
| return true; | |
| else if (value(ps[i]) != l_False && ps[i] != p) | |
| ps[j++] = p = ps[i]; | |
| ps.shrink(i - j); | |
| if (ps.size() == 0) | |
| return ok = false; | |
| else if (ps.size() == 1){ | |
| uncheckedEnqueue(ps[0]); | |
| return ok = (propagate() == CRef_Undef); | |
| }else{ | |
| CRef cr = ca.alloc(ps, false); | |
| clauses.push(cr); | |
| attachClause(cr); | |
| } | |
| return true; | |
| } | |
| void Solver::attachClause(CRef cr){ | |
| const Clause& c = ca[cr]; | |
| assert(c.size() > 1); | |
| watches[~c[0]].push(Watcher(cr, c[1])); | |
| watches[~c[1]].push(Watcher(cr, c[0])); | |
| if (c.learnt()) num_learnts++, learnts_literals += c.size(); | |
| else num_clauses++, clauses_literals += c.size(); | |
| } | |
| void Solver::detachClause(CRef cr, bool strict){ | |
| const Clause& c = ca[cr]; | |
| assert(c.size() > 1); | |
| // Strict or lazy detaching: | |
| if (strict){ | |
| remove(watches[~c[0]], Watcher(cr, c[1])); | |
| remove(watches[~c[1]], Watcher(cr, c[0])); | |
| }else{ | |
| watches.smudge(~c[0]); | |
| watches.smudge(~c[1]); | |
| } | |
| if (c.learnt()) num_learnts--, learnts_literals -= c.size(); | |
| else num_clauses--, clauses_literals -= c.size(); | |
| } | |
| void Solver::removeClause(CRef cr) { | |
| Clause& c = ca[cr]; | |
| detachClause(cr); | |
| // Don't leave pointers to free'd memory! | |
| if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; | |
| c.mark(1); | |
| ca.free(cr); | |
| } | |
| bool Solver::satisfied(const Clause& c) const { | |
| for (int i = 0; i < c.size(); i++) | |
| if (value(c[i]) == l_True) | |
| return true; | |
| return false; } | |
| // Revert to the state at given level (keeping all assignment at 'level' but not beyond). | |
| // | |
| void Solver::cancelUntil(int level) { | |
| if (decisionLevel() > level){ | |
| for (int c = trail.size()-1; c >= trail_lim[level]; c--){ | |
| Var x = var(trail[c]); | |
| assigns [x] = l_Undef; | |
| if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) | |
| polarity[x] = sign(trail[c]); | |
| insertVarOrder(x); } | |
| qhead = trail_lim[level]; | |
| trail.shrink(trail.size() - trail_lim[level]); | |
| trail_lim.shrink(trail_lim.size() - level); | |
| } } | |
| //================================================================================================= | |
| // Major methods: | |
| Lit Solver::pickBranchLit() | |
| { | |
| Var next = var_Undef; | |
| // Random decision: | |
| if (drand(random_seed) < random_var_freq && !order_heap.empty()){ | |
| next = order_heap[irand(random_seed,order_heap.size())]; | |
| if (value(next) == l_Undef && decision[next]) | |
| rnd_decisions++; } | |
| // Activity based decision: | |
| while (next == var_Undef || value(next) != l_Undef || !decision[next]) | |
| if (order_heap.empty()){ | |
| next = var_Undef; | |
| break; | |
| }else | |
| next = order_heap.removeMin(); | |
| // Choose polarity based on different polarity modes (global or per-variable): | |
| if (next == var_Undef) | |
| return lit_Undef; | |
| else if (user_pol[next] != l_Undef) | |
| return mkLit(next, user_pol[next] == l_True); | |
| else if (rnd_pol) | |
| return mkLit(next, drand(random_seed) < 0.5); | |
| else | |
| return mkLit(next, polarity[next]); | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] | |
| | | |
| | Description: | |
| | Analyze conflict and produce a reason clause. | |
| | | |
| | Pre-conditions: | |
| | * 'out_learnt' is assumed to be cleared. | |
| | * Current decision level must be greater than root level. | |
| | | |
| | Post-conditions: | |
| | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. | |
| | * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the | |
| | rest of literals. There may be others from the same level though. | |
| | | |
| |________________________________________________________________________________________________@*/ | |
| void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) | |
| { | |
| int pathC = 0; | |
| Lit p = lit_Undef; | |
| // Generate conflict clause: | |
| // | |
| out_learnt.push(); // (leave room for the asserting literal) | |
| int index = trail.size() - 1; | |
| do{ | |
| assert(confl != CRef_Undef); // (otherwise should be UIP) | |
| Clause& c = ca[confl]; | |
| if (c.learnt()) | |
| claBumpActivity(c); | |
| for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ | |
| Lit q = c[j]; | |
| if (!seen[var(q)] && level(var(q)) > 0){ | |
| varBumpActivity(var(q)); | |
| seen[var(q)] = 1; | |
| if (level(var(q)) >= decisionLevel()) | |
| pathC++; | |
| else | |
| out_learnt.push(q); | |
| } | |
| } | |
| // Select next clause to look at: | |
| while (!seen[var(trail[index--])]); | |
| p = trail[index+1]; | |
| confl = reason(var(p)); | |
| seen[var(p)] = 0; | |
| pathC--; | |
| }while (pathC > 0); | |
| out_learnt[0] = ~p; | |
| // Simplify conflict clause: | |
| // | |
| int i, j; | |
| out_learnt.copyTo(analyze_toclear); | |
| if (ccmin_mode == 2){ | |
| for (i = j = 1; i < out_learnt.size(); i++) | |
| if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i])) | |
| out_learnt[j++] = out_learnt[i]; | |
| }else if (ccmin_mode == 1){ | |
| for (i = j = 1; i < out_learnt.size(); i++){ | |
| Var x = var(out_learnt[i]); | |
| if (reason(x) == CRef_Undef) | |
| out_learnt[j++] = out_learnt[i]; | |
| else{ | |
| Clause& c = ca[reason(var(out_learnt[i]))]; | |
| for (int k = 1; k < c.size(); k++) | |
| if (!seen[var(c[k])] && level(var(c[k])) > 0){ | |
| out_learnt[j++] = out_learnt[i]; | |
| break; } | |
| } | |
| } | |
| }else | |
| i = j = out_learnt.size(); | |
| max_literals += out_learnt.size(); | |
| out_learnt.shrink(i - j); | |
| tot_literals += out_learnt.size(); | |
| // Find correct backtrack level: | |
| // | |
| if (out_learnt.size() == 1) | |
| out_btlevel = 0; | |
| else{ | |
| int max_i = 1; | |
| // Find the first literal assigned at the next-highest level: | |
| for (int i = 2; i < out_learnt.size(); i++) | |
| if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) | |
| max_i = i; | |
| // Swap-in this literal at index 1: | |
| Lit p = out_learnt[max_i]; | |
| out_learnt[max_i] = out_learnt[1]; | |
| out_learnt[1] = p; | |
| out_btlevel = level(var(p)); | |
| } | |
| for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) | |
| } | |
| // Check if 'p' can be removed from a conflict clause. | |
| bool Solver::litRedundant(Lit p) | |
| { | |
| enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 }; | |
| assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source); | |
| assert(reason(var(p)) != CRef_Undef); | |
| Clause* c = &ca[reason(var(p))]; | |
| vec<ShrinkStackElem>& stack = analyze_stack; | |
| stack.clear(); | |
| for (uint32_t i = 1; ; i++){ | |
| if (i < (uint32_t)c->size()){ | |
| // Checking 'p'-parents 'l': | |
| Lit l = (*c)[i]; | |
| // Variable at level 0 or previously removable: | |
| if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){ | |
| continue; } | |
| // Check variable can not be removed for some local reason: | |
| if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){ | |
| stack.push(ShrinkStackElem(0, p)); | |
| for (int i = 0; i < stack.size(); i++) | |
| if (seen[var(stack[i].l)] == seen_undef){ | |
| seen[var(stack[i].l)] = seen_failed; | |
| analyze_toclear.push(stack[i].l); | |
| } | |
| return false; | |
| } | |
| // Recursively check 'l': | |
| stack.push(ShrinkStackElem(i, p)); | |
| i = 0; | |
| p = l; | |
| c = &ca[reason(var(p))]; | |
| }else{ | |
| // Finished with current element 'p' and reason 'c': | |
| if (seen[var(p)] == seen_undef){ | |
| seen[var(p)] = seen_removable; | |
| analyze_toclear.push(p); | |
| } | |
| // Terminate with success if stack is empty: | |
| if (stack.size() == 0) break; | |
| // Continue with top element on stack: | |
| i = stack.last().i; | |
| p = stack.last().l; | |
| c = &ca[reason(var(p))]; | |
| stack.pop(); | |
| } | |
| } | |
| return true; | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | analyzeFinal : (p : Lit) -> [void] | |
| | | |
| | Description: | |
| | Specialized analysis procedure to express the final conflict in terms of assumptions. | |
| | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and | |
| | stores the result in 'out_conflict'. | |
| |________________________________________________________________________________________________@*/ | |
| void Solver::analyzeFinal(Lit p, LSet& out_conflict) | |
| { | |
| out_conflict.clear(); | |
| out_conflict.insert(p); | |
| if (decisionLevel() == 0) | |
| return; | |
| seen[var(p)] = 1; | |
| for (int i = trail.size()-1; i >= trail_lim[0]; i--){ | |
| Var x = var(trail[i]); | |
| if (seen[x]){ | |
| if (reason(x) == CRef_Undef){ | |
| assert(level(x) > 0); | |
| out_conflict.insert(~trail[i]); | |
| }else{ | |
| Clause& c = ca[reason(x)]; | |
| for (int j = 1; j < c.size(); j++) | |
| if (level(var(c[j])) > 0) | |
| seen[var(c[j])] = 1; | |
| } | |
| seen[x] = 0; | |
| } | |
| } | |
| seen[var(p)] = 0; | |
| } | |
| void Solver::uncheckedEnqueue(Lit p, CRef from) | |
| { | |
| assert(value(p) == l_Undef); | |
| assigns[var(p)] = lbool(!sign(p)); | |
| vardata[var(p)] = mkVarData(from, decisionLevel()); | |
| trail.push_(p); | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | propagate : [void] -> [Clause*] | |
| | | |
| | Description: | |
| | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, | |
| | otherwise CRef_Undef. | |
| | | |
| | Post-conditions: | |
| | * the propagation queue is empty, even if there was a conflict. | |
| |________________________________________________________________________________________________@*/ | |
| CRef Solver::propagate() | |
| { | |
| CRef confl = CRef_Undef; | |
| int num_props = 0; | |
| while (qhead < trail.size()){ | |
| Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. | |
| vec<Watcher>& ws = watches.lookup(p); | |
| Watcher *i, *j, *end; | |
| num_props++; | |
| for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ | |
| // Try to avoid inspecting the clause: | |
| Lit blocker = i->blocker; | |
| if (value(blocker) == l_True){ | |
| *j++ = *i++; continue; } | |
| // Make sure the false literal is data[1]: | |
| CRef cr = i->cref; | |
| Clause& c = ca[cr]; | |
| Lit false_lit = ~p; | |
| if (c[0] == false_lit) | |
| c[0] = c[1], c[1] = false_lit; | |
| assert(c[1] == false_lit); | |
| i++; | |
| // If 0th watch is true, then clause is already satisfied. | |
| Lit first = c[0]; | |
| Watcher w = Watcher(cr, first); | |
| if (first != blocker && value(first) == l_True){ | |
| *j++ = w; continue; } | |
| // Look for new watch: | |
| for (int k = 2; k < c.size(); k++) | |
| if (value(c[k]) != l_False){ | |
| c[1] = c[k]; c[k] = false_lit; | |
| watches[~c[1]].push(w); | |
| goto NextClause; } | |
| // Did not find watch -- clause is unit under assignment: | |
| *j++ = w; | |
| if (value(first) == l_False){ | |
| confl = cr; | |
| qhead = trail.size(); | |
| // Copy the remaining watches: | |
| while (i < end) | |
| *j++ = *i++; | |
| }else | |
| uncheckedEnqueue(first, cr); | |
| NextClause:; | |
| } | |
| ws.shrink(i - j); | |
| } | |
| propagations += num_props; | |
| simpDB_props -= num_props; | |
| return confl; | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | reduceDB : () -> [void] | |
| | | |
| | Description: | |
| | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | |
| | clauses are clauses that are reason to some assignment. Binary clauses are never removed. | |
| |________________________________________________________________________________________________@*/ | |
| struct reduceDB_lt { | |
| ClauseAllocator& ca; | |
| reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} | |
| bool operator () (CRef x, CRef y) { | |
| return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } | |
| }; | |
| void Solver::reduceDB() | |
| { | |
| int i, j; | |
| double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity | |
| sort(learnts, reduceDB_lt(ca)); | |
| // Don't delete binary or locked clauses. From the rest, delete clauses from the first half | |
| // and clauses with activity smaller than 'extra_lim': | |
| for (i = j = 0; i < learnts.size(); i++){ | |
| Clause& c = ca[learnts[i]]; | |
| if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) | |
| removeClause(learnts[i]); | |
| else | |
| learnts[j++] = learnts[i]; | |
| } | |
| learnts.shrink(i - j); | |
| checkGarbage(); | |
| } | |
| void Solver::removeSatisfied(vec<CRef>& cs) | |
| { | |
| int i, j; | |
| for (i = j = 0; i < cs.size(); i++){ | |
| Clause& c = ca[cs[i]]; | |
| if (satisfied(c)) | |
| removeClause(cs[i]); | |
| else{ | |
| // Trim clause: | |
| assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef); | |
| for (int k = 2; k < c.size(); k++) | |
| if (value(c[k]) == l_False){ | |
| c[k--] = c[c.size()-1]; | |
| c.pop(); | |
| } | |
| cs[j++] = cs[i]; | |
| } | |
| } | |
| cs.shrink(i - j); | |
| } | |
| void Solver::rebuildOrderHeap() | |
| { | |
| vec<Var> vs; | |
| for (Var v = 0; v < nVars(); v++) | |
| if (decision[v] && value(v) == l_Undef) | |
| vs.push(v); | |
| order_heap.build(vs); | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | simplify : [void] -> [bool] | |
| | | |
| | Description: | |
| | Simplify the clause database according to the current top-level assigment. Currently, the only | |
| | thing done here is the removal of satisfied clauses, but more things can be put here. | |
| |________________________________________________________________________________________________@*/ | |
| bool Solver::simplify() | |
| { | |
| assert(decisionLevel() == 0); | |
| if (!ok || propagate() != CRef_Undef) | |
| return ok = false; | |
| if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) | |
| return true; | |
| // Remove satisfied clauses: | |
| removeSatisfied(learnts); | |
| if (remove_satisfied){ // Can be turned off. | |
| removeSatisfied(clauses); | |
| // TODO: what todo in if 'remove_satisfied' is false? | |
| // Remove all released variables from the trail: | |
| for (int i = 0; i < released_vars.size(); i++){ | |
| assert(seen[released_vars[i]] == 0); | |
| seen[released_vars[i]] = 1; | |
| } | |
| int i, j; | |
| for (i = j = 0; i < trail.size(); i++) | |
| if (seen[var(trail[i])] == 0) | |
| trail[j++] = trail[i]; | |
| trail.shrink(i - j); | |
| //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead); | |
| qhead = trail.size(); | |
| for (int i = 0; i < released_vars.size(); i++) | |
| seen[released_vars[i]] = 0; | |
| // Released variables are now ready to be reused: | |
| append(released_vars, free_vars); | |
| released_vars.clear(); | |
| } | |
| checkGarbage(); | |
| rebuildOrderHeap(); | |
| simpDB_assigns = nAssigns(); | |
| simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) | |
| return true; | |
| } | |
| /*_________________________________________________________________________________________________ | |
| | | |
| | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] | |
| | | |
| | Description: | |
| | Search for a model the specified number of conflicts. | |
| | NOTE! Use negative value for 'nof_conflicts' indicate infinity. | |
| | | |
| | Output: | |
| | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If | |
| | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' | |
| | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. | |
| |________________________________________________________________________________________________@*/ | |
| lbool Solver::search(int nof_conflicts) | |
| { | |
| assert(ok); | |
| int backtrack_level; | |
| int conflictC = 0; | |
| vec<Lit> learnt_clause; | |
| starts++; | |
| for (;;){ | |
| CRef confl = propagate(); | |
| if (confl != CRef_Undef){ | |
| // CONFLICT | |
| conflicts++; conflictC++; | |
| if (decisionLevel() == 0) return l_False; | |
| learnt_clause.clear(); | |
| analyze(confl, learnt_clause, backtrack_level); | |
| cancelUntil(backtrack_level); | |
| if (learnt_clause.size() == 1){ | |
| uncheckedEnqueue(learnt_clause[0]); | |
| }else{ | |
| CRef cr = ca.alloc(learnt_clause, true); | |
| learnts.push(cr); | |
| attachClause(cr); | |
| claBumpActivity(ca[cr]); | |
| uncheckedEnqueue(learnt_clause[0], cr); | |
| } | |
| varDecayActivity(); | |
| claDecayActivity(); | |
| if (--learntsize_adjust_cnt == 0){ | |
| learntsize_adjust_confl *= learntsize_adjust_inc; | |
| learntsize_adjust_cnt = (int)learntsize_adjust_confl; | |
| max_learnts *= learntsize_inc; | |
| if (verbosity >= 1) | |
| printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", | |
| (int)conflicts, | |
| (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, | |
| (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); | |
| } | |
| }else{ | |
| // NO CONFLICT | |
| if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){ | |
| // Reached bound on number of conflicts: | |
| progress_estimate = progressEstimate(); | |
| cancelUntil(0); | |
| return l_Undef; } | |
| // Simplify the set of problem clauses: | |
| if (decisionLevel() == 0 && !simplify()) | |
| return l_False; | |
| if (learnts.size()-nAssigns() >= max_learnts) | |
| // Reduce the set of learnt clauses: | |
| reduceDB(); | |
| Lit next = lit_Undef; | |
| while (decisionLevel() < assumptions.size()){ | |
| // Perform user provided assumption: | |
| Lit p = assumptions[decisionLevel()]; | |
| if (value(p) == l_True){ | |
| // Dummy decision level: | |
| newDecisionLevel(); | |
| }else if (value(p) == l_False){ | |
| analyzeFinal(~p, conflict); | |
| return l_False; | |
| }else{ | |
| next = p; | |
| break; | |
| } | |
| } | |
| if (next == lit_Undef){ | |
| // New variable decision: | |
| decisions++; | |
| next = pickBranchLit(); | |
| if (next == lit_Undef) | |
| // Model found: | |
| return l_True; | |
| } | |
| // Increase decision level and enqueue 'next' | |
| newDecisionLevel(); | |
| uncheckedEnqueue(next); | |
| } | |
| } | |
| } | |
| double Solver::progressEstimate() const | |
| { | |
| double progress = 0; | |
| double F = 1.0 / nVars(); | |
| for (int i = 0; i <= decisionLevel(); i++){ | |
| int beg = i == 0 ? 0 : trail_lim[i - 1]; | |
| int end = i == decisionLevel() ? trail.size() : trail_lim[i]; | |
| progress += pow(F, i) * (end - beg); | |
| } | |
| return progress / nVars(); | |
| } | |
| /* | |
| Finite subsequences of the Luby-sequence: | |
| 0: 1 | |
| 1: 1 1 2 | |
| 2: 1 1 2 1 1 2 4 | |
| 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 | |
| ... | |
| */ | |
| static double luby(double y, int x){ | |
| // Find the finite subsequence that contains index 'x', and the | |
| // size of that subsequence: | |
| int size, seq; | |
| for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1); | |
| while (size-1 != x){ | |
| size = (size-1)>>1; | |
| seq--; | |
| x = x % size; | |
| } | |
| return pow(y, seq); | |
| } | |
| // NOTE: assumptions passed in member-variable 'assumptions'. | |
| lbool Solver::solve_() | |
| { | |
| model.clear(); | |
| conflict.clear(); | |
| if (!ok) return l_False; | |
| solves++; | |
| max_learnts = nClauses() * learntsize_factor; | |
| if (max_learnts < min_learnts_lim) | |
| max_learnts = min_learnts_lim; | |
| learntsize_adjust_confl = learntsize_adjust_start_confl; | |
| learntsize_adjust_cnt = (int)learntsize_adjust_confl; | |
| lbool status = l_Undef; | |
| if (verbosity >= 1){ | |
| printf("============================[ Search Statistics ]==============================\n"); | |
| printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); | |
| printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); | |
| printf("===============================================================================\n"); | |
| } | |
| // Search: | |
| int curr_restarts = 0; | |
| while (status == l_Undef){ | |
| double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); | |
| status = search(rest_base * restart_first); | |
| if (!withinBudget()) break; | |
| curr_restarts++; | |
| } | |
| if (verbosity >= 1) | |
| printf("===============================================================================\n"); | |
| if (status == l_True){ | |
| // Extend & copy model: | |
| model.growTo(nVars()); | |
| for (int i = 0; i < nVars(); i++) model[i] = value(i); | |
| }else if (status == l_False && conflict.size() == 0) | |
| ok = false; | |
| cancelUntil(0); | |
| return status; | |
| } | |
| bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out) | |
| { | |
| trail_lim.push(trail.size()); | |
| for (int i = 0; i < assumps.size(); i++){ | |
| Lit a = assumps[i]; | |
| if (value(a) == l_False){ | |
| cancelUntil(0); | |
| return false; | |
| }else if (value(a) == l_Undef) | |
| uncheckedEnqueue(a); | |
| } | |
| unsigned trail_before = trail.size(); | |
| bool ret = true; | |
| if (propagate() == CRef_Undef){ | |
| out.clear(); | |
| for (int j = trail_before; j < trail.size(); j++) | |
| out.push(trail[j]); | |
| }else | |
| ret = false; | |
| cancelUntil(0); | |
| return ret; | |
| } | |
| //================================================================================================= | |
| // Writing CNF to DIMACS: | |
| // | |
| // FIXME: this needs to be rewritten completely. | |
| static Var mapVar(Var x, vec<Var>& map, Var& max) | |
| { | |
| if (map.size() <= x || map[x] == -1){ | |
| map.growTo(x+1, -1); | |
| map[x] = max++; | |
| } | |
| return map[x]; | |
| } | |
| void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max) | |
| { | |
| if (satisfied(c)) return; | |
| for (int i = 0; i < c.size(); i++) | |
| if (value(c[i]) != l_False) | |
| fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1); | |
| fprintf(f, "0\n"); | |
| } | |
| void Solver::toDimacs(const char *file, const vec<Lit>& assumps) | |
| { | |
| FILE* f = fopen(file, "wr"); | |
| if (f == NULL) | |
| fprintf(stderr, "could not open file %s\n", file), exit(1); | |
| toDimacs(f, assumps); | |
| fclose(f); | |
| } | |
| void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) | |
| { | |
| // Handle case when solver is in contradictory state: | |
| if (!ok){ | |
| fprintf(f, "p cnf 1 2\n1 0\n-1 0\n"); | |
| return; } | |
| vec<Var> map; Var max = 0; | |
| // Cannot use removeClauses here because it is not safe | |
| // to deallocate them at this point. Could be improved. | |
| int cnt = 0; | |
| for (int i = 0; i < clauses.size(); i++) | |
| if (!satisfied(ca[clauses[i]])) | |
| cnt++; | |
| for (int i = 0; i < clauses.size(); i++) | |
| if (!satisfied(ca[clauses[i]])){ | |
| Clause& c = ca[clauses[i]]; | |
| for (int j = 0; j < c.size(); j++) | |
| if (value(c[j]) != l_False) | |
| mapVar(var(c[j]), map, max); | |
| } | |
| // Assumptions are added as unit clauses: | |
| cnt += assumps.size(); | |
| fprintf(f, "p cnf %d %d\n", max, cnt); | |
| for (int i = 0; i < assumps.size(); i++){ | |
| assert(value(assumps[i]) != l_False); | |
| fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1); | |
| } | |
| for (int i = 0; i < clauses.size(); i++) | |
| toDimacs(f, ca[clauses[i]], map, max); | |
| if (verbosity > 0) | |
| printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt); | |
| } | |
| void Solver::printStats() const | |
| { | |
| double cpu_time = cpuTime(); | |
| double mem_used = memUsedPeak(); | |
| printf("restarts : %" PRIu64 "\n", starts); | |
| printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time); | |
| printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); | |
| printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time); | |
| printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); | |
| if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); | |
| printf("CPU time : %g s\n", cpu_time); | |
| } | |
| //================================================================================================= | |
| // Garbage Collection methods: | |
| void Solver::relocAll(ClauseAllocator& to) | |
| { | |
| // All watchers: | |
| // | |
| watches.cleanAll(); | |
| for (int v = 0; v < nVars(); v++) | |
| for (int s = 0; s < 2; s++){ | |
| Lit p = mkLit(v, s); | |
| vec<Watcher>& ws = watches[p]; | |
| for (int j = 0; j < ws.size(); j++) | |
| ca.reloc(ws[j].cref, to); | |
| } | |
| // All reasons: | |
| // | |
| for (int i = 0; i < trail.size(); i++){ | |
| Var v = var(trail[i]); | |
| // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep | |
| // 'dangling' reasons here. It is safe and does not hurt. | |
| if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){ | |
| assert(!isRemoved(reason(v))); | |
| ca.reloc(vardata[v].reason, to); | |
| } | |
| } | |
| // All learnt: | |
| // | |
| int i, j; | |
| for (i = j = 0; i < learnts.size(); i++) | |
| if (!isRemoved(learnts[i])){ | |
| ca.reloc(learnts[i], to); | |
| learnts[j++] = learnts[i]; | |
| } | |
| learnts.shrink(i - j); | |
| // All original: | |
| // | |
| for (i = j = 0; i < clauses.size(); i++) | |
| if (!isRemoved(clauses[i])){ | |
| ca.reloc(clauses[i], to); | |
| clauses[j++] = clauses[i]; | |
| } | |
| clauses.shrink(i - j); | |
| } | |
| void Solver::garbageCollect() | |
| { | |
| // Initialize the next region to a size corresponding to the estimated utilization degree. This | |
| // is not precise but should avoid some unnecessary reallocations for the new region: | |
| ClauseAllocator to(ca.size() - ca.wasted()); | |
| relocAll(to); | |
| if (verbosity >= 2) | |
| printf("| Garbage collection: %12d bytes => %12d bytes |\n", | |
| ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); | |
| to.moveTo(ca); | |
| } |