Version abc80725

1 files changed, 16 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){