diff options
| -rw-r--r-- | src/sat/bsat/satSolver.c | 42 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 12 |
2 files changed, 1 insertions, 53 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 433f7c5f..6c987672 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -557,8 +557,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { s->qhead = s->qtail = bound; veci_resize(&s->trail_lim,level); - // update decision level - s->iDeciVar = level; } static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) { @@ -1160,7 +1158,6 @@ void sat_solver_delete(sat_solver* s) veci_delete(&s->pivot_vars); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); - veci_delete(&s->vDeciVars); // delete arrays if (s->reasons != 0){ @@ -1589,7 +1586,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) // double var_decay = 0.95; // double clause_decay = 0.999; double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; - int fGuided = (veci_size(&s->vDeciVars) > 0); ABC_INT64_T conflictC = 0; veci learnt_clause; int i; @@ -1603,15 +1599,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) // veci_resize(&s->model,0); veci_new(&learnt_clause); - // update variable polarity - if ( fGuided ) - { - int * pVars = veci_begin(&s->vDeciVars); - for ( i = 0; i < veci_size(&s->vDeciVars); i++ ) - var_set_polar( s, pVars[i], 0 ); - s->iDeciVar = 0; - } - // use activity factors in every even restart if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 ) // if ( veci_size(&s->act_vars) > 0 ) @@ -1658,16 +1645,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) }else{ // NO CONFLICT int next; - - // Reached bound on number of conflicts: - if ( !fGuided ) - { - if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){ - s->progress_estimate = sat_solver_progress(s); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; } - } // Reached bound on number of conflicts: if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || @@ -1690,24 +1667,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) // New variable decision: s->stats.decisions++; - if ( fGuided ) - { - int nVars = veci_size(&s->vDeciVars); - int * pVars = veci_begin(&s->vDeciVars); - next = var_Undef; - assert( s->iDeciVar <= nVars ); - while ( s->iDeciVar < nVars ) - { - int iVar = pVars[s->iDeciVar++]; - if ( var_value(s, iVar) == varX ) - { - next = iVar; - break; - } - } - } - else - next = order_select(s,(float)random_var_freq); + next = order_select(s,(float)random_var_freq); if (next == var_Undef){ // Model found: diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index e19b0b15..a0d9c478 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -179,9 +179,6 @@ struct sat_solver_t // clause store void * pStore; int fSolved; - // decision variables - veci vDeciVars; - int iDeciVar; // trace recording FILE * pFile; @@ -226,18 +223,9 @@ static void sat_solver_compress(sat_solver* s) (void) RetValue; } } -static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars ) -{ - int v; - assert( veci_size(&s->vDeciVars) == 0 ); - veci_new(&s->vDeciVars); - for ( v = 0; v < nVars; v++ ) - veci_push(&s->vDeciVars,pVars[v]); -} static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars ) { int i; - assert( veci_size(&s->vDeciVars) == 0 ); for ( i = 0; i < nVars; i++ ) s->polarity[pVars[i]] = 0; } |