Skip to content

A
abc
Commit 67bfb4ba by Alan Mishchenko
Options

Improved algo for edge computation.

parent 1b550cb8
Showing with 74 additions and 55 deletions
src/aig/gia/giaSatEdge.c
......@@ -33,7 +33,7 @@ typedef struct Seg_Man_t_ Seg_Man_t;
struct Seg_Man_t_
{
sat_solver * pSat; // SAT solver
Vec_Int_t * vCardVars; // candinality variables
//Vec_Int_t * vCardVars; // candinality variables
int nVars; // max vars (edge num)
int LogN; // base-2 log of max vars
int Power2; // power-2 of LogN
......@@ -82,11 +82,7 @@ Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p )
Gia_ManForEachLut( p, iLut )
Gia_LutForEachFanin( p, iLut, iFanin, i )
if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
{
//printf( "Var %d: %d -> %d\n", Vec_IntSize(vEdges)/2, iFanin, iLut );
Vec_IntPushTwo( vEdges, iFanin, iLut );
}
return vEdges;
}
Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
......@@ -149,7 +145,6 @@ Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia )
p->vLits = Vec_IntAlloc( 0 );
nVarsAll = Seg_ManCountIntLevels( p, p->FirstVar );
sat_solver_setnvars( p->pSat, nVarsAll );
printf( "Edges = %d. Total = %d.\n", p->FirstVar, nVarsAll );
// other
Gia_ManFillValue( pGia );
return p;
......@@ -192,7 +187,7 @@ void Seg_ManStop( Seg_Man_t * p )
SeeAlso []
***********************************************************************/
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
Gia_Obj_t * pObj;
Vec_Wec_t * vObjEdges;
......@@ -247,6 +242,7 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
}
}
assert( Count == p->nVars );
if ( fVerbose )
printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
nConstr = sat_solver_nclauses(p->pSat);
/*
......@@ -295,7 +291,9 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
}
}
Vec_WecFree( vObjEdges );
if ( fVerbose )
printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
......@@ -310,15 +308,14 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
SeeAlso []
***********************************************************************/
void Seg_ManConvertResult( Seg_Man_t * p )
Vec_Int_t * Seg_ManConvertResult( Seg_Man_t * p )
{
int iFanin, iObj, i;
Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 );
Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i )
if ( sat_solver_var_value(p->pSat, i/2) )
Vec_IntPushTwo( vEdges2, iFanin, iObj );
Gia_ManEdgeFromArray( p->pGia, vEdges2 );
Vec_IntFree( vEdges2 );
return vEdges2;
}
/**Function*************************************************************
......@@ -332,23 +329,34 @@ void Seg_ManConvertResult( Seg_Man_t * p )
SeeAlso []
***********************************************************************/
void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int fTwo, int fVerbose )
{
int nBTLimit = 0;
int nTimeOut = 0;
int fVeryVerbose = 0;
Gia_Obj_t * pObj;
abctime clk = Abc_Clock();
int i, d, iLut, iFirst, nVars, status, Limit;//, value;
Vec_Int_t * vEdges2 = NULL;
int i, iLut, iFirst, nVars, status, Delay, nConfs;
Seg_Man_t * p = Seg_ManAlloc( pGia );
Vec_Int_t * vVars = Vec_IntStartNatural( p->nVars );
int DelayStart = DelayInit ? DelayInit : p->DelayMax;
//if ( fVerbose )
printf( "Running SatEdge with delay %d and edge %d\n", Delay, fTwo+1 );
Seg_ManCreateCnf( p, fTwo );
if ( fVerbose )
printf( "Running SatEdge with starting delay %d and edge %d (edge vars %d, total vars %d)\n",
DelayStart, fTwo+1, p->FirstVar, sat_solver_nvars(p->pSat) );
Seg_ManCreateCnf( p, fTwo, fVerbose );
//Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
// for ( Delay = p->DelayMax; Delay >= 2; Delay-- )
// set resource limits
sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
sat_solver_set_random( p->pSat, 1 );
sat_solver_set_var_activity( p->pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
Vec_IntFree( vVars );
// increment delay gradually
for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
{
// collect assumptions
Vec_IntClear( p->vLits );
Gia_ManForEachCoDriver( p->pGia, pObj, i )
{
if ( !Gia_ObjIsAnd(pObj) )
......@@ -356,36 +364,32 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
iLut = Gia_ObjId( p->pGia, pObj );
iFirst = Vec_IntEntry( p->vFirsts, iLut );
nVars = Vec_IntEntry( p->vNvars, iLut );
Limit = Abc_MinInt( nVars, Delay );
// for ( d = 0; d < Limit; d++ )
// Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 0) );
// value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
// assert( value );
for ( d = Delay; d < nVars; d++ )
Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 1) );
if ( Delay < nVars )
sat_solver_push( p->pSat, Abc_Var2Lit(iFirst + Delay, 1) );
}
if ( Delay > DelayStart )
continue;
// solve with assumptions
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
//if ( status != l_True )
// break;
//clk = Abc_Clock();
nConfs = sat_solver_nconflicts( p->pSat );
status = sat_solver_solve_internal( p->pSat );
nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
if ( status == l_True )
{
int Count = 0;
for ( i = 0; i < p->nVars; i++ )
Count += sat_solver_var_value(p->pSat, i);
//printf( "\n" );
//Vec_IntPrint( p->vLits );
printf( "Solution with delay %d exists. Edges = %d. ", Delay, Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
{
int Count = 0;
for ( i = 0; i < p->nVars; i++ )
Count += sat_solver_var_value(p->pSat, i);
printf( "Solution with delay %2d and %5d edges exists. Conf = %8d. ", Delay, Count, nConfs );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// save the result
Vec_IntFreeP( &vEdges2 );
vEdges2 = Seg_ManConvertResult( p );
if ( fVeryVerbose )
{
for ( i = 0; i < p->nVars; i++ )
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
printf( " " );
......@@ -397,13 +401,19 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
}
else
{
printf( "Proved UNSAT for delay %d. ", Delay );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose )
{
if ( status == l_False )
printf( "Proved UNSAT for delay %d. ", Delay );
else
printf( "Resource limit reached for delay %d. ", Delay );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
break;
}
}
// convert and quit
if ( status == l_True )
Seg_ManConvertResult( p );
Gia_ManEdgeFromArray( p->pGia, vEdges2 );
Vec_IntFreeP( &vEdges2 );
Seg_ManStop( p );
}
......
src/base/abci/abc.c
......@@ -34923,11 +34923,6 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManConvertPackingToEdges( pAbc->pGia );
return 0;
}
if ( DelayMax )
{
Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
return 0;
}
if ( !fUseOld )
{
if ( pAbc->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pAbc->pGia->pManTime) )
......@@ -34935,7 +34930,8 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Currently this version of the algorithm does not work for designs with boxes.\n" );
return 0;
}
Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
//Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
return 0;
}
if ( pAbc->pGia->pManTime && fReverse )
src/sat/bsat/satSolver.c
......@@ -211,6 +211,19 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv
return var_Undef;
}
void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars)
{
int i;
for (i = 0; i < s->size; i++)
s->activity[i] = 0;
s->var_inc = 1;
for ( i = 0; i < nVars; i++ )
{
s->activity[pVars[i]] = nVars-i;
order_update( s, pVars[i] );
}
}
//=================================================================================================
// Activity functions:
......
src/sat/bsat/satSolver.h
......@@ -64,7 +64,7 @@ extern int sat_solver_count_assigned(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
extern int sat_solver_get_var_value(sat_solver* s, int v);
extern void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars);
extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
......
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