diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
commit | 0c6505a26a537dc911b6566f82d759521e527c08 (patch) | |
tree | f2687995efd4943fe3b1307fce7ef5942d0a57b3 /src/sat/msat/msatSolverSearch.c | |
parent | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (diff) | |
download | abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.gz abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.bz2 abc-0c6505a26a537dc911b6566f82d759521e527c08.zip |
Version abc80130_2
Diffstat (limited to 'src/sat/msat/msatSolverSearch.c')
-rw-r--r-- | src/sat/msat/msatSolverSearch.c | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index 13a0c403..11a6540c 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -31,7 +31,7 @@ static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC static void Msat_SolverReduceDB( Msat_Solver_t * p ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -534,12 +534,18 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi Msat_Clause_t * pConf; Msat_Var_t Var; int nLevelBack, nConfs, nAssigns, Value; + int i; assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); p->Stats.nStarts++; p->dVarDecay = 1 / pPars->dVarDecay; p->dClaDecay = 1 / pPars->dClaDecay; + // reset the activities + for ( i = 0; i < p->nVars; i++ ) + p->pdActivity[i] = (double)p->pFactors[i]; +// p->pdActivity[i] = 0.0; + nConfs = 0; while ( 1 ) { @@ -599,7 +605,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi Msat_SolverCancelUntil( p, p->nLevelRoot ); return MSAT_UNKNOWN; } - else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) { + else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) { // Reached bound on number of conflicts: Msat_QueueClear( p->pQueue ); Msat_SolverCancelUntil( p, p->nLevelRoot ); |