diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/asat/added.c | 17 | ||||
-rw-r--r-- | src/sat/asat/solver.c | 4 | ||||
-rw-r--r-- | src/sat/asat/solver.h | 2 | ||||
-rw-r--r-- | src/sat/fraig/fraigSat.c | 6 | ||||
-rw-r--r-- | src/sat/msat/msat.h | 2 | ||||
-rw-r--r-- | src/sat/msat/msatActivity.c | 1 | ||||
-rw-r--r-- | src/sat/msat/msatInt.h | 1 | ||||
-rw-r--r-- | src/sat/msat/msatSolverApi.c | 6 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 3 |
9 files changed, 36 insertions, 6 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 832bc0cf..100b823b 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -209,6 +209,23 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) s->nPrefVars = nPrefVars; } +/**Function************************************************************* + + Synopsis [Sets the preferred variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_SolverSetFactors(solver * s, int * pFactors) +{ + assert( s->factors == NULL ); + s->factors = pFactors; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 548abd1d..f2642c38 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -254,6 +254,7 @@ static inline void act_var_rescale(solver* s) { static inline void act_var_bump(solver* s, int v) { double* activity = s->activity; if ((activity[v] += s->var_inc) > 1e100) +// if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100) act_var_rescale(s); //printf("bump %d %f\n", v-1, activity[v]); @@ -947,6 +948,7 @@ solver* solver_new(void) // initialize arrays s->wlists = 0; s->activity = 0; + s->factors = 0; s->assigns = 0; s->orderpos = 0; s->reasons = 0; @@ -1039,9 +1041,9 @@ void solver_delete(solver* s) free(s->trail ); free(s->tags ); } - if ( s->pJMan ) Asat_JManStop( s ); if ( s->pPrefVars ) free( s->pPrefVars ); + if ( s->factors ) free( s->factors ); free(s); } diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 05e9dafa..7edfb537 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -89,6 +89,7 @@ extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, int incrementVars); extern void Asat_SatPrintStats( FILE * pFile, solver * p ); extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); +extern void Asat_SolverSetFactors( solver * s, int * pFactors ); // J-frontier support extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); @@ -127,6 +128,7 @@ struct solver_t vec* wlists; // double* activity; // A heuristic measurement of the activity of a variable. + int * factors; // the factor of variable activity lbool* assigns; // Current values of variables. int* orderpos; // Index in variable order. clause** reasons; // diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index aa28a4f2..1a56cf0e 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -326,7 +326,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * Fraig_ManCreateSolver( p ); // make sure the SAT solver has enough variables for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) - Msat_SolverAddVar( p->pSat ); + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); @@ -543,7 +543,7 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t Fraig_ManCreateSolver( p ); // make sure the SAT solver has enough variables for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) - Msat_SolverAddVar( p->pSat ); + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); // get the logic cone clk = clock(); @@ -642,7 +642,7 @@ int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_ Fraig_ManCreateSolver( p ); // make sure the SAT solver has enough variables for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ ) - Msat_SolverAddVar( p->pSat ); + Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level ); // get the logic cone clk = clock(); diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 5f8603a7..1d9c0005 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -80,7 +80,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ); /*=== satSolver.c ===========================================================*/ // adding vars, clauses, simplifying the database, and solving -extern bool Msat_SolverAddVar( Msat_Solver_t * p ); +extern bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ); extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p ); extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index 0947d6d5..f808d9bc 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -46,6 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) return; Var = MSAT_LIT2VAR(Lit); if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 ) +// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 ) Msat_SolverVarRescaleActivity( p ); Msat_OrderUpdate( p->pOrder, Var ); } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 03e7b873..15932c67 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -119,6 +119,7 @@ struct Msat_Solver_t_ double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. double * pdActivity; // A heuristic measurement of the activity of a variable. + int * pLevels; // the levels of the variables double dVarInc; // Amount to bump next variable with. double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. Msat_Order_t * pOrder; // Keeps track of the decision variable order. diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index e3d85774..8c1542df 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -174,8 +174,12 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarDecay = dVarDecay; p->pdActivity = ALLOC( double, p->nVarsAlloc ); + p->pLevels = ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) + { p->pdActivity[i] = 0; + p->pLevels = 0; + } p->pAssigns = ALLOC( int, p->nVarsAlloc ); p->pModel = ALLOC( int, p->nVarsAlloc ); @@ -239,6 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) p->nVarsAlloc = nVarsAlloc; p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); + p->pLevels = REALLOC( int, p->pLevels, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pdActivity[i] = 0; @@ -394,6 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseVecFree( p->vLearned ); FREE( p->pdActivity ); + FREE( p->pLevels ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 397dbcdc..f9fee73c 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -39,10 +39,11 @@ SeeAlso [] ***********************************************************************/ -bool Msat_SolverAddVar( Msat_Solver_t * p ) +bool Msat_SolverAddVar( Msat_Solver_t * p, int Level ) { if ( p->nVars == p->nVarsAlloc ) Msat_SolverResize( p, 2 * p->nVarsAlloc ); + p->pLevel[p->nVars] = Level; p->nVars++; return 1; } |