From 66796c38088a3ff74c530b3ee4a6dab33382f99a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 8 Feb 2016 16:29:36 -0800 Subject: Experiments with SAT-based mapping. --- src/aig/gia/giaNf.c | 106 +++++++++++++++++-------------- src/aig/gia/giaSatMap.c | 163 ++++++++++++++++++++++++++++++++++-------------- src/base/abci/abc.c | 2 +- 3 files changed, 176 insertions(+), 95 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c index 29f8679c..510e7ddb 100644 --- a/src/aig/gia/giaNf.c +++ b/src/aig/gia/giaNf.c @@ -1895,7 +1895,8 @@ void Nf_ManResetMatches( Nf_Man_t * p, int Round ) else { assert( Round > 0 || (!pDc->fBest && !pAc->fBest) ); - if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl ) +// if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl ) + if ( (Round & 1) && !pAc->fCompl ) ABC_SWAP( Nf_Mat_t, *pDc, *pAc ); pDc->fBest = 1; pAc->fBest = 0; @@ -2185,38 +2186,59 @@ void Nf_ManUpdateStats( Nf_Man_t * p ) Vec_Int_t * vCutGates; // gates (cut -> gate) */ -int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, int StartVar ) +int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars ) { Nf_Man_t * p = (Nf_Man_t *)pMan; int nInputs = Gia_ManCiNum(p->pGia); + int LitShift = 2*nInputs+2; Gia_Obj_t * pObj; int c, iObj; - Vec_Int_t * vInvCuts = Vec_IntAlloc( Gia_ManAndNum(p->pGia) ); + if ( 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia) > nVars ) + { + printf( "The number of variables is too large: 2*%d + %d = %d > %d.\n", Gia_ManAndNum(p->pGia), Gia_ManCiNum(p->pGia), 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia), nVars ); + return 0; + } + *pInvArea = p->InvAreaW; // save roots Vec_IntClear( vRoots ); Gia_ManForEachCo( p->pGia, pObj, c ) - Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-2*nInputs-2 ); + { + assert( !Gia_ObjIsCi(Gia_ObjFanin0(pObj)) ); + Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-LitShift ); + } // prepare Vec_WecClear( vCuts ); Vec_WecClear( vObjCuts ); Vec_IntClear( vSolCuts ); Vec_IntClear( vCutGates ); + Vec_WrdClear( vCutAreas ); // collect cuts for each node Gia_ManForEachAndId( p->pGia, iObj ) { - Vec_Int_t * vObj[2], * vCut; + Vec_Int_t * vObj[2], * vCutOne; int iCut, * pCut, * pCutSet; int iCutInv[2] = {-1, -1}; // get matches - Nf_Mat_t * pM[2]; + Nf_Mat_t * pM[2] = {NULL, NULL}; for ( c = 0; c < 2; c++ ) - pM[c] = Nf_ObjMapRefNum(p, iObj, c) ? Nf_ObjMatchBest(p, iObj, c) : NULL; + { + if ( Nf_ObjMapRefNum(p, iObj, c) == 0 ) + continue; + if ( Nf_ObjMatchBest(p, iObj, c)->fCompl ) + { + assert( iCutInv[c] == -1 ); + iCutInv[c] = Vec_IntSize(vSolCuts); + Vec_IntPush( vSolCuts, -1 ); + continue; + } + pM[c] = Nf_ObjMatchBest(p, iObj, c); + } // start collecting cuts of pos-obj and neg-obj - assert( Vec_WecSize(vObjCuts) == 2*(iObj-nInputs-1) ); + assert( Vec_WecSize(vObjCuts) == 2*iObj-LitShift ); for ( c = 0; c < 2; c++ ) { vObj[c] = Vec_WecPushLevel( vObjCuts ); - Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj-nInputs-1, c), 1) ); + Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj, c)-LitShift, 1) ); } // enumerate cuts pCutSet = Nf_ObjCutSet( p, iObj ); @@ -2239,6 +2261,7 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec Mio_Cell2_t*pC = Nf_ManCell( p, Info ); assert( nFans == (int)pC->nFanins ); Vec_IntPush( vCutGates, Info ); + Vec_WrdPush( vCutAreas, pC->AreaW ); // to make comparison possible Cfg.fCompl = 0; // add solution cut @@ -2246,31 +2269,26 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec { if ( pM[c] == NULL ) continue; - if ( pM[c]->fCompl ) - { - assert( iCutInv[c] == -1 ); - iCutInv[c] = Vec_IntSize(vSolCuts); - Vec_IntPush( vSolCuts, -1 ); - printf( "adding inv for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) ); - } - else if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) ) + if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) ) { Vec_IntPush( vSolCuts, Vec_WecSize(vCuts) ); - printf( "adding solution for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) ); + //printf( "adding solution for %d\n", Abc_Var2Lit(iObj, c)-LitShift ); } } // add new cut iCutLit = Abc_Var2Lit( StartVar + Vec_WecSize(vCuts), 0 ); - vCut = Vec_WecPushLevel( vCuts ); + vCutOne = Vec_WecPushLevel( vCuts ); // add literals - Vec_IntPush( vCut, Abc_Var2Lit(iObj, fCompl) ); + Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, fCompl) ); Vec_IntPush( vObj[fCompl], iCutLit ); Nf_CfgForEachVarCompl( Cfg, nFans, iFanin, fComplF, k ) - if ( pFans[iFanin] >= nInputs + 1 ) // and-node + if ( pFans[iFanin] >= nInputs + 1 ) // internal node { - Vec_IntPush( vCut, Abc_Var2Lit(pFans[iFanin], fComplF) ); - Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin]-nInputs-1, fComplF)), iCutLit ); + Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], fComplF) ); + //Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin], fComplF)-LitShift), iCutLit ); } + else if ( fComplF ) // complemented primary input + Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], 1) ); } } } @@ -2280,29 +2298,27 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec { if ( iCutInv[c] != -1 ) Vec_IntWriteEntry( vSolCuts, iCutInv[c], Vec_WecSize(vCuts) ); - Vec_IntPush( vInvCuts, Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) ); - vCut = Vec_WecPushLevel( vCuts ); - Vec_IntPush( vCut, Abc_Var2Lit(iObj, c) ); - Vec_IntPush( vCut, Abc_Var2Lit(iObj, !c) ); + // the obj-lit implies its cut + Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj, c)-LitShift), Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) ); + // the cut includes both literals + vCutOne = Vec_WecPushLevel( vCuts ); + Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, c) ); + Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, !c) ); Vec_IntPush( vCutGates, 3 ); + Vec_WrdPush( vCutAreas, p->InvAreaW ); } } - assert( Vec_WecSize(vObjCuts) == Vec_IntSize(vInvCuts) ); - Gia_ManForEachAndId( p->pGia, iObj ) - { - int iCutInv[2]; - for ( c = 0; c < 2; c++ ) - iCutInv[c] = Vec_IntEntry(vInvCuts, Abc_Var2Lit(iObj-nInputs-1, c)); - for ( c = 0; c < 2; c++ ) - { - Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[0] ); - Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[1] ); - } - } - Vec_IntFree( vInvCuts ); +// for ( c = 0; c < p->nCells; c++ ) +// printf( "%d=%s ", c, p->pCells[c].pName ); +// printf( "\n" ); + // add complemented inputs + Gia_ManForEachCiId( p->pGia, iObj, c ) + if ( Nf_ObjMapRefNum(p, iObj, 1) ) + Vec_IntPush( vSolCuts, -(2*Gia_ManAndNum(p->pGia)+c) ); assert( Vec_WecSize(vCuts) == Vec_IntSize(vCutGates) ); + assert( Vec_WecSize(vCuts) == Vec_WrdSize(vCutAreas) ); assert( Vec_WecSize(vObjCuts) == 2*Gia_ManAndNum(p->pGia) ); - return 2*nInputs+2; + return nInputs; } /**Function************************************************************* @@ -2390,13 +2406,11 @@ Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) } Nf_ManFixPoDrivers( p ); pNew = Nf_ManDeriveMapping( p ); - - // experimental mapper + if ( pPars->fAreaOnly ) { -// extern int Sbm_ManTestSat( void * p ); -// Sbm_ManTestSat( p ); + int Sbm_ManTestSat( void * pMan ); + Sbm_ManTestSat( p ); } - Nf_StoDelete( p ); return pNew; } diff --git a/src/aig/gia/giaSatMap.c b/src/aig/gia/giaSatMap.c index 377ce772..db04aa1c 100644 --- a/src/aig/gia/giaSatMap.c +++ b/src/aig/gia/giaSatMap.c @@ -21,6 +21,8 @@ #include "gia.h" #include "sat/bsat/satStore.h" #include "misc/vec/vecWec.h" +#include "misc/util/utilNam.h" +#include "map/scl/sclCon.h" ABC_NAMESPACE_IMPL_START @@ -39,12 +41,14 @@ struct Sbm_Man_t_ int LogN; // max vars int FirstVar; // first variable to be used int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2) + int nInputs; // the number of inputs // window Vec_Int_t * vRoots; // output drivers to be mapped (root -> lit) Vec_Wec_t * vCuts; // cuts (cut -> node lit + fanin lits) Vec_Wec_t * vObjCuts; // cuts (obj -> node lit + cut lits) Vec_Int_t * vSolCuts; // current solution (index -> cut) Vec_Int_t * vCutGates; // gates (cut -> gate) + Vec_Wrd_t * vCutAreas; // area of each cut // solver Vec_Int_t * vAssump; // assumptions (root nodes) Vec_Int_t * vPolar; // polarity of nodes and cuts @@ -86,12 +90,17 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol ) Vec_Int_t * vCut; // clear polarity and assumptions Vec_IntClear( p->vPolar ); - Vec_IntClear( p->vAssump ); - Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, K), 1) ); // mark used literals - Vec_IntFill( p->vLit2Used, Vec_WecSize(p->vObjCuts), 0 ); + Vec_IntFill( p->vLit2Used, Vec_WecSize(p->vObjCuts) + p->nInputs, 0 ); Vec_IntForEachEntry( p->vSolCuts, Cut, i ) { + if ( Cut < 0 ) // input inverter variable + { + Vec_IntWriteEntry( p->vLit2Used, -Cut, 1 ); + Vec_IntPush( p->vPolar, -Cut ); + continue; + } + Vec_IntPush( p->vPolar, p->FirstVar + Cut ); vCut = Vec_WecEntry( p->vCuts, Cut ); Lit = Vec_IntEntry( vCut, 0 ) - p->LitShift; // obj literal if ( Vec_IntEntry(p->vLit2Used, Lit) ) @@ -104,15 +113,21 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol ) { if ( Vec_IntEntry(p->vLit2Used, Lit) == 0 ) printf( "Output literal %d has no cut.\n", Lit ), RetValue = 0; - // create assumption - Vec_IntPush( p->vAssump, Abc_Var2Lit(Lit, 0) ); } // check internal nodes Vec_IntForEachEntry( p->vSolCuts, Cut, i ) { + if ( Cut < 0 ) + continue; vCut = Vec_WecEntry( p->vCuts, Cut ); Vec_IntForEachEntryStart( vCut, Lit, j, 1 ) - if ( Vec_IntEntry(p->vLit2Used, Lit - p->LitShift) == 0 ) + if ( Lit - p->LitShift < 0 ) + { + assert( Abc_LitIsCompl(Lit) ); + if ( Vec_IntEntry(p->vLit2Used, Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1) == 0 ) + printf( "Inverter of input %d of cut %d is not mapped.\n", Abc_Lit2Var(Lit)-1, Cut ), RetValue = 0; + } + else if ( Vec_IntEntry(p->vLit2Used, Lit - p->LitShift) == 0 ) printf( "Internal literal %d of cut %d is not mapped.\n", Lit - p->LitShift, Cut ), RetValue = 0; // create polarity Vec_IntPush( p->vPolar, p->FirstVar + Cut ); // cut variable @@ -134,7 +149,7 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol ) int Sbm_ManCreateCnf( Sbm_Man_t * p ) { int i, k, Lit, Lits[2], value; - Vec_Int_t * vLits; + Vec_Int_t * vLits, * vCutOne, * vLitsPrev; // sat_solver_rollback( p->Sat ); if ( !Sbm_ManCheckSol(p, p->vSolCuts) ) return 0; @@ -142,11 +157,13 @@ int Sbm_ManCreateCnf( Sbm_Man_t * p ) assert( p->FirstVar == sat_solver_nvars(p->pSat) ); sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WecSize(p->vCuts) ); // iterate over arrays containing obj-lit cuts (neg-obj-lit cut-lits followed by pos-obj-lit cut-lits) + vLitsPrev = NULL; Vec_WecForEachLevel( p->vObjCuts, vLits, i ) { assert( Vec_IntSize(vLits) >= 2 ); value = sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); assert( value ); +/* // for each cut, add implied nodes Lits[0] = Abc_LitNot( Vec_IntEntry(vLits, 0) ); assert( Lits[0] < 2*p->FirstVar ); @@ -158,17 +175,38 @@ int Sbm_ManCreateCnf( Sbm_Man_t * p ) assert( value ); //printf( "Adding clause %d + %d.\n", Lits[0], Lits[1]-2*p->FirstVar ); } +*/ //printf( "\n" ); // create invertor exclusivity clause if ( i & 1 ) { - Lits[0] = Abc_LitNot( Vec_IntEntry(vLits, Vec_IntSize(vLits)-1) ); - Lits[1] = Abc_LitNot( Vec_IntEntry(vLits, Vec_IntSize(vLits)-2) ); + Lits[0] = Abc_LitNot( Vec_IntEntryLast(vLits) ); + Lits[1] = Abc_LitNot( Vec_IntEntryLast(vLitsPrev) ); value = sat_solver_addclause( p->pSat, Lits, Lits + 2 ); assert( value ); //printf( "Adding exclusivity clause %d + %d.\n", Lits[0]-2*p->FirstVar, Lits[1]-2*p->FirstVar ); } + vLitsPrev = vLits; } + // add inverters + Vec_WecForEachLevel( p->vCuts, vCutOne, i ) + Vec_IntForEachEntry( vCutOne, Lit, k ) + if ( Abc_Lit2Var(Lit)-1 < p->nInputs ) // input + { + assert( k > 0 ); + Lits[0] = Abc_Var2Lit( Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1, 0 ); + Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 ); + value = sat_solver_addclause( p->pSat, Lits, Lits + 2 ); + assert( value ); + } + else // internal node + { + Lits[0] = Abc_Var2Lit( Lit-p->LitShift, 0 ); + Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 ); + value = sat_solver_addclause( p->pSat, Lits, Lits + 2 ); + assert( value ); + } + sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) ); return 1; } @@ -312,15 +350,6 @@ sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ) void Sbm_AddCardinConstrTest() { -/* - int Lit, LogN = 3, nVars = 1 << LogN, K = 2, Count = 1; - int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1), nVarsReal; - Vec_Int_t * vVars = Vec_IntStartNatural( nVars ); - sat_solver * pSat = sat_solver_new(); - sat_solver_setnvars( pSat, nVarsAlloc ); - nVarsReal = Sbm_AddCardinConstrPairWise( pSat, vVars, 2 ); - assert( nVarsReal == nVarsAlloc ); -*/ int LogN = 3, nVars = 1 << LogN, K = 2, Count = 1; Vec_Int_t * vVars, * vLits = Vec_IntAlloc( nVars ); sat_solver * pSat = Sbm_AddCardinSolver( LogN, &vVars ); @@ -328,7 +357,6 @@ void Sbm_AddCardinConstrTest() int Lit = Abc_Var2Lit( Vec_IntEntry(vVars, K), 1 ); printf( "LogN = %d. N = %3d. Vars = %5d. Clauses = %6d. Comb = %d.\n", LogN, nVars, nVarsReal, sat_solver_nclauses(pSat), nVars * (nVars-1)/2 + nVars + 1 ); - while ( 1 ) { int i, status = sat_solver_solve( pSat, &Lit, &Lit+1, 0, 0, 0, 0 ); @@ -375,6 +403,7 @@ Sbm_Man_t * Sbm_ManAlloc( int LogN ) p->vObjCuts = Vec_WecAlloc( 1000 ); p->vSolCuts = Vec_IntAlloc( 100 ); p->vCutGates = Vec_IntAlloc( 100 ); + p->vCutAreas = Vec_WrdAlloc( 100 ); // solver p->vAssump = Vec_IntAlloc( 100 ); p->vPolar = Vec_IntAlloc( 100 ); @@ -398,6 +427,7 @@ void Sbm_ManStop( Sbm_Man_t * p ) Vec_WecFree( p->vObjCuts ); Vec_IntFree( p->vSolCuts ); Vec_IntFree( p->vCutGates ); + Vec_WrdFree( p->vCutAreas ); // internal Vec_IntFree( p->vAssump ); Vec_IntFree( p->vPolar ); @@ -408,24 +438,32 @@ void Sbm_ManStop( Sbm_Man_t * p ) Vec_IntFree( p->vLit2Used ); Vec_IntFree( p->vDelays ); Vec_IntFree( p->vReason ); + ABC_FREE( p ); } int Sbm_ManTestSat( void * pMan ) { abctime clk = Abc_Clock(), clk2; - int i, LogN = 4, nVars = 1 << LogN, status, Root; + int i, k, Lit, LogN = 7, nVars = 1 << LogN, status, Root; Sbm_Man_t * p = Sbm_ManAlloc( LogN ); + word InvArea = 0; + int fKeepTrying = 1; + int StartSol; // derive window - extern int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, int StartVar ); - p->LitShift = Nf_ManExtractWindow( pMan, p->vRoots, p->vCuts, p->vObjCuts, p->vSolCuts, p->vCutGates, p->FirstVar ); - assert( Vec_WecSize(p->vObjCuts) <= nVars ); + extern int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars ); + p->nInputs = Nf_ManExtractWindow( pMan, p->vRoots, p->vCuts, p->vObjCuts, p->vSolCuts, p->vCutGates, p->vCutAreas, &InvArea, p->FirstVar, nVars ); + p->LitShift = 2*p->nInputs+2; + assert( Vec_WecSize(p->vObjCuts) + p->nInputs <= nVars ); // print-out // Vec_WecPrint( p->vCuts, 0 ); // printf( "\n" ); - Vec_WecPrint( p->vObjCuts, 0 ); - printf( "\n" ); +// Vec_WecPrint( p->vObjCuts, 0 ); +// printf( "\n" ); Vec_IntPrint( p->vSolCuts ); + printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n", + sat_solver_nclauses(p->pSat), Vec_WecSize(p->vObjCuts), Vec_WecSizeSize(p->vCuts), + sat_solver_nclauses(p->pSat) - Vec_WecSize(p->vObjCuts) - Vec_WecSizeSize(p->vCuts) ); // creating CNF if ( !Sbm_ManCreateCnf(p) ) @@ -434,39 +472,68 @@ int Sbm_ManTestSat( void * pMan ) // create assumptions // cardinality Vec_IntClear( p->vAssump ); -// for ( i = 0; i < Vec_IntSize(p->vSolCuts); i++ ) -// Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) ); - Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, Vec_IntSize(p->vSolCuts)), 1) ); + Vec_IntPush( p->vAssump, -1 ); // unused variables - for ( i = Vec_WecSize(p->vObjCuts); i < nVars; i++ ) + for ( i = Vec_WecSize(p->vObjCuts) + p->nInputs; i < nVars; i++ ) Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); // root variables Vec_IntForEachEntry( p->vRoots, Root, i ) Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); // Vec_IntPrint( p->vAssump ); - // solve the problem - clk2 = Abc_Clock(); - status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 ); - if ( status == l_False ) - printf( "UNSAT " ); - else if ( status == l_True ) - printf( "SAT " ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); - - if ( status == l_True ) + StartSol = Vec_IntSize(p->vSolCuts); +// StartSol = 30; + while ( fKeepTrying ) { - for ( i = 0; i < nVars; i++ ) - printf( "%d", sat_solver_var_value(p->pSat, i) ); - printf( "\n" ); - for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) - printf( "%d ", sat_solver_var_value(p->pSat, i) ); - printf( "\n" ); - for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) - printf( "%d=%d ", i-p->FirstVar, sat_solver_var_value(p->pSat, i) ); + printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying ); + // for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ ) + // Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) ); + Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) ); + // solve the problem + clk2 = Abc_Clock(); + status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 ); + if ( status == l_True ) + { + word AreaNew = 0; + int Count = 0; + printf( "AND Lits = %d. Inputs = %d. Vars = %d. All vars = %d.\n", Vec_WecSize(p->vObjCuts), p->nInputs, Vec_WecSize(p->vObjCuts) + p->nInputs, nVars ); +// for ( i = 0; i < nVars; i++ ) +// printf( "%d", sat_solver_var_value(p->pSat, i) ); +// printf( "\n" ); + for ( i = 0; i < nVars; i++ ) + if ( sat_solver_var_value(p->pSat, i) ) + { + printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); + Count++; + if ( i >= Vec_WecSize(p->vObjCuts) ) + AreaNew += InvArea; + } + printf( "Count = %d\n", Count ); +// for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) +// printf( "%d", sat_solver_var_value(p->pSat, i) ); +// printf( "\n" ); + Count = 1; + for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) + if ( sat_solver_var_value(p->pSat, i) ) + { + Vec_Int_t * vCutOne = Vec_WecEntry(p->vCuts, i-p->FirstVar); + printf( "%2d : Cut %3d (Gate %2d) ", Count, i-p->FirstVar, Vec_IntEntry(p->vCutGates, i-p->FirstVar) ); + Vec_IntForEachEntry( vCutOne, Lit, k ) + printf( "%d(%d) ", Lit - 2*(p->nInputs+1), Abc_Lit2Var(Lit) ); + printf( "\n" ); + Count++; + AreaNew += Vec_WrdEntry(p->vCutAreas, i-p->FirstVar); + } + printf( "Area = %7.2f\n", Scl_Int2Flt((int)AreaNew) ); + } + if ( status == l_False ) + printf( "UNSAT " ), fKeepTrying = 0; + else if ( status == l_True ) + printf( "SAT " ), fKeepTrying++; + Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); printf( "\n" ); } - Sbm_ManStop( p ); return 1; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 73175997..92d6557d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34467,7 +34467,7 @@ usage: Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner ); Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer ); Abc_Print( -2, "\t-Q num : internal parameter impacting area of the mapping [default = %d]\n", pPars->nReqTimeFlex ); - Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" ); + Abc_Print( -2, "\t-a : toggles SAT-based area-oriented mapping (experimental) [default = %s]\n", pPars->fAreaOnly? "yes": "no" ); Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" ); Abc_Print( -2, "\t-p : toggles pin permutation (more matches - better quality) [default = %s]\n", pPars->fPinPerm? "yes": "no" ); Abc_Print( -2, "\t-q : toggles quick mapping (fewer matches - worse quality) [default = %s]\n", pPars->fPinQuick? "yes": "no" ); -- cgit v1.2.3