diff options
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 21 | ||||
-rw-r--r-- | src/base/abci/abc.c | 16 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 115 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 18 |
5 files changed, 89 insertions, 82 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1069f5d2..76f8d3ad 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -205,6 +205,7 @@ struct Gia_ParVta_t_ int nFramesStart; // starting frame int nFramesPast; // overlap frames int nConfLimit; // conflict limit + int nLearntMax; // max number of learned clauses int nTimeOut; // timeout in seconds int nRatioMin; // stop when less than this % of object is abstracted int fUseTermVars; // use terminal variables diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 764f5d30..0c33ed1f 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -145,15 +145,16 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { memset( p, 0, sizeof(Gia_ParVta_t) ); - p->nFramesMax = 0; // maximum frames - p->nFramesStart = 5; // starting frame - p->nFramesPast = 4; // overlap frames - p->nConfLimit = 0; // conflict limit - p->nTimeOut = 0; // timeout in seconds - p->nRatioMin = 10; // stop when less than this % of object is abstracted - p->fUseTermVars = 1; // use terminal variables - p->fVerbose = 0; // verbose flag - p->iFrame = -1; // the number of frames covered + p->nFramesMax = 0; // maximum frames + p->nFramesStart = 5; // starting frame + p->nFramesPast = 4; // overlap frames + p->nConfLimit = 0; // conflict limit + p->nLearntMax = 10000; // max number of learned clauses + p->nTimeOut = 0; // timeout in seconds + p->nRatioMin = 10; // stop when less than this % of object is abstracted + p->fUseTermVars = 1; // use terminal variables + p->fVerbose = 0; // verbose flag + p->iFrame = -1; // the number of frames covered } /**Function************************************************************* @@ -1401,6 +1402,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); // start the manager p = Vga_ManStart( pAig, pPars ); + sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); // set runtime limit if ( p->pPars->nTimeOut ) sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); @@ -1432,6 +1434,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { // create bookmark to be used for rollback int nObjOld = p->nObjs; +// sat_solver2_reducedb( p->pSat ); sat_solver2_bookmark( p->pSat ); Vec_IntClear( p->vAddedNew ); // load the time frame diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8ae4e467..e2f0200d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26711,7 +26711,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Gia_VtaSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCTRtvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtvh" ) ) != EOF ) { switch ( c ) { @@ -26759,6 +26759,17 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nConfLimit < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLearntMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLearntMax < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -26824,12 +26835,13 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &vta [-FSPCTR num] [-tvh]\n" ); + Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-tvh]\n" ); Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin ); Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" ); diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 50a46050..ba23dcd6 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -183,9 +183,12 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) { if ( s->fProofLogging ) { +// int CapOld = (&s->proofs)->cap; satset* c = cls ? cls : var_unit_clause( s, Var ); veci_push(&s->proofs, clause_proofid(s, c, var_is_partA(s,Var)) ); // printf( "%d %d ", clause_proofid(s, c), Var ); +// if ( (&s->proofs)->cap > CapOld ) +// printf( "Resized proof from %d to %d.\n", CapOld, (&s->proofs)->cap ); } } @@ -1006,46 +1009,6 @@ int sat_solver2_simplify(sat_solver2* s) return (solver2_propagate(s) == NULL); } -/* - -void solver2_reducedb(sat_solver2* s) -{ - satset* c; - cla Cid; - int clk = clock(); - - // sort the clauses by activity - int nLearnts = veci_size(&s->claActs) - 1; - extern int * Abc_SortCost( int * pCosts, int nSize ); - int * pPerm, * pCosts = veci_begin(&s->claActs); - pPerm = Abc_SortCost( pCosts, veci_size(&s->claActs) ); - assert( pCosts[pPerm[1]] <= pCosts[pPerm[veci_size(&s->claActs)-1]] ); - - // mark clauses to be removed - { - double extra_limD = (double)s->cla_inc / nLearnts; // Remove any clause below this activity - unsigned extra_lim = (extra_limD < 1.0) ? 1 : (int)extra_limD; - unsigned * pActs = (unsigned *)veci_begin(&s->claActs); - int k = 1, Counter = 0; - sat_solver_foreach_learnt( s, c, Cid ) - { - assert( c->Id == k ); - c->mark = 0; - if ( c->nEnts > 2 && lit_reason(s,c->pEnts[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) - { - c->mark = 1; - Counter++; - } - k++; - } -printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d ", Counter, nLearnts, extra_lim ); -Abc_PrintTime( 1, "Time", clock() - clk ); - } - ABC_FREE( pPerm ); -} -*/ - - static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) { double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; @@ -1119,6 +1082,10 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) // Simplify the set of problem clauses: // sat_solver2_simplify(s); + // Reduce the set of learnt clauses: +// if (s->nLearntMax > 0 && s->stats.learnts >= (unsigned)s->nLearntMax) +// sat_solver2_reducedb(s); + // New variable decision: s->stats.decisions++; next = order_select(s,(float)random_var_freq); @@ -1130,15 +1097,6 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) s->model[i] = (var_value(s,i)==var1 ? l_True : l_False); solver2_canceluntil(s,s->root_level); veci_delete(&learnt_clause); - - /* - veci apa; veci_new(&apa); - for (i = 0; i < s->size; i++) - veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); - printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); - veci_delete(&apa); - */ - return l_True; } @@ -1193,6 +1151,7 @@ sat_solver2* sat_solver2_new(void) #endif s->fSkipSimplify = 1; s->fNotUseRandom = 0; + s->nLearntMax = 0; // prealloc clause assert( !s->clauses.ptr ); @@ -1430,25 +1389,34 @@ void luby2_test() for ( i = 0; i < 20; i++ ) printf( "%d ", (int)luby2(2,i) ); printf( "\n" ); -} +} // updates clauses, watches, units, and proof -void solver2_reducedb(sat_solver2* s) +void sat_solver2_reducedb(sat_solver2* s) { - satset * c; + static int TimeTotal = 0; cla h,* pArray,* pArray2; - int Counter = 0, CounterStart = s->stats.learnts * 3 / 4; // 2/3; + satset * c, * pivot; + int Counter, CounterStart; int i, j, k, hTemp, hHandle, clk = clock(); - static int TimeTotal = 0; + + if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax ) + return; + + CounterStart = s->stats.learnts - (s->nLearntMax / 3); + s->nLearntMax = s->nLearntMax * 11 / 10; // remove 2/3 of learned clauses while skipping small clauses + Counter = 0; veci_resize( &s->learnt_live, 0 ); sat_solver_foreach_learnt( s, c, h ) - if ( Counter++ > CounterStart || c->nEnts < 3 ) + { + if ( Counter++ > CounterStart || c->nEnts < 3 || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 ) veci_push( &s->learnt_live, h ); else c->mark = 1; + } // report the results printf( "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts ); @@ -1468,6 +1436,15 @@ void solver2_reducedb(sat_solver2* s) veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1); veci_resize(&s->claActs,veci_size(&s->learnt_live)+1); + // update reason clauses + for ( i = 0; i < s->size; i++ ) + if ( s->reasons[i] && (s->reasons[i] & 1) ) + { + c = clause_read( s, s->reasons[i] ); + assert( c->mark == 0 ); + s->reasons[i] = (c->Id << 1) | 1; + } + // compact watches for ( i = 0; i < s->size*2; i++ ) { @@ -1483,12 +1460,22 @@ void solver2_reducedb(sat_solver2* s) if ( s->fProofLogging ) for ( i = 0; i < s->size; i++ ) if ( s->units[i] && (s->units[i] & 1) ) - s->units[i] = (clause_read(s, s->units[i])->Id << 1) | 1; + { + c = clause_read( s, s->units[i] ); + assert( c->mark == 0 ); + s->units[i] = (c->Id << 1) | 1; + } // compact clauses + pivot = satset_read( &s->learnts, s->hLearntPivot ); satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) { hTemp = c->Id; c->Id = i + 1; memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*satset_size(c->nEnts) ); + if ( pivot && pivot <= c ) + { + s->hLearntPivot = hTemp; + pivot = NULL; + } } assert( hHandle == hTemp + satset_size(c->nEnts) ); veci_resize(&s->learnts,hHandle); @@ -1496,7 +1483,7 @@ void solver2_reducedb(sat_solver2* s) // compact proof (compacts 'proofs' and update 'claProofs') if ( s->fProofLogging ) - Sat_ProofReduce( s ); + Sat_ProofReduce( s ); TimeTotal += clock() - clk; Abc_PrintTime( 1, "Time", TimeTotal ); @@ -1607,7 +1594,7 @@ void sat_solver2_rollback( sat_solver2* s ) s->hLearntLast = -1; // the last learnt clause s->hProofLast = -1; // the last proof ID s->hClausePivot = 1; // the pivot among clauses - s->hLearntPivot = 1; // the pivot moang learned clauses + s->hLearntPivot = 1; // the pivot among learned clauses s->iVarPivot = 0; // the pivot among the variables s->iSimpPivot = 0; // marker of unit-clauses } @@ -1671,7 +1658,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim { int restart_iter = 0; ABC_INT64_T nof_conflicts; - ABC_INT64_T nof_learnts = sat_solver2_nclauses(s) / 3; lbool status = l_Undef; int proof_id; lit * i; @@ -1786,8 +1772,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim (double)s->stats.conflicts, (double)s->stats.clauses, (double)s->stats.clauses_literals, -// (double)nof_learnts, - (double)0, + (double)s->nLearntMax, (double)s->stats.learnts, (double)s->stats.learnts_literals, (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts, @@ -1796,12 +1781,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) break; - // reduce the set of learnt clauses: - if (nof_learnts > 0 && s->stats.learnts > nof_learnts) - { -// solver2_reducedb(s); - nof_learnts = nof_learnts * 11 / 10; - } + // reduce the set of learnt clauses: + sat_solver2_reducedb(s); // perform next run nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) ); status = solver2_search(s, nof_conflicts); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 63fc9755..4d01427a 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -47,6 +47,7 @@ extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); extern int sat_solver2_simplify(sat_solver2* s); extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern void sat_solver2_rollback(sat_solver2* s); +extern void sat_solver2_reducedb(sat_solver2* s); extern void sat_solver2_setnvars(sat_solver2* s,int n); @@ -101,6 +102,7 @@ struct sat_solver2_t unsigned* activity; // A heuristic measurement of the activity of a variable. #endif + int nLearntMax; // enables using reduce DB method int fNotUseRandom; // do not allow random decisions with a fixed probability int fSkipSimplify; // set to one to skip simplification of the clause database int fProofLogging; // enable proof-logging @@ -115,6 +117,7 @@ struct sat_solver2_t int hLearntPivot; // the pivot among learned clause int iVarPivot; // the pivot among the variables int iSimpPivot; // marker of unit-clauses + int nof_learnts; // the number of clauses to trigger reduceDB veci claActs; // clause activities veci claProofs; // clause proofs @@ -232,16 +235,23 @@ static inline int sat_solver2_final(sat_solver2* s, int ** ppArray) static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit) { - int nRuntimeLimit = s->nRuntimeLimit; + int temp = s->nRuntimeLimit; s->nRuntimeLimit = Limit; - return nRuntimeLimit; + return temp; } static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) { - int fNotUseRandomOld = s->fNotUseRandom; + int temp = s->fNotUseRandom; s->fNotUseRandom = fNotUseRandom; - return fNotUseRandomOld; + return temp; +} + +static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax) +{ + int temp = s->nLearntMax; + s->nLearntMax = nLearntMax; + return temp; } static inline void sat_solver2_bookmark(sat_solver2* s) |