From b2055bd6373e7b0c0da16ca423770131e2f48dbf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 20 Feb 2018 16:00:58 -0800 Subject: Improvements to circuit based solver. --- src/aig/gia/giaCSat2.c | 114 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 81 insertions(+), 33 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat2.c index f80c4533..ee0ce311 100644 --- a/src/aig/gia/giaCSat2.c +++ b/src/aig/gia/giaCSat2.c @@ -75,6 +75,7 @@ struct Cbs2_Man_t_ Vec_Str_t vMark; Vec_Int_t vLevReason; Vec_Int_t vWatches; + Vec_Int_t vWatchUpds; Vec_Int_t vFanoutN; Vec_Int_t vFanout0; Vec_Int_t vActivity; @@ -98,6 +99,7 @@ struct Cbs2_Man_t_ // other statistics int nPropCalls[3]; int nFails[2]; + int nClauseConf; }; static inline int Cbs2_VarUnused( Cbs2_Man_t * p, int iVar ) { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; } @@ -227,8 +229,9 @@ Cbs2_Man_t * Cbs2_ManAlloc( Gia_Man_t * pGia ) Vec_IntFill( &p->vFanout0, Gia_ManObjNum(pGia), 0 ); Vec_IntFill( &p->vFanoutN, 2*Gia_ManObjNum(pGia), 0 ); Vec_IntFill( &p->vActivity, Gia_ManObjNum(pGia), 0 ); - Vec_IntGrow( &p->vActStore, 1000 ); - Vec_IntGrow( &p->vJStore, 1000 ); + Vec_IntGrow( &p->vActStore, 1000 ); + Vec_IntGrow( &p->vJStore, 1000 ); + Vec_IntGrow( &p->vWatchUpds, 1000 ); return p; } @@ -254,6 +257,7 @@ void Cbs2_ManStop( Cbs2_Man_t * p ) Vec_IntErase( &p->vActivity ); Vec_IntErase( &p->vActStore ); Vec_IntErase( &p->vJStore ); + Vec_IntErase( &p->vWatchUpds ); Vec_IntFree( p->vModel ); Vec_IntFree( p->vTemp ); ABC_FREE( p->pClauses.pData ); @@ -370,6 +374,15 @@ static inline void Cbs2_QuePush( Cbs2_Que_t * p, int iObj ) } p->pData[p->iTail++] = iObj; } +static inline void Cbs2_QueGrow( Cbs2_Que_t * p, int Plus ) +{ + if ( p->iTail + Plus > p->nSize ) + { + p->nSize *= 2; + p->pData = ABC_REALLOC( int, p->pData, p->nSize ); + } + assert( p->iTail + Plus <= p->nSize ); +} /**Function************************************************************* @@ -588,14 +601,15 @@ static inline void Cbs2_ManAssign( Cbs2_Man_t * p, int iLit, int Level, int iRes ***********************************************************************/ static inline void Cbs2_ManPrintClause( Cbs2_Man_t * p, int Level, int hClause ) { - int i, iObj; + int i, iLit; assert( Cbs2_QueIsEmpty( &p->pClauses ) ); printf( "Level %2d : ", Level ); - Cbs2_ClauseForEachEntry( p, hClause, iObj, i ) - printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, iObj), Cbs2_VarDecLevel(p, iObj) ); + Cbs2_ClauseForEachEntry( p, hClause, iLit, i ) + printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) ); +// printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, Abc_Lit2Var(iLit)), Cbs2_VarDecLevel(p, Abc_Lit2Var(iLit)) ); printf( "\n" ); } -static inline void Cbs2_ManPrintClauseNew( Cbs2_Man_t * p, int Level, int hClause ) +static inline void Cbs2_ManPrintCube( Cbs2_Man_t * p, int Level, int hClause ) { int i, iObj; assert( Cbs2_QueIsEmpty( &p->pClauses ) ); @@ -633,10 +647,21 @@ static inline void Cbs2_ManBumpClean( Cbs2_Man_t * p ) SeeAlso [] ***********************************************************************/ +static inline void Cbs2_ManCleanWatch( Cbs2_Man_t * p ) +{ + int i, iLit; + Vec_IntForEachEntry( &p->vWatchUpds, iLit, i ) + Vec_IntWriteEntry( &p->vWatches, iLit, 0 ); + Vec_IntClear( &p->vWatchUpds ); + //Vec_IntForEachEntry( &p->vWatches, iLit, i ) + // assert( iLit == 0 ); +} static inline void Cbs2_ManWatchClause( Cbs2_Man_t * p, int hClause, int Lit ) { int * pLits = Cbs2_ClauseLits( p, hClause ); int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) ); + if ( *pPlace == 0 ) + Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) ); /* if ( pClause->pLits[0] == Lit ) pClause->pNext0 = p->pWatches[lit_neg(Lit)]; @@ -648,23 +673,36 @@ static inline void Cbs2_ManWatchClause( Cbs2_Man_t * p, int hClause, int Lit ) p->pWatches[lit_neg(Lit)] = pClause; */ assert( Lit == pLits[0] || Lit == pLits[1] ); - Cbs2_ClauseSetNext( p, hClause, Lit != pLits[0], *pPlace ); + Cbs2_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace ); *pPlace = hClause; } -static inline int Cbs2_QueFinish( Cbs2_Man_t * p ) +static inline int Cbs2_QueFinish( Cbs2_Man_t * p, int Level ) { Cbs2_Que_t * pQue = &(p->pClauses); - int hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1; + int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1; assert( pQue->iHead+1 < pQue->iTail ); Cbs2_ClauseSetSize( p, pQue->iHead, Size ); - Cbs2_QuePush( pQue, 0 ); - Cbs2_QuePush( pQue, 0 ); - pQue->iHead = pQue->iTail; - if ( Size > 1 ) + hClauseC = pQue->iHead = pQue->iTail; + //printf( "Adding cube: " ); Cbs2_ManPrintCube(p, Level, hClause); + if ( Size == 1 ) + return hClause; + // create watched clause + pQue->iHead = hClause; + Cbs2_QueForEachEntry( p->pClauses, iObj, i ) { - Cbs2_ManWatchClause( p, hClause, Cbs2_ClauseLit(p, hClause, 0) ); - Cbs2_ManWatchClause( p, hClause, Cbs2_ClauseLit(p, hClause, 1) ); + if ( i == hClauseC ) + break; + else if ( i == hClause ) // nlits + Cbs2_QuePush( pQue, iObj ); + else // literals + Cbs2_QuePush( pQue, Abc_Var2Lit(iObj, Cbs2_VarValue(p, iObj)) ); // complement } + Cbs2_QuePush( pQue, 0 ); // next0 + Cbs2_QuePush( pQue, 0 ); // next1 + pQue->iHead = pQue->iTail; + Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 0) ); + Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 1) ); + //printf( "Adding clause %d: ", hClauseC ); Cbs2_ManPrintClause(p, Level, hClauseC); return hClause; } @@ -723,9 +761,10 @@ static inline int Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level ) } else // clause reason { - int i, nLits = Cbs2_ClauseSize( p, pReason[1] ); - int * pLits = Cbs2_ClauseLits( p, pReason[1] ); + int i, * pLits, nLits = Cbs2_ClauseSize( p, pReason[1] ); assert( pReason[1] ); + Cbs2_QueGrow( pQue, nLits ); + pLits = Cbs2_ClauseLits( p, pReason[1] ); assert( iObj == Abc_Lit2Var(pLits[0]) ); for ( i = 1; i < nLits; i++ ) Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) ); @@ -737,31 +776,33 @@ static inline int Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level ) // clear the marks Vec_IntForEachEntry( p->vTemp, iObj, i ) Cbs2_VarSetMark0(p, iObj, 0); - return Cbs2_QueFinish( p ); + return Cbs2_QueFinish( p, Level ); } static inline int Cbs2_ManAnalyze( Cbs2_Man_t * p, int Level, int iVar, int iFan0, int iFan1 ) { Cbs2_Que_t * pQue = &(p->pClauses); assert( Cbs2_VarIsAssigned(p, iVar) ); - assert( Cbs2_VarIsAssigned(p, iFan0) ); - assert( iFan1 == 0 || Cbs2_VarIsAssigned(p, iFan1) ); assert( Cbs2_QueIsEmpty( pQue ) ); Cbs2_QuePush( pQue, 0 ); Cbs2_QuePush( pQue, 0 ); - Cbs2_QuePush( pQue, iVar ); - if ( iFan0 ) + if ( iFan0 ) // circuit conflict { + assert( Cbs2_VarIsAssigned(p, iFan0) ); + assert( iFan1 == 0 || Cbs2_VarIsAssigned(p, iFan1) ); + Cbs2_QuePush( pQue, iVar ); Cbs2_QuePush( pQue, iFan0 ); if ( iFan1 ) Cbs2_QuePush( pQue, iFan1 ); } - else + else // clause conflict { - int i, nLits = Cbs2_ClauseSize( p, iFan1 ); - int * pLits = Cbs2_ClauseLits( p, iFan1 ); + int i, * pLits, nLits = Cbs2_ClauseSize( p, iFan1 ); assert( iFan1 ); + Cbs2_QueGrow( pQue, nLits ); + pLits = Cbs2_ClauseLits( p, iFan1 ); assert( iVar == Abc_Lit2Var(pLits[0]) ); - for ( i = 1; i < nLits; i++ ) + assert( Cbs2_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) ); + for ( i = 0; i < nLits; i++ ) Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) ); } return Cbs2_ManDeriveReason( p, Level ); @@ -788,6 +829,8 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit ) { int nLits = Cbs2_ClauseSize( p, Cur ); int * pLits = Cbs2_ClauseLits( p, Cur ); + p->nPropCalls[1]++; +//printf( " Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level ); // make sure the false literal is in the second literal of the clause //if ( pCur->pLits[0] == LitF ) if ( pLits[0] == LitF ) @@ -799,7 +842,7 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit ) //pTemp = pCur->pNext0; //pCur->pNext0 = pCur->pNext1; //pCur->pNext1 = pTemp; - ABC_SWAP( int, pLits[nLits+1], pLits[nLits+2] ); + ABC_SWAP( int, pLits[nLits], pLits[nLits+1] ); } //assert( pCur->pLits[1] == LitF ); assert( pLits[1] == LitF ); @@ -855,7 +898,10 @@ static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit ) // conflict detected - return the conflict clause //return pCur; if ( Value == Abc_LitIsCompl(pLits[0]) ) + { + p->nClauseConf++; return Cbs2_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur ); + } } return 0; } @@ -1086,8 +1132,8 @@ int Cbs2_ManPropagate2( Cbs2_Man_t * p, int Level ) int i, iLit, iFan, hClause; Cbs2_QueForEachEntry( p->pProp, iLit, i ) { - //if ( (hClause = Cbs2_ManPropagateClauses(p, Level, iLit)) ) - // return hClause; + if ( (hClause = Cbs2_ManPropagateClauses(p, Level, iLit)) ) + return hClause; Cbs2_ObjForEachFanout( p, Abc_Lit2Var(iLit), iFan ) { int iFanout = Abc_Lit2Var(iFan); @@ -1251,7 +1297,7 @@ int Cbs2_ManSolve1_rec( Cbs2_Man_t * p, int Level ) return hLearn1; hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 ); Cbs2_ManBumpClause( p, hClause ); -// Cbs2_ManPrintClauseNew( p, Level, hClause ); +// Cbs2_ManPrintCube( p, Level, hClause ); // if ( Level > Cbs2_ClauseDecLevel(p, hClause) ) // p->Pars.nBTThisNc++; p->Pars.nBTThis++; @@ -1315,7 +1361,7 @@ int Cbs2_ManSolve2_rec( Cbs2_Man_t * p, int Level ) return hLearn1; hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 ); Cbs2_ManBumpClause( p, hClause ); - //Cbs2_ManPrintClauseNew( p, Level, hClause ); + //Cbs2_ManPrintCube( p, Level, hClause ); // if ( Level > Cbs2_ClauseDecLevel(p, hClause) ) // p->Pars.nBTThisNc++; p->Pars.nBTThis++; @@ -1353,6 +1399,7 @@ int Cbs2_ManSolve( Cbs2_Man_t * p, int iLit ) else RetValue = 1; Cbs2_ManCancelUntil( p, 0 ); + Cbs2_ManCleanWatch( p ); Cbs2_ManBumpClean( p ); p->pJust.iHead = p->pJust.iTail = 0; p->pClauses.iHead = p->pClauses.iTail = 1; @@ -1377,6 +1424,7 @@ int Cbs2_ManSolve2( Cbs2_Man_t * p, int iLit, int iLit2 ) else RetValue = 1; Cbs2_ManCancelUntil( p, 0 ); + Cbs2_ManCleanWatch( p ); Cbs2_ManBumpClean( p ); p->pJust.iHead = p->pJust.iTail = 0; p->pClauses.iHead = p->pClauses.iTail = 1; @@ -1538,7 +1586,7 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS // solve for each output Gia_ManForEachCo( pAig, pRoot, i ) { -// printf( "\n" ); + //printf( "\nOutput %d\n", i ); Vec_IntClear( vCex ); if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) @@ -1606,7 +1654,7 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS if ( fVerbose ) Cbs2_ManSatPrintStats( p ); // printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro ); - printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nFails[0], p->nFails[1] ); + printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] ); Abc_PrintTime( 1, "JFront", p->timeJFront ); Cbs2_ManStop( p ); -- cgit v1.2.3