summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaCSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaCSat.c')
-rw-r--r--src/aig/gia/giaCSat.c497
1 files changed, 345 insertions, 152 deletions
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 5fa9f40f..15faea72 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -32,6 +32,7 @@ struct Cbs_Par_t_
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
+ int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
@@ -48,7 +49,7 @@ struct Cbs_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
- int nSize; // allocated size
+ int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
@@ -59,7 +60,11 @@ struct Cbs_Man_t_
Gia_Man_t * pAig; // AIG manager
Cbs_Que_t pProp; // propagation queue
Cbs_Que_t pJust; // justification queue
+ Cbs_Que_t pClauses; // clause queue
+ Gia_Obj_t ** pIter; // iterator through clause vars
+ Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vModel; // satisfying assignment
+ Vec_Ptr_t * vTemp; // temporary storage
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
@@ -78,16 +83,26 @@ struct Cbs_Man_t_
static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
-static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; }
+static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); }
static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
-#define Cbs_QueForEachEntry( Que, pObj, i ) \
+static inline int Cbs_VarDecLevel( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
+static inline Gia_Obj_t * Cbs_VarReason0( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
+static inline Gia_Obj_t * Cbs_VarReason1( Cbs_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
+static inline int Cbs_ClauseDecLevel( Cbs_Man_t * p, int hClause ) { return Cbs_VarDecLevel( p, p->pClauses.pData[hClause] ); }
+
+#define Cbs_QueForEachEntry( Que, pObj, i ) \
for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+#define Cbs_ClauseForEachVar( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
+#define Cbs_ClauseForEachVar1( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc()
{
Cbs_Man_t * p;
p = ABC_CALLOC( Cbs_Man_t, 1 );
- p->pProp.nSize = p->pJust.nSize = 10000;
+ p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
- p->vModel = Vec_IntAlloc( 1000 );
+ p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->vModel = Vec_IntAlloc( 1000 );
+ p->vLevReas = Vec_IntAlloc( 1000 );
+ p->vTemp = Vec_PtrAlloc( 1000 );
Cbs_SetDefaultParams( &p->Pars );
return p;
}
@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc()
***********************************************************************/
void Cbs_ManStop( Cbs_Man_t * p )
{
+ Vec_IntFree( p->vLevReas );
Vec_IntFree( p->vModel );
+ Vec_PtrFree( p->vTemp );
+ ABC_FREE( p->pClauses.pData );
ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData );
ABC_FREE( p );
@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld )
p->iTail = iTailOld;
}
+/**Function*************************************************************
+
+ Synopsis [Finalized the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_QueFinish( Cbs_Que_t * p )
+{
+ int iHeadOld = p->iHead;
+ assert( p->iHead < p->iTail );
+ Cbs_QuePush( p, NULL );
+ p->iHead = p->iTail;
+ return iHeadOld;
+}
+
/**Function*************************************************************
@@ -400,7 +442,7 @@ static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p )
pObjMax = pObj;
}
}
- return pObjMax;
+ return pObjMax;
}
@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
Cbs_QueForEachEntry( p->pProp, pVar, i )
Cbs_VarUnassign( pVar );
p->pProp.iTail = iBound;
+ Vec_IntShrink( p->vLevReas, 3*iBound );
}
/**Function*************************************************************
@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
SeeAlso []
***********************************************************************/
-static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj )
+static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
{
Gia_Obj_t * pObjR = Gia_Regular(pObj);
assert( Gia_ObjIsCand(pObjR) );
assert( !Cbs_VarIsAssigned(pObjR) );
Cbs_VarAssign( pObjR );
Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ assert( pObjR->Value == ~0 );
+ pObjR->Value = p->pProp.iTail;
Cbs_QuePush( &p->pProp, pObjR );
+ Vec_IntPush( p->vLevReas, Level );
+ Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
+ Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
+ assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns clause size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManClauseSize( Cbs_Man_t * p, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t ** pIter;
+ for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
+ return pIter - pQue->pData - hClause ;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClause( Cbs_Man_t * p, int Level, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs_VarValue(pObj), Cbs_VarDecLevel(p, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClauseNew( Cbs_Man_t * p, int Level, int hClause )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%c%d ", Cbs_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj, * pReason;
+ int i, k, iLitLevel;
+ assert( pQue->pData[pQue->iHead] == NULL );
+ assert( pQue->iHead + 1 < pQue->iTail );
+/*
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ assert( pObj->fMark0 == 1 );
+ }
+*/
+ // compact literals
+ Vec_PtrClear( p->vTemp );
+ for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Vec_PtrPush( p->vTemp, pObj );
+ // check decision level
+ iLitLevel = Cbs_VarDecLevel( p, pObj );
+ if ( iLitLevel < Level )
+ {
+ pQue->pData[k++] = pObj;
+ continue;
+ }
+ assert( iLitLevel == Level );
+ pReason = Cbs_VarReason0( p, pObj );
+ if ( pReason == pObj ) // no reason
+ {
+ assert( pQue->pData[pQue->iHead] == NULL );
+ pQue->pData[pQue->iHead] = pObj;
+ continue;
+ }
+ Cbs_QuePush( pQue, pReason );
+ pReason = Cbs_VarReason1( p, pObj );
+ if ( pReason != pObj ) // second reason
+ Cbs_QuePush( pQue, pReason );
+ }
+ assert( pQue->pData[pQue->iHead] != NULL );
+ pQue->iTail = k;
+ // clear the marks
+ Vec_PtrForEachEntry( p->vTemp, pObj, i )
+ pObj->fMark0 = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManAnalyze( Cbs_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ assert( Cbs_VarIsAssigned(pVar) );
+ assert( Cbs_VarIsAssigned(pFan0) );
+ assert( pFan1 == NULL || Cbs_VarIsAssigned(pFan1) );
+ assert( Cbs_QueIsEmpty( pQue ) );
+ Cbs_QuePush( pQue, NULL );
+ Cbs_QuePush( pQue, pVar );
+ Cbs_QuePush( pQue, pFan0 );
+ if ( pFan1 )
+ Cbs_QuePush( pQue, pFan1 );
+ Cbs_ManDeriveReason( p, Level );
+ return Cbs_QueFinish( pQue );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs resolution of two clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs_ManResolve( Cbs_Man_t * p, int Level, int hClause0, int hClause1 )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i, LevelMax = -1, LevelCur;
+ assert( pQue->pData[hClause0] != NULL );
+ assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
+/*
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+*/
+ assert( Cbs_QueIsEmpty( pQue ) );
+ Cbs_QuePush( pQue, NULL );
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs_QuePush( pQue, pObj );
+ LevelCur = Cbs_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs_QuePush( pQue, pObj );
+ LevelCur = Cbs_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ pQue->pData[i]->fMark0 = 1;
+ Cbs_ManDeriveReason( p, LevelMax );
+ return Cbs_QueFinish( pQue );
}
/**Function*************************************************************
Synopsis [Propagates a variable.]
- Description [Returns 1 if conflict; 0 if no conflict.]
+ Description [Returns clause handle if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
-static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Cbs_VarValue(pVar) )
{ // value is 1
if ( Value0 == 0 || Value1 == 0 ) // one is 0
- return 1;
+ {
+ if ( Value0 == 0 && Value1 != 0 )
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
+ if ( Value0 != 0 && Value1 == 0 )
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
+ assert( Value0 == 0 && Value1 == 0 );
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ }
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_ObjChild0(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_ObjChild1(pVar) );
+ Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
return 0;
}
// value is 0
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
- return 1;
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
if ( Value0 == 1 || Value1 == 1 ) // one is 1
{
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // second is unassigned
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
assert( Cbs_VarIsJust(pVar) );
@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso []
***********************************************************************/
-static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
{
int Value0, Value1;
assert( !Gia_IsComplement(pVar) );
@@ -522,12 +788,12 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
if ( Value0 == 0 || Value1 == 0 ) // one is 0
return 0;
if ( Value0 == 1 && Value1 == 1 ) // both are 1
- return 1;
+ return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
assert( Value0 == 1 || Value1 == 1 );
if ( Value0 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
if ( Value1 == 2 ) // first is unassigned
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+ Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
return 0;
}
@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
SeeAlso []
***********************************************************************/
-int Cbs_ManPropagate( Cbs_Man_t * p )
+int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
{
+ int hClause;
Gia_Obj_t * pVar;
int i, k;
while ( 1 )
{
Cbs_QueForEachEntry( p->pProp, pVar, i )
{
- if ( Cbs_ManPropagateOne( p, pVar ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
+ return hClause;
}
p->pProp.iHead = p->pProp.iTail;
k = p->pJust.iHead;
@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
{
if ( Cbs_VarIsJust( pVar ) )
p->pJust.pData[k++] = pVar;
- else if ( Cbs_ManPropagateTwo( p, pVar ) )
- return 1;
+ else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
+ return hClause;
}
if ( k == p->pJust.iTail )
break;
@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
Synopsis [Solve the problem recursively.]
- Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
+ Description [Returns learnt clause if unsat, NULL if sat or undecided.]
SideEffects []
SeeAlso []
-
+
***********************************************************************/
-int Cbs_ManSolve_rec( Cbs_Man_t * p )
-{
- Gia_Obj_t * pVar;
+int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
+{
+ Cbs_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pVar, * pDecVar;
+ int hClause, hLearn0, hLearn1;
int iPropHead, iJustHead, iJustTail;
// propagate assignments
assert( !Cbs_QueIsEmpty(&p->pProp) );
- if ( Cbs_ManPropagate( p ) )
- return 1;
+ if ( (hClause = Cbs_ManPropagate( p, Level )) )
+ return hClause;
// check for satisfying assignment
assert( Cbs_QueIsEmpty(&p->pProp) );
if ( Cbs_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
- p->Pars.nBTThis++;
p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs_ManCheckLimits( p ) )
- return 1;
+ return 0;
// remember the state before branching
iPropHead = p->pProp.iHead;
Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
pVar = Cbs_ManDecideMaxFF( p );
else assert( 0 );
assert( Cbs_VarIsJust( pVar ) );
- // decide using fanout count!
- if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
- {
- // decide on first fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- if ( !Cbs_ManSolve_rec( p ) )
- return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- Cbs_ManCancelUntil( p, iPropHead );
- Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
- // decide on second fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
- }
+ // chose decision variable using fanout count
+ if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
else
- {
- // decide on first fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
- if ( !Cbs_ManSolve_rec( p ) )
- return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- Cbs_ManCancelUntil( p, iPropHead );
- Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
- // decide on second fanin
- Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
- }
- if ( !Cbs_ManSolve_rec( p ) )
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+ // decide on first fanin
+ Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+ if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
return 0;
- if ( Cbs_ManCheckLimits( p ) )
- return 1;
- return 1;
+ if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+ return hLearn0;
+ Cbs_ManCancelUntil( p, iPropHead );
+ Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+ if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+ return hLearn1;
+ hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 );
+// Cbs_ManPrintClauseNew( p, Level, hClause );
+// if ( Level > Cbs_ClauseDecLevel(p, hClause) )
+// p->Pars.nBTThisNc++;
+ p->Pars.nBTThis++;
+ return hClause;
}
/**Function*************************************************************
@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
***********************************************************************/
int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
{
-// Gia_Obj_t * pTemp;
-// int i;
- int RetValue;
-// Gia_ManForEachObj( p->pAig, pTemp, i )
-// assert( pTemp->fMark0 == 0 );
+ int RetValue = 0;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
- p->Pars.nBTThis = p->Pars.nJustThis = 0;
- Cbs_ManAssign( p, pObj );
- RetValue = Cbs_ManSolve_rec( p );
- if ( RetValue == 0 )
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
Cbs_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
+ p->pClauses.iHead = p->pClauses.iTail = 1;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs_ManCheckLimits( p ) )
- return -1;
+ RetValue = -1;
return RetValue;
}
/**Function*************************************************************
- Synopsis [Procedure to test the new SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cbs_ManSolveTest( Gia_Man_t * pGia )
-{
- extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
- int nConfsMax = 1000;
- int CountUnsat, CountSat, CountUndec;
- Cbs_Man_t * p;
- Vec_Int_t * vCex;
- Vec_Int_t * vVisit;
- Gia_Obj_t * pRoot;
- int i, RetValue, clk = clock();
- Gia_ManCreateRefs( pGia );
- // create logic network
- p = Cbs_ManAlloc();
- p->pAig = pGia;
- // prepare AIG
- Gia_ManCleanValue( pGia );
- Gia_ManCleanMark0( pGia );
- Gia_ManCleanMark1( pGia );
-// vCex = Vec_IntAlloc( 100 );
- vVisit = Vec_IntAlloc( 100 );
- // solve for each output
- CountUnsat = CountSat = CountUndec = 0;
- Gia_ManForEachCo( pGia, pRoot, i )
- {
- if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
- continue;
-
-// Gia_ManIncrementTravId( pGia );
-
-//printf( "Output %6d : ", i );
-// iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
-// RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex );
- RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
- if ( RetValue == 1 )
- CountUnsat++;
- else if ( RetValue == -1 )
- CountUndec++;
- else
- {
-// int iLit, k;
- vCex = Cbs_ReadModel( p );
-
-// printf( "complemented = %d. ", Gia_ObjFaninC0(pRoot) );
-//printf( "conflicts = %6d max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis );
-// Vec_IntForEachEntry( vCex, iLit, k )
-// printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) );
-// printf( "\n" );
-
- Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
- assert( RetValue == 0 );
- CountSat++;
- }
-// Gia_ManCheckMark0( p );
-// Gia_ManCheckMark1( p );
- }
- Cbs_ManStop( p );
-// Vec_IntFree( vCex );
- Vec_IntFree( vVisit );
- printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec );
- ABC_PRT( "Time", clock() - clk );
-}
-
-
-/**Function*************************************************************
-
Synopsis [Prints statistics of the manager.]
Description []
@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus )
+Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p;
@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
+ Gia_ManFillValue( pAig ); // maps nodes into trail ids
// create logic network
p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs;
@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
}
else
{
- printf( "Constant 0 output of SRM!!!\n" );
+// printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
@@ -838,12 +1025,15 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
p->Pars.fUseHighest = 1;
p->Pars.fUseLowest = 0;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+// printf( "\n" );
+/*
if ( status == -1 )
{
p->Pars.fUseHighest = 0;
p->Pars.fUseLowest = 1;
status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
}
+*/
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
continue;
}
p->nSatSat++;
- p->nConfUnsat += p->Pars.nBTThis;
+ p->nConfSat += p->Pars.nBTThis;
// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += clock() - clk;
@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = clock() - clkTotal;
-// Cbs_ManSatPrintStats( p );
+ if ( fVerbose )
+ Cbs_ManSatPrintStats( p );
+// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
Cbs_ManStop( p );
*pvStatus = vStatus;
+
// printf( "Total number of cex literals = %d. (Ave = %d)\n",
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-02 22:07:26 +0000