diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:31:26 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:31:26 -0700 |
| commit | ed564664f1ab86611cc05245745a22501f8414c2 (patch) | |
| tree | bb9c5d150a72ae5f4112006619debea8ef7f4ab8 /src/sat | |
| parent | cd39fd6b0585659922908d172b0d058a5cb02dbb (diff) | |
| download | abc-ed564664f1ab86611cc05245745a22501f8414c2.tar.gz abc-ed564664f1ab86611cc05245745a22501f8414c2.tar.bz2 abc-ed564664f1ab86611cc05245745a22501f8414c2.zip | |
Disabling learned clause removal when incremental proof-logging is running (tends to generate smaller abstarctions).
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 6662eca5..934f1be1 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1913,7 +1913,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; // reduce the set of learnt clauses - if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax ) + if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL ) sat_solver2_reducedb(s); // perform next run nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) ); |