diff options
Diffstat (limited to 'src/sat/asat/solver.c')
| -rw-r--r-- | src/sat/asat/solver.c | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index f2642c38..34b4d233 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -253,12 +253,11 @@ static inline void act_var_rescale(solver* s) { static inline void act_var_bump(solver* s, int v) { double* activity = s->activity; - if ((activity[v] += s->var_inc) > 1e100) -// if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100) + activity[v] += s->var_inc; +// activity[v] += s->var_inc * s->factors[v]; + if (activity[v] > 1e100) act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); - if ( s->pJMan == NULL && s->orderpos[v] != -1 ) order_update(s,v); @@ -842,6 +841,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) int conflictC = 0; veci learnt_clause; + int i; assert(s->root_level == solver_dlevel(s)); @@ -851,6 +851,12 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) veci_resize(&s->model,0); veci_new(&learnt_clause); + // reset the activities + if ( s->factors ) + for ( i = 0; i < s->size; i++ ) + s->activity[i] = (double)s->factors[i]; +// s->activity[i] = 1.0; + for (;;){ clause* confl = solver_propagate(s); if (confl != 0){ |