Version abc80314

18 files changed, 519 insertions, 137 deletions

diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index f0b0f3bc..13275377 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -48,11 +48,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     p->pPars = pPars;
     p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
     p->nDivsLimit = 200;
-    // memory
-    p->vMemory = Vec_IntStart( 1 << 16 );
     // internal nodes
     p->nNodesAlloc = 512;
     p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
+    // memory
+    p->vMemory = Vec_IntStart( 4 * p->nWords * p->nNodesAlloc );
     // set up hash table
     p->nTableSize = (1 << p->pPars->nVarsMax);
     p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
@@ -69,7 +69,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     p->pIsfOR = &p->IsfOR;  Bdc_IsfStart( p, p->pIsfOR );
     p->pIsfAL = &p->IsfAL;  Bdc_IsfStart( p, p->pIsfAL );
     p->pIsfAR = &p->IsfAR;  Bdc_IsfStart( p, p->pIsfAR );   
-    return p;
+    return p; 
 }
 
 /**Function*************************************************************
@@ -85,6 +85,18 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
 ***********************************************************************/
 void Bdc_ManFree( Bdc_Man_t * p )
 {
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Bi-decomposition stats: Calls = %d.  Nodes = %d. Reuse = %d.\n", 
+            p->numCalls, p->numNodes, p->numReuse );
+        printf( "ANDs = %d.  ORs = %d.  Weak = %d.  Muxes = %d.  Memory = %.2f K\n", 
+            p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
+        PRT( "Cache", p->timeCache );
+        PRT( "Check", p->timeCheck );
+        PRT( "Muxes", p->timeMuxes );
+        PRT( "Supps", p->timeSupps );
+        PRT( "TOTAL", p->timeTotal );
+    }
     Vec_IntFree( p->vMemory );
     Vec_IntFree( p->vSpots );
     Vec_PtrFree( p->vTruths );
@@ -118,7 +130,8 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
     // add constant 1
     pNode = Bdc_FunNew( p );
     pNode->Type = BDC_TYPE_CONST1;
-    pNode->puFunc = NULL;
+    pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
+    Kit_TruthFill( pNode->puFunc, p->nVars );
     pNode->uSupp = 0;
     Bdc_TableAdd( p, pNode );
     // add variables
@@ -192,6 +205,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
 int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
 {
     Bdc_Isf_t Isf, * pIsf = &Isf;
+    int clk = clock();
     assert( nVars <= p->pPars->nVarsMax );
     // set current manager parameters
     p->nVars = nVars;
@@ -213,8 +227,14 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n
     Bdc_SuppMinimize( p, pIsf );
     // call decomposition
     p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
+    p->timeTotal += clock() - clk;
+    p->numCalls++;
+    p->numNodes += p->nNodesNew;
     if ( p->pRoot == NULL )
         return -1;
+    if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
+        printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
+//    assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
     return p->nNodesNew;
 }
 
diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c
index 13a33196..55ce97a0 100644
--- a/src/aig/bdc/bdcDec.c
+++ b/src/aig/bdc/bdcDec.c
@@ -30,6 +30,82 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v, clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // compute support
+    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
+        Kit_TruthSupport( pIsf->puOff, p->nVars );
+    // go through the support variables
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( (pIsf->uSupp & (1 << v)) == 0 )
+            continue;
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+        Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+        if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+            continue;
+//        if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+//            continue;
+        // remove the variable
+        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+//        Kit_TruthExist( pIsf->puOn, p->nVars, v );
+//        Kit_TruthExist( pIsf->puOff, p->nVars, v );
+        pIsf->uSupp &= ~(1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of the ISF.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int v, clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    // go through the support variables
+    pIsf->uSupp = 0;
+    for ( v = 0; v < p->nVars; v++ )
+    {
+        if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) && 
+             !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
+              continue;
+        if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+        {
+            Kit_TruthExist( pIsf->puOn, p->nVars, v );
+            Kit_TruthExist( pIsf->puOff, p->nVars, v );
+            continue;
+        }
+        pIsf->uSupp |= (1 << v);
+    }
+    if ( p->pPars->fVerbose )
+        p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Updates the ISF of the right after the left was decompoosed.]
 
   Description []
@@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     // check if there is any reuse for the components
     if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
     {
+        p->numReuse++;
+        p->numOrs++;
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
     if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
     {
+        p->numReuse++;
+        p->numAnds++;
         Bdc_IsfCopy( pIsfL, p->pIsfAL );
         Bdc_IsfCopy( pIsfR, p->pIsfAR );
         return BDC_TYPE_AND; 
@@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     // compare the two-component costs
     if ( WeightOr > WeightAnd )
     {
+        if ( WeightOr < BDC_SCALE )
+            p->numWeaks++;
+        p->numOrs++;
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
+    if ( WeightAnd < BDC_SCALE )
+        p->numWeaks++;
+    p->numAnds++;
     Bdc_IsfCopy( pIsfL, p->pIsfAL );
     Bdc_IsfCopy( pIsfR, p->pIsfAR );
     return BDC_TYPE_AND;
@@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
 {
     int Var, VarMin, nSuppMin, nSuppCur;
     unsigned uSupp0, uSupp1;
+    int clk;
+    if ( p->pPars->fVerbose )
+        clk = clock();
     VarMin = -1;
     nSuppMin = 1000;
     for ( Var = 0; Var < p->nVars; Var++ )
@@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
         {
             nSuppMin = nSuppCur;
             VarMin = Var;
-//            break;
+            break;
         }
     }
     if ( VarMin >= 0 )
@@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
         Bdc_SuppMinimize( p, pIsfL );
         Bdc_SuppMinimize( p, pIsfR );
     }
+    if ( p->pPars->fVerbose )
+        p->timeMuxes += clock() - clk;
     return VarMin;
 }
 
@@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
     Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
     Bdc_Isf_t IsfL, * pIsfL = &IsfL;
     Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+    int iVar, clk;
 /*
 printf( "Init function (%d):\n", LocalCounter );
 Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
@@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
 */
     // check computed results
     assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
-    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+    if ( p->pPars->fVerbose )
+        clk = clock();
+    pFunc = Bdc_TableLookup( p, pIsf );
+    if ( p->pPars->fVerbose )
+        p->timeCache += clock() - clk;
+    if ( pFunc )
         return pFunc;
     // decide on the decomposition type
+    if ( p->pPars->fVerbose )
+        clk = clock();
     Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+    if ( p->pPars->fVerbose )
+        p->timeCheck += clock() - clk;
     if ( Type == BDC_TYPE_MUX )
     {
-        int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        if ( p->pPars->fVerbose )
+            clk = clock();
+        iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        if ( p->pPars->fVerbose )
+            p->timeMuxes += clock() - clk;
+        p->numMuxes++;
         pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
         pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
         if ( pFunc0 == NULL || pFunc1 == NULL )
@@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
         // create new gate
         pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
     }
-    if ( pFunc == NULL )
-        return NULL;
-    assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
     return pFunc;
 }
 
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index 5fda4301..afba0e67 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -106,6 +106,20 @@ struct Bdc_Man_t_
     Bdc_Isf_t * pIsfAR, IsfAR;
     // internal memory manager
     Vec_Int_t *      vMemory;      // memory for internal truth tables
+    // statistics
+    int              numCalls;
+    int              numNodes;
+    int              numMuxes;
+    int              numAnds;
+    int              numOrs;
+    int              numWeaks;
+    int              numReuse;
+    // runtime
+    int              timeCache;
+    int              timeCheck;
+    int              timeMuxes;
+    int              timeSupps;
+    int              timeTotal;
 };
 
 // working with complemented attributes of objects
@@ -132,11 +146,12 @@ static inline void        Bdc_IsfNot( Bdc_Isf_t * p )                   { unsign
 
 /*=== bdcDec.c ==========================================================*/
 extern Bdc_Fun_t *      Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern int              Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc );
 /*=== bdcTable.c ==========================================================*/
 extern Bdc_Fun_t *      Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
 extern void             Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
 extern void             Bdc_TableClear( Bdc_Man_t * p );
-extern void             Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
 extern int              Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
 
 #ifdef __cplusplus
diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c
index b7f10344..3a6ed126 100644
--- a/src/aig/bdc/bdcTable.c
+++ b/src/aig/bdc/bdcTable.c
@@ -30,39 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Minimizes the support of the ISF.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
-{
-    int v;
-    // compute support
-    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
-        Kit_TruthSupport( pIsf->puOff, p->nVars );
-    // go through the support variables
-    for ( v = 0; v < p->nVars; v++ )
-    {
-        if ( (pIsf->uSupp & (1 << v)) == 0 )
-            continue;
-        Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
-        Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
-        if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
-            continue;
-        // remove the variable
-        Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
-        Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
-        pIsf->uSupp &= ~(1 << v);
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Checks containment of the function in the ISF.]
 
   Description []
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index a765ec30..e814840f 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -21,6 +21,9 @@
 #include "darInt.h"
 #include "kit.h"
 
+#include "bdc.h"
+#include "bdcInt.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,6 +47,9 @@ struct Ref_Man_t_
     Kit_Graph_t *    pGraphBest;     // the best factored form
     int              GainBest;       // the best gain
     int              LevelBest;      // the level of node with the best gain
+    // bi-decomposition
+    Bdc_Par_t        DecPars;        // decomposition parameters
+    Bdc_Man_t *      pManDec;        // decomposition manager
     // node statistics
     int              nNodesInit;     // the initial number of nodes
     int              nNodesTried;    // the number of nodes tried
@@ -111,6 +117,11 @@ Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     p->vMemory      = Vec_IntAlloc( 1 << 16 );
     p->vCutNodes    = Vec_PtrAlloc( 256 );
     p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
+    // alloc bi-decomposition manager
+    p->DecPars.nVarsMax = pPars->nLeafMax;
+    p->DecPars.fVerbose = pPars->fVerbose;
+    p->DecPars.fVeryVerbose = 0;
+//    p->pManDec = Bdc_ManAlloc( &p->DecPars );
     return p;
 }
 
@@ -151,6 +162,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p )
 ***********************************************************************/
 void Dar_ManRefStop( Ref_Man_t * p )
 {
+    if ( p->pManDec )
+        Bdc_ManFree( p->pManDec );
     if ( p->pPars->fVerbose )
         Dar_ManRefPrintStats( p );
     Vec_VecFree( p->vCuts );
@@ -381,6 +394,13 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         if ( RetValue > -1 )
         {
             pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+    int RetValue;
+    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
             if ( nNodesAdded > -1 )
             {
@@ -403,9 +423,17 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         // try negative phase
         Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+//        Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
         if ( RetValue > -1 )
         {
             pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+    int RetValue;
+    RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+    printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
             if ( nNodesAdded > -1 )
             {
@@ -426,6 +454,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
                 Kit_GraphFree( pGraphCur );
         }
     }
+
     return p->GainBest;
 }
 
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 06a93cf0..23e3ce8d 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -564,6 +564,7 @@ extern void            Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVa
 extern void            Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
 extern void            Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
+extern int             Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar );
 extern void            Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index dab60132..9ddc7562 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -520,6 +520,64 @@ void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes negative cofactor of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
+                 return 0;
+        return 1;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
+                 return 0;
+            return 1;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
+                 return 0;
+        return 1;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
+                 return 0;
+        return 1;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
+                 return 0;
+        return 1;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
+                     return 0;
+            pOnset += 2*Step;
+            pOffset += 2*Step;
+        }
+        return 1;
+    }
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f366a612..4262cd0d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -93,6 +93,7 @@ static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAig            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBidec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOrder          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -275,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "aig",           Abc_CommandAig,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
+    Cmd_CommandAdd( pAbc, "Various",      "bidec",         Abc_CommandBidec,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
@@ -5202,6 +5204,69 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandBidec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+    extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkIsAigLogic(pNtk) )
+    {
+        fprintf( pErr, "Bi-decomposition only works when node functions are AIGs (run \"aig\").\n" );
+        return 1;
+    }
+    Abc_NtkBidecResyn( pNtk, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: bidec [-vh]\n" );
+    fprintf( pErr, "\t         applies bi-decomposition to local functions of the nodes\n" );
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr, * pFile;
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
new file mode 100644
index 00000000..ad332314
--- /dev/null
+++ b/src/base/abci/abcBidec.c
@@ -0,0 +1,126 @@
+/**CFile****************************************************************
+
+  FileName    [abcBidec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface to bi-decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+#include "bdc.h"
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int i;
+    assert( nVars <= 16 );
+    // derive truth table
+    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        Extra_TruthNot( pTruth, pTruth, nVars );
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
+    for ( i = nVars + 1; i < p->nNodes; i++ )
+    {
+        pFunc = Bdc_FunWithId( p, i );
+        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+    }
+    return Bdc_FunCopyHop(p->pRoot);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Abc_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    assert( Abc_NtkIsLogic(pNtk) );
+    if ( !Abc_NtkToAig(pNtk) )
+        return;
+    pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
+    pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax > 15 )
+    {
+        if ( fVerbose )
+        printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
+        pPars->nVarsMax = 15;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) > 15 )
+            continue;
+        nNodes1 = Hop_DagSize(pObj->pData);
+        pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL );
+        nNodes2 = Hop_DagSize(pObj->pData);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+    if ( fVerbose )
+    {
+    printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
+    PRT( "Total runtime", clock() - clk );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index a20925b2..35ec473f 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -34,7 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O
 static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
 
 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
-extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk );
+extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         return NULL;
     If_ManStop( pIfMan );
     if ( pPars->fBidec && pPars->nLutSize <= 8 )
-        Abc_NtkBidecResyn( pNtkNew );
+        Abc_NtkBidecResyn( pNtkNew, 0 );
 
     // duplicate EXDC
     if ( pNtk->pExdc )
@@ -256,7 +256,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
 //    if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
-//        If_CutRotatePins( pIfMan, pCutBest );
+    If_CutRotatePins( pIfMan, pCutBest );
     if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
     {
         If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
@@ -551,86 +551,6 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
 }
 
 
-#include "bdc.h"
-#include "bdcInt.h"
-
-static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
-
-/**Function*************************************************************
-
-  Synopsis    [Resynthesizes nodes using bi-decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
-{
-    unsigned * pTruth;
-    Bdc_Fun_t * pFunc;
-    int i;
-    // derive truth table
-    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
-    if ( Hop_IsComplement(pRoot) )
-        Extra_TruthNot( pTruth, pTruth, nVars );
-    // decompose truth table
-    Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
-    // convert back into HOP
-    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
-    for ( i = 0; i < nVars; i++ )
-        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
-    for ( i = nVars + 1; i < p->nNodes; i++ )
-    {
-        pFunc = Bdc_FunWithId( p, i );
-        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
-    }
-    return Bdc_FunCopyHop(p->pRoot);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resynthesizes nodes using bi-decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk )
-{
-    Bdc_Par_t Pars = {0}, * pPars = &Pars;
-    Bdc_Man_t * p;
-    Abc_Obj_t * pObj;
-    Vec_Int_t * vTruth;
-    int i, nGainTotal = 0, nNodes1, nNodes2;
-    int clk = clock();
-    pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
-    if ( pPars->nVarsMax > 8 )
-    {
-        printf( "Resynthesis is not performed.\n" );
-        return;
-    }
-    vTruth = Vec_IntAlloc( 0 );
-    p = Bdc_ManAlloc( pPars );
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        nNodes1 = Hop_DagSize(pObj->pData);
-        pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth );
-        nNodes2 = Hop_DagSize(pObj->pData);
-        nGainTotal += nNodes1 - nNodes2;
-    }
-//    printf( "LUTs = %d.  Total gain in AIG nodes = %d.  ", Abc_NtkNodeNum(pNtk), nGainTotal );
-//    PRT( "Time", clock() - clk );
-    Bdc_ManFree( p );
-    Vec_IntFree( vTruth );
-}
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 55b724b8..a2f879e3 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -2,6 +2,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcAttach.c \
     src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \
+    src/base/abci/abcBidec.c \
     src/base/abci/abcBmc.c \
     src/base/abci/abcCas.c \
     src/base/abci/abcClpBdd.c \
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index 33bbdf74..59322cad 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -238,7 +238,7 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
     float PinDelays[32];
 //    int PinPerm[32];
     int i;
-    assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); 
+//    assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); 
     If_CutForEachLeaf( p, pCut, pLeaf, i )
         PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
     If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index a3a7e1ee..637a42b4 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -146,16 +146,18 @@ void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDe
         for ( i = 0; i < nVars - 1; i++ )
         {
             if ( pDelays[i] >= pDelays[i+1] )
+//            if ( pDelays[i] <= pDelays[i+1] )
                 continue;
             tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
             Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
+            if ( pOut && pIn )
             If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
             pTemp = pOut; pOut = pIn; pIn = pTemp;
             fChange = 1;
             Counter++;
         }
     }
-    if ( Counter & 1 )
+    if ( pOut && pIn && (Counter & 1) )
         If_TruthCopy( pOut, pIn, nVars );
 }
 
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 34911c20..80080d50 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -500,6 +500,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     Lpk_Man_t * p;
     Abc_Obj_t * pObj;
     double Delta;
+//    int * pnFanouts, nObjMax;
     int i, Iter, nNodes, nNodesPrev, clk = clock();
     assert( Abc_NtkIsLogic(pNtk) );
  
@@ -554,6 +555,14 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
         p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
         p->nTotalNodes = Abc_NtkNodeNum(pNtk);
     }
+/*
+    // save the number of fanouts of all objects
+    nObjMax = Abc_NtkObjNumMax( pNtk );
+    pnFanouts = ALLOC( int, nObjMax );
+    memset( pnFanouts, 0, sizeof(int) * nObjMax );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pnFanouts[pObj->Id] = Abc_ObjFanoutNum(pObj);
+*/
 
     // iterate over the network
     nNodesPrev = p->nNodesTotal;
@@ -604,6 +613,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
             break;
     }
     Abc_NtkStopReverseLevels( pNtk );
+/*
+    // report the fanout changes
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( i >= nObjMax )
+            continue;
+        if ( Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] == 0 )
+            continue;
+        printf( "%d ", Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] );
+    }
+    printf( "\n" );
+*/
 
     if ( pPars->fVerbose )
     {
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 4e4f7490..bde2ad42 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -100,7 +100,10 @@ p->timeSat += clock() - clk;
 ***********************************************************************/
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
-    int clk;
+    Hop_Obj_t * pObj;
+    extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
+
+    int nGain, clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
@@ -128,6 +131,16 @@ clk = clock();
     // solve the SAT problem
     Abc_NtkMfsSolveSat( p, pNode );
 p->timeSat += clock() - clk;
+    // minimize the local function of the node using bi-decomposition
+    assert( p->nFanins == Abc_ObjFaninNum(pNode) );
+    pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
+    nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
+    if ( nGain >= 0 )
+    {
+        p->nNodesDec++;
+        p->nNodesGained += nGain;
+        pNode->pData = pObj;    
+    }
     return 1;
 }
 
@@ -146,6 +159,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
 
+    Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
     ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
@@ -157,8 +171,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     nFaninMax = Abc_NtkGetFaninMax(pNtk);
     if ( nFaninMax > MFS_FANIN_MAX )
     {
-        printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
-        return 1;
+        printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
+        nFaninMax = MFS_FANIN_MAX;
     }
     // perform the network sweep
     Abc_NtkSweep( pNtk, 0 );
@@ -186,11 +200,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     {
         if ( p->pCare != NULL )
             printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
-        else
-            printf( "Performing optimization without constraints.\n" );
+//        else
+//            printf( "Performing optimization without constraints.\n" );
     }
     if ( !pPars->fResub )
-        printf( "Currently don't-cares are not used but the stats are printed.\n" );
+    {
+        pDecPars->nVarsMax = nFaninMax;
+        pDecPars->fVerbose = pPars->fVerbose;
+        p->vTruth = Vec_IntAlloc( 0 );
+        p->pManDec = Bdc_ManAlloc( pDecPars );
+    }
 
     // label the register outputs
     if ( p->pCare )
@@ -211,15 +230,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     {
         if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
             continue;
+        if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
+            continue;
         if ( !p->pPars->fVeryVerbose )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pPars->fResub )
             Abc_NtkMfsResub( p, pObj );
-        else
+        else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
             Abc_NtkMfsNode( p, pObj );
     }
     Extra_ProgressBarStop( pProgress );
     Abc_NtkStopReverseLevels( pNtk );
+
+    // perform the sweeping
+    if ( !pPars->fResub )
+    {
+        extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
+        Abc_NtkSweep( pNtk, 0 );
+        Abc_NtkBidecResyn( pNtk, 0 );
+    }
+
     p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
     p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
 
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 91395d03..f4da45ef 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -35,12 +35,13 @@ extern "C" {
 #include "cnf.h"
 #include "satSolver.h"
 #include "satStore.h"
+#include "bdc.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#define MFS_FANIN_MAX   10
+#define MFS_FANIN_MAX   12
 
 typedef struct Mfs_Man_t_ Mfs_Man_t;
 struct Mfs_Man_t_
@@ -64,6 +65,11 @@ struct Mfs_Man_t_
     int                 nCexes;    // the numbe rof current counter-examples
     int                 nSatCalls; 
     int                 nSatCexes;
+    // used for bidecomposition
+    Vec_Int_t *         vTruth;
+    Bdc_Man_t *         pManDec;
+    int                 nNodesDec;
+    int                 nNodesGained;
     // solving data
     Aig_Man_t *         pAigWin;   // window AIG with constraints
     Cnf_Dat_t *         pCnf;      // the CNF for the window
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 17ca40fc..f1b3f44c 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -131,6 +131,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
 //        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
 //            1.0-(p->dTotalRatios/p->nNodesTried) );
+        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d.\n", 
+            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
     }
 /*
     PRTP( "Win", p->timeWin            ,  p->timeTotal );
@@ -158,6 +160,10 @@ void Mfs_ManStop( Mfs_Man_t * p )
 {
     if ( p->pPars->fVerbose )
         Mfs_ManPrint( p );
+    if ( p->vTruth )
+        Vec_IntFree( p->vTruth );
+    if ( p->pManDec )
+        Bdc_ManFree( p->pManDec );
     if ( p->pCare )
         Aig_ManStop( p->pCare );
     if ( p->vSuppsInv )
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index efb09b39..2529e207 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -110,6 +110,18 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
         Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
         printf( "\n" );
     }
+
+    // map the care 
+    if ( p->nFanins > 4 )
+        return;
+    if ( p->nFanins == 4 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
+    if ( p->nFanins == 3 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24);
+    if ( p->nFanins == 2 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] <<  4) | (p->uCare[0] <<  8) | (p->uCare[0] << 12) |
+              (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
+    assert( p->nFanins != 1 );
 }
 
 ////////////////////////////////////////////////////////////////////////