Commit 997e4c77 by Alan Mishchenko

Performance bug fix in the SAT solver (clearing variable activity after rollback).

parent 6ba6c327
......@@ -1574,8 +1574,15 @@ void sat_solver2_rollback( sat_solver2* s )
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
// clear variable activity
#ifdef USE_FLOAT_ACTIVITY2
for ( i = s->iVarPivot; i < s->size; i++ )
s->activity[i] = 0;
#else
for ( i = s->iVarPivot; i < s->size; i++ )
s->activity[i] = (1<<10);
#endif
// initialize other vars
s->size = s->iVarPivot;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment