diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-25 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-25 08:01:00 -0700 |
commit | 1afa8a2f38bacb9f2f8faaf06b4f01c70560a419 (patch) | |
tree | 8aa41b5eea9d26befaf1604e8cc6c61b59eaef1b /src/sat/bsat | |
parent | 2c96c8af36446d3b855e07d78975cfad50c2917c (diff) | |
download | abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.tar.gz abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.tar.bz2 abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.zip |
Version abc80725
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/satSolver.c | 17 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 |
2 files changed, 17 insertions, 1 deletions
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){ diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 86e7a966..00ac60ca 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -180,6 +180,7 @@ struct sat_solver_t int fSkipSimplify; // set to one to skip simplification of the clause database + int * pGlobalVars; // for experiments with global vars during interpolation // clause store void * pStore; int fSolved; |