diff options
Diffstat (limited to 'src/sat/asat')
| -rw-r--r-- | src/sat/asat/added.c | 2 | ||||
| -rw-r--r-- | src/sat/asat/solver.c | 14 | ||||
| -rw-r--r-- | src/sat/asat/solver.h | 4 |
3 files changed, 13 insertions, 7 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 100b823b..222693ad 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -220,7 +220,7 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) SeeAlso [] ***********************************************************************/ -void Asat_SolverSetFactors(solver * s, int * pFactors) +void Asat_SolverSetFactors(solver * s, float * pFactors) { assert( s->factors == NULL ); s->factors = pFactors; 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){ diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 7edfb537..7a5e5be6 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -89,7 +89,7 @@ extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, int incrementVars); extern void Asat_SatPrintStats( FILE * pFile, solver * p ); extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); -extern void Asat_SolverSetFactors( solver * s, int * pFactors ); +extern void Asat_SolverSetFactors( solver * s, float * pFactors ); // J-frontier support extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); @@ -128,7 +128,7 @@ struct solver_t vec* wlists; // double* activity; // A heuristic measurement of the activity of a variable. - int * factors; // the factor of variable activity + float * factors; // the factor of variable activity lbool* assigns; // Current values of variables. int* orderpos; // Index in variable order. clause** reasons; // |