From 1afa8a2f38bacb9f2f8faaf06b4f01c70560a419 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 25 Jul 2008 08:01:00 -0700 Subject: Version abc80725 --- src/sat/bsat/satSolver.c | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'src/sat/bsat/satSolver.c') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 12529ca7..833ea394 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -226,7 +226,8 @@ static inline void act_var_rescale(sat_solver* s) { } static inline void act_var_bump(sat_solver* s, int v) { - s->activity[v] += s->var_inc; +// s->activity[v] += s->var_inc; + s->activity[v] += (s->pGlobalVars? 3.0 : 1.0) * s->var_inc; if (s->activity[v] > 1e100) act_var_rescale(s); //printf("bump %d %f\n", v-1, activity[v]); @@ -243,6 +244,15 @@ static inline void act_var_bump_factor(sat_solver* s, int v) { order_update(s,v); } +static inline void act_var_bump_global(sat_solver* s, int v) { + s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); + if (s->activity[v] > 1e100) + act_var_rescale(s); + //printf("bump %d %f\n", v-1, activity[v]); + if (s->orderpos[v] != -1) + order_update(s,v); +} + static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } static inline void act_clause_rescale(sat_solver* s) { @@ -845,6 +855,11 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l for ( i = 0; i < s->act_vars.size; i++ ) act_var_bump_factor(s, s->act_vars.ptr[i]); + // use activity factors in every restart + if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_global(s, s->act_vars.ptr[i]); + for (;;){ clause* confl = sat_solver_propagate(s); if (confl != 0){ -- cgit v1.2.3