summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-09 23:09:59 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-09 23:09:59 -0700
commit6ba6c3279aa7a3d2f2bd6507a029e7aee0dcf65c (patch)
treea20685a579bd02b423fb9c539b31fb52b755123a /src/sat
parent908d5e696c7e73f80abcef85ec796511f3bffb0f (diff)
downloadabc-6ba6c3279aa7a3d2f2bd6507a029e7aee0dcf65c.tar.gz
abc-6ba6c3279aa7a3d2f2bd6507a029e7aee0dcf65c.tar.bz2
abc-6ba6c3279aa7a3d2f2bd6507a029e7aee0dcf65c.zip
Performance bug fix in the SAT solver (clearing variable activity after rollback).
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satSolver2.c3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 0e456f46..631051e0 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1573,6 +1573,9 @@ void sat_solver2_rollback( sat_solver2* s )
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
+ // clear variable activity
+ for ( i = s->iVarPivot; i < s->size; i++ )
+ s->activity[i] = (1<<10);
// initialize other vars
s->size = s->iVarPivot;