Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lsids #41

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Lsids #41

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c726330
Showing number of decisions taken by CBT and NCBT
arijitsh Jan 23, 2020
b1e989d
Putting LSIDS to Devel (#3)
arijitsh Jan 23, 2020
ca8cd93
LSIDS phase selections in CB only
arijitsh Jan 23, 2020
e36cb60
lsids: allow to activate separately
conp-solutions Jun 14, 2020
f3cf842
lsids: fix 'no-lsids' case
conp-solutions Jun 14, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 51 additions & 3 deletions minisat/core/Solver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,17 @@ 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 BoolOption opt_use_lsids(cat2, "lsids", "Use LSIDS as literal polarity heuristic", true);

static DoubleOption opt_inprocessing_inc(_cat,
"inprocess-delay",
"Use this factor to wait for next inprocessing (0=off)",
Expand Down Expand Up @@ -167,7 +178,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)
Expand All @@ -190,6 +203,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)
Expand Down Expand Up @@ -217,9 +232,12 @@ Solver::Solver()
, VSIDS_propagations(opt_vsids_p)
, reactivate_VSIDS(false)

, CBT(false)
, use_lsids(opt_use_lsids)
, ok(true)
, cla_inc(1)
, var_inc(1)
, lit_inc(1)
, watches_bin(WatcherDeleted(ca))
, watches(WatcherDeleted(ca))
, qhead(0)
Expand Down Expand Up @@ -686,6 +704,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);
Expand Down Expand Up @@ -916,7 +937,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);
}
}
Expand All @@ -939,6 +963,9 @@ void Solver::cancelUntil(int bLevel)
Lit Solver::pickBranchLit()
{
Var next = var_Undef;
Lit lit = lit_Undef;
float diff_ratio = 1;

// Heap<VarOrderLt>& order_heap = VSIDS ? order_heap_VSIDS : order_heap_CHB;
Heap<VarOrderLt> &order_heap = VSIDS ? order_heap_VSIDS : (DISTANCE ? order_heap_distance : order_heap_CHB);

Expand Down Expand Up @@ -974,7 +1001,12 @@ Lit Solver::pickBranchLit()
if (posMissingInSome == 0 || negMissingInSome == 0)
return posMissingInSome == 0 ? mkLit(next, false) : mkLit(next, true);

return mkLit(next, polarity[next]);
if (CBT && use_lsids) {
lit = pickLsidsBasedPhase(next);
return lit;
} else {
return mkLit(next, polarity[next]);
}
}

inline Solver::ConflictData Solver::FindConflictLevel(CRef cind)
Expand Down Expand Up @@ -1084,7 +1116,8 @@ void Solver::analyze(CRef confl, vec<Lit> &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);
if(use_lsids) litBumpActivity(~q, .5);
else add_tmp.push(q);
} else
conflicted[var(q)]++;
seen[var(q)] = 1;
Expand Down Expand Up @@ -1170,9 +1203,20 @@ void Solver::analyze(CRef confl, vec<Lit> &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 {
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();
}

seen[var(p)] = true;
for (int i = out_learnt.size() - 1; i >= 0; i--) {
Var v = var(out_learnt[i]);
Expand Down Expand Up @@ -1944,6 +1988,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)
Expand Down Expand Up @@ -1982,10 +2027,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);
}

Expand Down Expand Up @@ -2033,6 +2080,7 @@ lbool Solver::search(int &nof_conflicts)
}

if (VSIDS) varDecayActivity();
litDecayActivity();
claDecayActivity();

/*if (--learntsize_adjust_cnt == 0){
Expand Down
38 changes: 37 additions & 1 deletion minisat/core/Solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -226,11 +228,15 @@ 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;
uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
uint64_t chrono_backtrack, non_chrono_backtrack;
bool CBT, use_lsids;

vec<uint32_t> picked;
vec<uint32_t> conflicted;
Expand Down Expand Up @@ -317,7 +323,9 @@ class Solver
double cla_inc; // Amount to bump next clause with.
vec<double> 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<double> activity_lit;
double var_inc; // Amount to bump next variable with.
double lit_inc;
OccLists<Lit, vec<Watcher>, 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<lbool> assigns; // The current assignments.
Expand Down Expand Up @@ -464,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:
//
Expand Down Expand Up @@ -640,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) {
Expand All @@ -652,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)
{
Expand Down