summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satSolver.c17
-rw-r--r--src/sat/bsat/satSolver.h1
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;