diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-23 15:13:22 +0300 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-23 15:13:22 +0300 |
commit | 67bfb4ba09aa02870140290f669360c302d55eb7 (patch) | |
tree | 122b1fa7f821c275687bf2fe036fcc48a5bb447c /src/sat/bsat | |
parent | 1b550cb87be41af5e0f2c0ce7805b9ab645d87cc (diff) | |
download | abc-67bfb4ba09aa02870140290f669360c302d55eb7.tar.gz abc-67bfb4ba09aa02870140290f669360c302d55eb7.tar.bz2 abc-67bfb4ba09aa02870140290f669360c302d55eb7.zip |
Improved algo for edge computation.
Diffstat (limited to 'src/sat/bsat')
-rw-r--r-- | src/sat/bsat/satSolver.c | 13 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index b9ab0740..815626ad 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -211,6 +211,19 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv return var_Undef; } +void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars) +{ + int i; + for (i = 0; i < s->size; i++) + s->activity[i] = 0; + s->var_inc = 1; + for ( i = 0; i < nVars; i++ ) + { + s->activity[pVars[i]] = nVars-i; + order_update( s, pVars[i] ); + } +} + //================================================================================================= // Activity functions: diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index e729d2c8..c4888c73 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -64,7 +64,7 @@ extern int sat_solver_count_assigned(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); extern int sat_solver_get_var_value(sat_solver* s, int v); - +extern void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars); extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); |