Skip to content

A
abc
Commit d9edb7e5 by Alan Mishchenko
Options

Variable timeframe abstraction.

parent 862ebb21
Showing with 89 additions and 82 deletions
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
......
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
......
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" );
......
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);
......
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)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment