From c7263309fca42e084345a2e36492d9c510bdfca7 Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Thu, 23 Jan 2020 15:06:38 +0800 Subject: [PATCH 1/5] Showing number of decisions taken by CBT and NCBT --- minisat/core/Solver.cc | 3 +++ minisat/core/Solver.h | 1 + 2 files changed, 4 insertions(+) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 663e9573..94c08351 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -217,6 +217,7 @@ Solver::Solver() , VSIDS_propagations(opt_vsids_p) , reactivate_VSIDS(false) + , CBT(false) , ok(true) , cla_inc(1) , var_inc(1) @@ -1982,10 +1983,12 @@ lbool Solver::search(int &nof_conflicts) if ((confl_to_chrono < 0 || confl_to_chrono <= (int64_t)conflicts) && chrono > -1 && (decisionLevel() - backtrack_level) >= chrono) { ++chrono_backtrack; + CBT = true; cancelUntil(data.nHighestLevel - 1); } else // default behavior { ++non_chrono_backtrack; + CBT = false; cancelUntil(backtrack_level); } diff --git a/minisat/core/Solver.h b/minisat/core/Solver.h index 1c85ce77..7cc718ed 100644 --- a/minisat/core/Solver.h +++ b/minisat/core/Solver.h @@ -231,6 +231,7 @@ class Solver uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, conflicts_VSIDS; uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; uint64_t chrono_backtrack, non_chrono_backtrack; + bool CBT; vec picked; vec conflicted; From b1e989ded13ebeb55726e5130424f6510fbc58e6 Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Thu, 23 Jan 2020 15:12:12 +0800 Subject: [PATCH 2/5] Putting LSIDS to Devel (#3) * Minimal LSIDS * Bump for non-VSIDS section, Decaying * bump lit scores during cancelUntil * Creating lit_decay --- minisat/core/Solver.cc | 50 +++++++++++++++++++++++++++++++++++++++--- minisat/core/Solver.h | 37 ++++++++++++++++++++++++++++++- 2 files changed, 83 insertions(+), 4 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 94c08351..b298e4f8 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -111,6 +111,16 @@ static Int64Option opt_VSIDS_props_init_limit(_cat, "specifies the number of propagations before we start with LRB.", 10000, Int64Range(1, INT64_MAX)); +static const char *cat2 = "LSIDS"; + +static DoubleOption opt_lsids_phase(cat2, + "lsids-pick", + "Use LSIDS for phase selection. p : when diff between the literal activity is p " + "high then choose LSIDS, else polarity caching.", + 0.5, + DoubleRange(0, true, 1, true)); +static DoubleOption opt_lsids_erase_weight(cat2, "lsids-erase-weight", "Weight for LSIDS bump", 2.0, DoubleRange(0, true, 5, true)); + static DoubleOption opt_inprocessing_inc(_cat, "inprocess-delay", "Use this factor to wait for next inprocessing (0=off)", @@ -167,7 +177,9 @@ Solver::Solver() , step_size_dec(opt_step_size_dec) , min_step_size(opt_min_step_size) , timer(5000) + , timer_lit(5000) , var_decay(opt_var_decay) + , lit_decay(opt_var_decay) , clause_decay(opt_clause_decay) , random_var_freq(opt_random_var_freq) , random_seed(opt_random_seed) @@ -190,6 +202,8 @@ Solver::Solver() , learntsize_adjust_start_confl(100) , learntsize_adjust_inc(1.5) + , lsids_pick(opt_lsids_phase) + , lsids_erase_bump_weight(opt_lsids_erase_weight) // Statistics: (formerly in 'SolverStats') // , solves(0) @@ -221,6 +235,7 @@ Solver::Solver() , ok(true) , cla_inc(1) , var_inc(1) + , lit_inc(1) , watches_bin(WatcherDeleted(ca)) , watches(WatcherDeleted(ca)) , qhead(0) @@ -687,6 +702,9 @@ Var Solver::newVar(bool sign, bool dvar) vardata.push(mkVarData(CRef_Undef, 0)); activity_CHB.push(0); activity_VSIDS.push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); + activity_lit.push(0); + activity_lit.push(0); + picked.push(0); conflicted.push(0); @@ -917,7 +935,10 @@ void Solver::cancelUntil(int bLevel) #ifdef PRINT_OUT std::cout << "undo " << x << "\n"; #endif - if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) polarity[x] = sign(trail[c]); + if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) { + polarity[x] = sign(trail[c]); + litBumpActivity(mkLit(x, !polarity[x]), lsids_erase_bump_weight); + } insertVarOrder(x); } } @@ -940,6 +961,9 @@ void Solver::cancelUntil(int bLevel) Lit Solver::pickBranchLit() { Var next = var_Undef; + Lit lit = lit_Undef; + float diff_ratio = 1; + // Heap& order_heap = VSIDS ? order_heap_VSIDS : order_heap_CHB; Heap &order_heap = VSIDS ? order_heap_VSIDS : (DISTANCE ? order_heap_distance : order_heap_CHB); @@ -975,7 +999,15 @@ Lit Solver::pickBranchLit() if (posMissingInSome == 0 || negMissingInSome == 0) return posMissingInSome == 0 ? mkLit(next, false) : mkLit(next, true); - return mkLit(next, polarity[next]); + long double activity_diff = abs(activity_lit[2 * next] - activity_lit[2 * next + 1]); + diff_ratio = activity_diff / std::max(activity_lit[2 * next], activity_lit[2 * next + 1]); + + if (diff_ratio < lsids_pick) { + lit = pickLsidsBasedPhase(next); + return lit; + } else { + return mkLit(next, polarity[next]); + } } inline Solver::ConflictData Solver::FindConflictLevel(CRef cind) @@ -1085,7 +1117,8 @@ void Solver::analyze(CRef confl, vec &out_learnt, int &out_btlevel, int &ou if (!seen[var(q)] && level(var(q)) > 0) { if (VSIDS) { varBumpActivity(var(q), .5); - add_tmp.push(q); + litBumpActivity(~q, .5); + // add_tmp.push(q); } else conflicted[var(q)]++; seen[var(q)] = 1; @@ -1171,9 +1204,18 @@ void Solver::analyze(CRef confl, vec &out_learnt, int &out_btlevel, int &ou for (int i = 0; i < add_tmp.size(); i++) { Var v = var(add_tmp[i]); if (level(v) >= out_btlevel - 1) varBumpActivity(v, 1); + litBumpActivity(~add_tmp[i], 1); } add_tmp.clear(); } else { + for (int i = 0; i < add_tmp.size(); i++) { + Var v = var(add_tmp[i]); + if (level(v) >= out_btlevel - 1) { + litBumpActivity(~add_tmp[i], 1); + } + } + add_tmp.clear(); + seen[var(p)] = true; for (int i = out_learnt.size() - 1; i >= 0; i--) { Var v = var(out_learnt[i]); @@ -1945,6 +1987,7 @@ lbool Solver::search(int &nof_conflicts) if (confl != CRef_Undef) { // CONFLICT + if (--timer_lit == 0 && lit_decay < 0.95) timer_lit = 5000, lit_decay += 0.01; if (VSIDS) { if (--timer == 0 && var_decay < 0.95) timer = 5000, var_decay += 0.01; } else if (step_size > min_step_size) @@ -2036,6 +2079,7 @@ lbool Solver::search(int &nof_conflicts) } if (VSIDS) varDecayActivity(); + litDecayActivity(); claDecayActivity(); /*if (--learntsize_adjust_cnt == 0){ diff --git a/minisat/core/Solver.h b/minisat/core/Solver.h index 7cc718ed..0e6148c6 100644 --- a/minisat/core/Solver.h +++ b/minisat/core/Solver.h @@ -207,7 +207,9 @@ class Solver double step_size_dec; double min_step_size; int timer; + int timer_lit; double var_decay; + double lit_decay; double clause_decay; double random_var_freq; double random_seed; @@ -226,6 +228,9 @@ class Solver int learntsize_adjust_start_confl; double learntsize_adjust_inc; + double lsids_pick; + double lsids_erase_bump_weight; + // Statistics: (read-only member variable) // uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, conflicts_VSIDS; @@ -318,7 +323,9 @@ class Solver double cla_inc; // Amount to bump next clause with. vec activity_CHB, // A heuristic measurement of the activity of a variable. activity_VSIDS, activity_distance; - double var_inc; // Amount to bump next variable with. + vec activity_lit; + double var_inc; // Amount to bump next variable with. + double lit_inc; OccLists, WatcherDeleted> watches_bin, // Watches for binary clauses only. watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments. @@ -465,10 +472,14 @@ class Solver // Maintaining Variable/Clause activity: // + void litDecayActivity(); void varDecayActivity(); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. void varBumpActivity(Var v, double mult); // Increase a variable with the current 'bump' value. + void litBumpActivity(Lit l, double mult); void claDecayActivity(); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. void claBumpActivity(Clause &c); // Increase a clause with the current 'bump' value. + Lit pickLsidsBasedPhase(Var v); + // Operations on clauses: // @@ -641,6 +652,8 @@ inline void Solver::insertVarOrder(Var x) inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); } +inline void Solver::litDecayActivity() { lit_inc *= (1 / lit_decay); } + inline void Solver::varBumpActivity(Var v, double mult) { if ((activity_VSIDS[v] += var_inc * mult) > 1e100) { @@ -653,6 +666,28 @@ inline void Solver::varBumpActivity(Var v, double mult) if (order_heap_VSIDS.inHeap(v)) order_heap_VSIDS.decrease(v); } + +inline void Solver::litBumpActivity(Lit l, double mult) +{ + if ((activity_lit[l.x] += lit_inc * mult) > 1e100) { + // Rescale: + for (int i = 0; i < 2 * nVars(); i++) activity_lit[i] *= 1e-100; + lit_inc *= 1e-100; + } +} + +inline Lit Solver::pickLsidsBasedPhase(Var v) +{ + Lit pos_lit = mkLit(v, true); + Lit neg_lit = mkLit(v, false); + if (activity_lit[pos_lit.x] > activity_lit[neg_lit.x]) { + return pos_lit; + } else { + return neg_lit; + } +} + + inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); } inline void Solver::claBumpActivity(Clause &c) { From ca8cd93414e367a33c78564e98501659abae3ac0 Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Thu, 23 Jan 2020 15:21:11 +0800 Subject: [PATCH 3/5] LSIDS phase selections in CB only --- minisat/core/Solver.cc | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index b298e4f8..462dc080 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -999,10 +999,7 @@ Lit Solver::pickBranchLit() if (posMissingInSome == 0 || negMissingInSome == 0) return posMissingInSome == 0 ? mkLit(next, false) : mkLit(next, true); - long double activity_diff = abs(activity_lit[2 * next] - activity_lit[2 * next + 1]); - diff_ratio = activity_diff / std::max(activity_lit[2 * next], activity_lit[2 * next + 1]); - - if (diff_ratio < lsids_pick) { + if (CBT) { lit = pickLsidsBasedPhase(next); return lit; } else { From e36cb6020274263014f5c83808565496aa78480f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Sun, 14 Jun 2020 21:42:18 +0200 Subject: [PATCH 4/5] lsids: allow to activate separately Signed-off-by: Norbert Manthey --- minisat/core/Solver.cc | 4 +++- minisat/core/Solver.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 462dc080..22d455da 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -120,6 +120,7 @@ static DoubleOption opt_lsids_phase(cat2, 0.5, DoubleRange(0, true, 1, true)); static DoubleOption opt_lsids_erase_weight(cat2, "lsids-erase-weight", "Weight for LSIDS bump", 2.0, DoubleRange(0, true, 5, true)); +static BoolOption opt_use_lsids(cat2, "lsids", "Use LSIDS as literal polarity heuristic", true); static DoubleOption opt_inprocessing_inc(_cat, "inprocess-delay", @@ -232,6 +233,7 @@ Solver::Solver() , reactivate_VSIDS(false) , CBT(false) + , use_lsids(opt_use_lsids) , ok(true) , cla_inc(1) , var_inc(1) @@ -999,7 +1001,7 @@ Lit Solver::pickBranchLit() if (posMissingInSome == 0 || negMissingInSome == 0) return posMissingInSome == 0 ? mkLit(next, false) : mkLit(next, true); - if (CBT) { + if (CBT && use_lsids) { lit = pickLsidsBasedPhase(next); return lit; } else { diff --git a/minisat/core/Solver.h b/minisat/core/Solver.h index 0e6148c6..0b797583 100644 --- a/minisat/core/Solver.h +++ b/minisat/core/Solver.h @@ -236,7 +236,7 @@ class Solver uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, conflicts_VSIDS; uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; uint64_t chrono_backtrack, non_chrono_backtrack; - bool CBT; + bool CBT, use_lsids; vec picked; vec conflicted; From f3cf84282f8a33a6fcdd293f3190193346996049 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Sun, 14 Jun 2020 22:07:20 +0200 Subject: [PATCH 5/5] lsids: fix 'no-lsids' case When using no-lsids, we expect the solver to behave as before the changes of this series. However, when comparing the output of the solver with deactivated LSIDS, changes in the search behavior have been spotted. These changes are caused by modifications to the way variable activities are bumped during conflict analysis. This change reverts these changes in case LSIDS is not used. Signed-off-by: Norbert Manthey --- minisat/core/Solver.cc | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 22d455da..4089508e 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -1116,8 +1116,8 @@ void Solver::analyze(CRef confl, vec &out_learnt, int &out_btlevel, int &ou if (!seen[var(q)] && level(var(q)) > 0) { if (VSIDS) { varBumpActivity(var(q), .5); - litBumpActivity(~q, .5); - // add_tmp.push(q); + if(use_lsids) litBumpActivity(~q, .5); + else add_tmp.push(q); } else conflicted[var(q)]++; seen[var(q)] = 1; @@ -1207,13 +1207,15 @@ void Solver::analyze(CRef confl, vec &out_learnt, int &out_btlevel, int &ou } add_tmp.clear(); } else { - for (int i = 0; i < add_tmp.size(); i++) { - Var v = var(add_tmp[i]); - if (level(v) >= out_btlevel - 1) { - litBumpActivity(~add_tmp[i], 1); + if(use_lsids) { + for (int i = 0; i < add_tmp.size(); i++) { + Var v = var(add_tmp[i]); + if (level(v) >= out_btlevel - 1) { + litBumpActivity(~add_tmp[i], 1); + } } + add_tmp.clear(); } - add_tmp.clear(); seen[var(p)] = true; for (int i = out_learnt.size() - 1; i >= 0; i--) {