summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-04-12 12:04:03 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2016-04-12 12:04:03 -0700
commitb4bb88ae5dc120118f419f5f70475c9a5dbe0727 (patch)
tree18044acce457da791f95c43ea7ec20a07490f559
parent3a553e15ac2f6c035bab1bec32c76ca8830ac4d7 (diff)
downloadabc-b4bb88ae5dc120118f419f5f70475c9a5dbe0727.tar.gz
abc-b4bb88ae5dc120118f419f5f70475c9a5dbe0727.tar.bz2
abc-b4bb88ae5dc120118f419f5f70475c9a5dbe0727.zip
Removing unused feature of the SAT solver (user-guided variable ordering).
-rw-r--r--src/sat/bsat/satSolver.c42
-rw-r--r--src/sat/bsat/satSolver.h12
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;
}