From c8008383cf3a3180701a8527fa3f83a3873aff58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 27 Jan 2018 20:29:46 -0800 Subject: Experiments with circuit-based SAT. --- src/aig/gia/giaCSat2.c | 251 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 225 insertions(+), 26 deletions(-) (limited to 'src/aig/gia/giaCSat2.c') diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat2.c index b75055ec..3e924811 100644 --- a/src/aig/gia/giaCSat2.c +++ b/src/aig/gia/giaCSat2.c @@ -68,14 +68,15 @@ struct Cbs2_Man_t_ Cbs2_Que_t pJust; // justification queue Cbs2_Que_t pClauses; // clause queue int * pIter; // iterator through clause vars - //Vec_Int_t * vLevReas; // levels and decisions Vec_Int_t * vModel; // satisfying assignment Vec_Int_t * vTemp; // temporary storage // internal data Vec_Str_t vAssign; Vec_Str_t vValue; Vec_Int_t vLevReason; - Vec_Int_t vIndex; + Vec_Int_t vFanoutN; + Vec_Int_t vFanout0; + Vec_Int_t vJStore; // SAT calls statistics int nSatUnsat; // the number of proofs int nSatSat; // the number of failure @@ -175,14 +176,15 @@ Cbs2_Man_t * Cbs2_ManAlloc( Gia_Man_t * pGia ) p->pClauses.pData = ABC_ALLOC( int, p->pClauses.nSize ); p->pClauses.iHead = p->pClauses.iTail = 1; p->vModel = Vec_IntAlloc( 1000 ); - //p->vLevReas = Vec_IntAlloc( 1000 ); p->vTemp = Vec_IntAlloc( 1000 ); p->pAig = pGia; Cbs2_SetDefaultParams( &p->Pars ); Vec_StrFill( &p->vAssign, Gia_ManObjNum(pGia), 0 ); Vec_StrFill( &p->vValue, Gia_ManObjNum(pGia), 0 ); Vec_IntFill( &p->vLevReason, 3*Gia_ManObjNum(pGia), -1 ); - Vec_IntFill( &p->vIndex, Gia_ManObjNum(pGia), -1 ); + Vec_IntFill( &p->vFanout0, Gia_ManObjNum(pGia), 0 ); + Vec_IntFill( &p->vFanoutN, 2*Gia_ManObjNum(pGia), 0 ); + Vec_IntGrow( &p->vJStore, 1000 ); return p; } @@ -202,8 +204,9 @@ void Cbs2_ManStop( Cbs2_Man_t * p ) Vec_StrErase( &p->vAssign ); Vec_StrErase( &p->vValue ); Vec_IntErase( &p->vLevReason ); - Vec_IntErase( &p->vIndex ); - //Vec_IntFree( p->vLevReas ); + Vec_IntErase( &p->vFanout0 ); + Vec_IntErase( &p->vFanoutN ); + Vec_IntErase( &p->vJStore ); Vec_IntFree( p->vModel ); Vec_IntFree( p->vTemp ); ABC_FREE( p->pClauses.pData ); @@ -569,18 +572,6 @@ static inline void Cbs2_ManPrintClause( Cbs2_Man_t * p, int Level, int hClause ) printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, iObj), Cbs2_VarDecLevel(p, iObj) ); printf( "\n" ); } - -/**Function************************************************************* - - Synopsis [Prints conflict clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline void Cbs2_ManPrintClauseNew( Cbs2_Man_t * p, int Level, int hClause ) { Cbs2_Que_t * pQue = &(p->pClauses); int i, iObj; @@ -816,6 +807,31 @@ static inline int Cbs2_ManPropagateTwo( Cbs2_Man_t * p, int iVar, int Level ) return 0; } +/**Function************************************************************* + + Synopsis [Propagates a variable.] + + Description [Returns 1 if conflict; 0 if no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs2_ManPropagateUnassigned( Cbs2_Man_t * p, int iVar, int Level ) +{ + Gia_Obj_t * pVar = Gia_ManObj( p->pAig, iVar ); int Value0, Value1; + assert( !Gia_IsComplement(pVar) ); + assert( Gia_ObjIsAnd(pVar) ); + assert( !Cbs2_VarIsAssigned(p, iVar) ); + Value0 = Cbs2_VarFanin0Value(p, pVar, iVar); + Value1 = Cbs2_VarFanin1Value(p, pVar, iVar); + if ( Value0 == 0 || Value1 == 0 ) // the output becomes 0 + Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 1), Level, Gia_ObjFaninId0(pVar, iVar), 0 ); + if ( Value0 == 1 && Value1 == 1 ) // the output becomes 1 + Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 0), Level, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) ); +} + /**Function************************************************************* Synopsis [Propagates all variables.] @@ -852,6 +868,57 @@ int Cbs2_ManPropagate( Cbs2_Man_t * p, int Level ) } return 0; } +/* +int Cbs2_ManPropagate( Cbs2_Man_t * p, int Level ) +{ + int i, iVar, iFan, hClause; + Cbs2_QueForEachEntry( p->pProp, iVar, i ) + { + Cbs2_ObjForEachFanout( p, iVar, iFan ) + { + if ( !Cbs2_VarIsAssigned(p, iFan) ) + Cbs2_ManPropagateUnassigned( p, iFan, Level ); + else if ( (hClause = Cbs2_ManPropagateOne(p, iFan, Level)) ) + return hClause; + } + if ( (hClause = Cbs2_ManPropagateOne( p, iVar, Level )) ) + return hClause; + } + p->pProp.iHead = p->pProp.iTail; + return 0; +} +*/ + +/**Function************************************************************* + + Synopsis [Updates J-frontier.] + + Description [Returns 1 if found SAT; 0 if continues solving.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cbs2_ManUpdateFrontier( Cbs2_Man_t * p, int iPropHeadOld ) +{ + int i, iVar, iJustTailOld = p->pJust.iTail; + assert( Cbs2_QueIsEmpty(&p->pProp) ); + // visit old frontier nodes + Cbs2_QueForEachEntry( p->pJust, iVar, i ) + if ( Cbs2_VarIsJust(p, Gia_ManObj(p->pAig, iVar), iVar) ) + Cbs2_QuePush( &p->pJust, iVar ); + // append new nodes + p->pProp.iHead = iPropHeadOld; + Cbs2_QueForEachEntry( p->pProp, iVar, i ) + if ( Cbs2_VarIsJust(p, Gia_ManObj(p->pAig, iVar), iVar) ) + Cbs2_QuePush( &p->pJust, iVar ); + p->pProp.iHead = p->pProp.iTail; + // update the head of the frontier + p->pJust.iHead = iJustTailOld; + // return 1 if the queue is empty + return Cbs2_QueIsEmpty(&p->pJust); +} /**Function************************************************************* @@ -886,15 +953,64 @@ int Cbs2_ManSolve_rec( Cbs2_Man_t * p, int Level ) iPropHead = p->pProp.iHead; Cbs2_QueStore( &p->pJust, &iJustHead, &iJustTail ); // find the decision variable + assert( p->Pars.fUseHighest ); + iVar = Cbs2_ManDecideHighest( p ); + pVar = Gia_ManObj( p->pAig, iVar ); + assert( Cbs2_VarIsJust(p, pVar, iVar) ); + // chose decision variable using fanout count + if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) ) + iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pVar, iVar)); + else + iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pVar, iVar)); + // decide on first fanin + Cbs2_ManAssign( p, iDecLit, Level+1, 0, 0 ); + if ( !(hLearn0 = Cbs2_ManSolve_rec( p, Level+1 )) ) + return 0; + if ( pQue->pData[hLearn0] != Abc_Lit2Var(iDecLit) ) + return hLearn0; + Cbs2_ManCancelUntil( p, iPropHead ); + Cbs2_QueRestore( &p->pJust, iJustHead, iJustTail ); + // decide on second fanin + Cbs2_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 ); + if ( !(hLearn1 = Cbs2_ManSolve_rec( p, Level+1 )) ) + return 0; + if ( pQue->pData[hLearn1] != Abc_Lit2Var(iDecLit) ) + return hLearn1; + hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 ); +// Cbs2_ManPrintClauseNew( p, Level, hClause ); +// if ( Level > Cbs2_ClauseDecLevel(p, hClause) ) +// p->Pars.nBTThisNc++; + p->Pars.nBTThis++; + return hClause; +} /* - if ( p->Pars.fUseHighest ) - pVar = Cbs2_ManDecideHighest( p ); - else if ( p->Pars.fUseLowest ) - pVar = Cbs2_ManDecideLowest( p ); - else if ( p->Pars.fUseMaxFF ) - pVar = Cbs2_ManDecideMaxFF( p ); - else assert( 0 ); -*/ +int Cbs2_ManSolve_rec( Cbs2_Man_t * p, int Level ) +{ + Gia_Obj_t * pVar; + Cbs2_Que_t * pQue = &(p->pClauses); + int iPropHead, iJustHead, iJustTail; + int hClause, hLearn0, hLearn1, iVar, iDecLit; + int iPropHeadOld = p->pProp.iHead; + // propagate assignments + assert( !Cbs2_QueIsEmpty(&p->pProp) ); + if ( (hClause = Cbs2_ManPropagate( p, Level )) ) + return hClause; + // check for satisfying assignment + assert( Cbs2_QueIsEmpty(&p->pProp) ); +// if ( Cbs2_QueIsEmpty(&p->pJust) ) +// return 0; + if ( Cbs2_ManUpdateFrontier(p, iPropHeadOld) ) + return 0; + // quit using resource limits + p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); + if ( Cbs2_ManCheckLimits( p ) ) + return 0; + // remember the state before branching + iPropHead = p->pProp.iHead; +// Cbs2_QueStore( &p->pJust, &iJustHead, &iJustTail ); + iJustHead = p->pJust.iHead; + iJustTail = p->pJust.iTail; + // find the decision variable assert( p->Pars.fUseHighest ); iVar = Cbs2_ManDecideHighest( p ); pVar = Gia_ManObj( p->pAig, iVar ); @@ -925,6 +1041,7 @@ int Cbs2_ManSolve_rec( Cbs2_Man_t * p, int Level ) p->Pars.nBTThis++; return hClause; } +*/ /**Function************************************************************* @@ -1014,6 +1131,82 @@ void Cbs2_ManSatPrintStats( Cbs2_Man_t * p ) ABC_PRT( "Total time", p->timeTotal ); } +/**Function************************************************************* + + Synopsis [Create fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cbs2_ObjCreateFanout( Cbs2_Man_t * p, int iObj, int iFan0, int iFan1 ) +{ + Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 0), Vec_IntEntry(&p->vFanout0, iFan0) ); + Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 1), Vec_IntEntry(&p->vFanout0, iFan1) ); + Vec_IntWriteEntry( &p->vFanout0, iFan0, Abc_Var2Lit(iObj, 0) ); + Vec_IntWriteEntry( &p->vFanout0, iFan1, Abc_Var2Lit(iObj, 1) ); +} +void Cbs2_ObjDeleteFanout( Cbs2_Man_t * p, int iObj ) +{ + Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 0), 0 ); + Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 1), 0 ); + Vec_IntWriteEntry( &p->vFanout0, iObj, 0 ); +} +void Cbs2_ManCreateFanout_rec( Cbs2_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan0, iFan1; + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + iFan0 = Gia_ObjFaninId0(pObj, iObj); + iFan1 = Gia_ObjFaninId1(pObj, iObj); + if ( !Vec_IntEntry(&p->vFanout0, iFan0) ) Cbs2_ManCreateFanout_rec( p, iFan0 ); + if ( !Vec_IntEntry(&p->vFanout0, iFan1) ) Cbs2_ManCreateFanout_rec( p, iFan1 ); + Cbs2_ObjCreateFanout( p, iObj, iFan0, iFan1 ); +} +void Cbs2_ManDeleteFanout_rec( Cbs2_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan0, iFan1; + Cbs2_ObjDeleteFanout( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + iFan0 = Gia_ObjFaninId0(pObj, iObj); + iFan1 = Gia_ObjFaninId1(pObj, iObj); + if ( Vec_IntEntry(&p->vFanout0, iFan0) ) Cbs2_ManDeleteFanout_rec( p, iFan0 ); + if ( Vec_IntEntry(&p->vFanout0, iFan1) ) Cbs2_ManDeleteFanout_rec( p, iFan1 ); +} + +#define Cbs2_ObjForEachFanout( p, iObj, iFanLit ) \ + for ( iFanLit = Vec_IntEntry(&p->vFanout0, iObj); iFanLit; iFanLit = Vec_IntEntry(&p->vFanoutN, iFanLit) ) + +void Cbs2_ManPrintFanouts( Cbs2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int iObj, iFanLit; + Gia_ManForEachObj( p->pAig, pObj, iObj ) + { + printf( "Fanouts of node %d: ", iObj ); + Cbs2_ObjForEachFanout( p, iObj, iFanLit ) + printf( "%d ", Abc_Lit2Var(iFanLit) ); + printf( "\n" ); + } +} +void Cbs2_ManCheckFanouts( Cbs2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int iObj; + Gia_ManForEachObj( p->pAig, pObj, iObj ) + { + assert( Vec_IntEntry(&p->vFanout0, iObj) == 0 ); + assert( Vec_IntEntry(&p->vFanoutN, Abc_Var2Lit(iObj, 0)) == 0 ); + assert( Vec_IntEntry(&p->vFanoutN, Abc_Var2Lit(iObj, 1)) == 0 ); + } +} + /**Function************************************************************* Synopsis [Procedure to test the new SAT solver.] @@ -1075,6 +1268,12 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS clk = Abc_Clock(); p->Pars.fUseHighest = 1; p->Pars.fUseLowest = 0; + + //Cbs2_ManCreateFanout_rec( p, Gia_ObjFaninId0p(pAig, pRoot) ); + //Cbs2_ManPrintFanouts( p ); + //Cbs2_ManDeleteFanout_rec( p, Gia_ObjFaninId0p(pAig, pRoot) ); + //Cbs2_ManCheckFanouts( p ); + status = Cbs2_ManSolve( p, Gia_ObjFaninLit0p(pAig, pRoot) ); // printf( "\n" ); /* -- cgit v1.2.3