Version abc80207

5 files changed, 300 insertions, 54 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 9fc6a253..cb2da431 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -49,6 +49,8 @@ struct Mfs_Par_t_
     int           nGrowthLevel;  // the maximum allowed growth in level
     int           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
+    int           fMoreEffort;   // performs high-affort minimization
+    int           fSwapEdge;     // performs edge swapping
     int           fDelay;        // performs optimization for delay
     int           fVerbose;      // enable basic stats
     int           fVeryVerbose;  // enable detailed stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 332a6ad9..aed0abe5 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -74,10 +74,14 @@ clk = clock();
         return 1;
     }
     // solve the SAT problem
-    if ( p->pPars->fArea )
-        Abc_NtkMfsResubArea( p, pNode );
+    if ( p->pPars->fSwapEdge )
+        Abc_NtkMfsEdgeSwapEval( p, pNode );
     else
-        Abc_NtkMfsResubEdge( p, pNode );
+    {
+        Abc_NtkMfsResubNode( p, pNode );
+        if ( p->pPars->fMoreEffort )
+            Abc_NtkMfsResubNode2( p, pNode );
+    }
 p->timeSat += clock() - clk;
     return 1;
 }
@@ -140,12 +144,13 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, clk = clock();
+    int i, nFaninMax, clk = clock();
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
     assert( Abc_NtkIsLogic(pNtk) );
-    if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
+    nFaninMax = Abc_NtkGetFaninMax(pNtk);
+    if ( nFaninMax > MFS_FANIN_MAX )
     {
         printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
         return 1;
@@ -162,7 +167,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 
     // start the manager
     p = Mfs_ManAlloc( pPars );
-    p->pNtk  = pNtk;
+    p->pNtk = pNtk;
+    p->nFaninMax = nFaninMax;
     if ( pNtk->pExcare )
     {
         Abc_Ntk_t * pTemp;
@@ -170,7 +176,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         p->pCare = Abc_NtkToDar( pTemp, 0 );
         Abc_NtkDelete( pTemp );
     }
-    if ( pPars->fVerbose )
+//    if ( pPars->fVerbose )
     {
         if ( p->pCare != NULL )
             printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 54826bc1..ddd16407 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -49,6 +49,7 @@ struct Mfs_Man_t_
     Mfs_Par_t *         pPars;
     Abc_Ntk_t *         pNtk;
     Aig_Man_t *         pCare;
+    int                 nFaninMax;
     // intermeditate data for the node
     Vec_Ptr_t *         vRoots;    // the roots of the window
     Vec_Ptr_t *         vSupp;     // the support of the window
@@ -78,7 +79,6 @@ struct Mfs_Man_t_
     // performance statistics
     int                 nNodesTried;
     int                 nNodesResub;
-    int                 nNodesGained;
     int                 nMintsCare;
     int                 nMintsTotal;
     int                 nNodesBad;
@@ -119,8 +119,10 @@ extern Mfs_Man_t *      Mfs_ManAlloc( Mfs_Par_t * pPars );
 extern void             Mfs_ManStop( Mfs_Man_t * p );
 extern void             Mfs_ManClean( Mfs_Man_t * p );
 /*=== mfsResub.c ==========================================================*/
-extern int              Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
-extern int              Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern void             Abc_NtkMfsPrintResubStats( Mfs_Man_t * p );
+extern int              Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
 extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 67981d5a..519b855d 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -85,12 +85,12 @@ void Mfs_ManClean( Mfs_Man_t * p )
     if ( p->vDivs )
         Vec_PtrFree( p->vDivs );
     p->pAigWin = NULL;
-    p->pCnf   = NULL;
-    p->pSat   = NULL;
-    p->vRoots = NULL;
-    p->vSupp  = NULL;
-    p->vNodes = NULL;
-    p->vDivs  = NULL;
+    p->pCnf    = NULL;
+    p->pSat    = NULL;
+    p->vRoots  = NULL;
+    p->vSupp   = NULL;
+    p->vNodes  = NULL;
+    p->vDivs   = NULL;
 }
 
 /**Function*************************************************************
@@ -117,6 +117,11 @@ void Mfs_ManPrint( Mfs_Man_t * p )
         printf( "\n" );
         printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
             Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+        if ( p->pPars->fSwapEdge )
+            printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
+                p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
+        else
+            Abc_NtkMfsPrintResubStats( p );
     }
     else
     {
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index ae1132f2..1e9da4d2 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -57,6 +57,35 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
 
 /**Function*************************************************************
 
+  Synopsis    [Prints resub candidate stats.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
+{
+    Abc_Obj_t * pFanin, * pNode;
+    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
+    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
+    Abc_NtkForEachNode( p->pNtk, pNode, i )
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            {
+                nAreaCrits++;
+                nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
+            }
+        }
+    printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", 
+        nAreaCrits, nAreaExpanse );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Tries resubstitution.]
 
   Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
@@ -68,7 +97,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
 ***********************************************************************/
 int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
-    unsigned * pData, * pDataTot;
+    unsigned * pData;
     int RetValue, iVar, i;
     p->nSatCalls++;
     RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
@@ -77,17 +106,16 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
         return 1;
     p->nSatCexes++;
     // store the counter-example
-    pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
-    assert( pData[0] == 0 );
     Vec_IntForEachEntry( p->vProjVars, iVar, i )
     {
-        if ( sat_solver_var_value( p->pSat, iVar ) )
-            Aig_InfoSetBit( pData, i );
+        pData = Vec_PtrEntry( p->vDivCexes, i );
+        if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
+        {
+            assert( Aig_InfoHasBit(pData, p->nCexes) );
+            Aig_InfoXorBit( pData, p->nCexes );
+        }
     }
-    // AND the result with the previous ones
-    pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
-    for ( i = 0; i < p->nDivWords; i++ )
-        pDataTot[i] &= pData[i];
+    p->nCexes++;
     return 0;
 }
 
@@ -102,22 +130,19 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
 {
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
-    int iVar, i, nCands, clk;
+    int iVar, i, nCands, nWords, w, clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
 
     // clean simulation info
-    Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); 
-    pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
-    memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
     p->nCexes = 0;
-
     if ( fVeryVerbose )
     {
         printf( "\n" );
@@ -143,7 +168,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         if ( fVeryVerbose )
         printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
         p->nNodesResub++;
-//        p->nNodesGained += Abc_NodeMffcLabel(pNode);
+        if ( fSkipUpdate )
+            return 1;
 clk = clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
@@ -156,11 +182,6 @@ p->timeInt += clock() - clk;
     if ( fOnlyRemove )
         return 0;
 
-    // shift variables by 1
-    for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
-        p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
-    p->vFanins->nSize++;
-
     if ( fVeryVerbose )
     {
         for ( i = 0; i < 8; i++ )
@@ -180,37 +201,52 @@ p->timeInt += clock() - clk;
         if ( fVeryVerbose )
         {
             printf( "%3d: %2d ", p->nCexes, iVar );
-            pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
-//            Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
-                printf( "%d", Aig_InfoHasBit(pData, i) );
+            {
+                pData = Vec_PtrEntry( p->vDivCexes, i );
+                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+            }
             printf( "\n" );
         }
 
         // find the next divisor to try
-        pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+        nWords = Aig_BitWordNum(p->nCexes);
+        assert( nWords <= p->nDivWords );
         for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
-            if ( Aig_InfoHasBit( pData, iVar ) )
+        {
+            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            for ( w = 0; w < nWords; w++ )
+                if ( pData[w] != ~0 )
+                    break;
+            if ( w == nWords )
                 break;
+        }
         if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
             return 0;
+
         pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
         if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
         {
             if ( fVeryVerbose )
             printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
             p->nNodesResub++;
-//            p->nNodesGained += Abc_NodeMffcLabel(pNode);
+            if ( fSkipUpdate )
+                return 1;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
-            // update the network
-//            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
             Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+            // update the network
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
         }
+        if ( p->nCexes >= p->pPars->nDivMax )
+            break;
     }
     return 0;
 }
@@ -226,16 +262,155 @@ p->timeInt += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
 {
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData, * pData2;
+    int pCands[MFS_FANIN_MAX];
+    int iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
     Abc_Obj_t * pFanin;
-    int i;
+    Hop_Obj_t * pFunc;
+    assert( iFanin >= 0 );
+    assert( iFanin2 >= 0 || iFanin2 == -1 );
+
+    // clean simulation info
+    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
+    p->nCexes = 0;
+    if ( fVeryVerbose )
+    {
+        printf( "\n" );
+        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanins = %d/%d (out of %d). MFFC = %d\n", 
+            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
+            iFanin, iFanin2, Abc_ObjFaninNum(pNode), 
+            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+    {
+        if ( i == iFanin || i == iFanin2 )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    {
+        if ( fVeryVerbose )
+        printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
+        p->nNodesResub++;
+clk = clock();
+        // derive the function
+        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        // update the network
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+        return 1;
+    }
+
+    if ( fVeryVerbose )
+    {
+        for ( i = 0; i < 11; i++ )
+            printf( " " );
+        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+            if ( i == iFanin || i == iFanin2 )
+                printf( "*" );
+            else
+                printf( "%c", 'a' + i );
+        printf( "\n" );
+    }
+    iVar = iVar2 = -1;
+    while ( 1 )
+    {
+        if ( fVeryVerbose )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
-                return 1;
+            printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
+            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
+            {
+                pData = Vec_PtrEntry( p->vDivCexes, i );
+                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+            }
+            printf( "\n" );
+        }
+
+        // find the next divisor to try
+        nWords = Aig_BitWordNum(p->nCexes);
+        assert( nWords <= p->nDivWords );
+        fBreak = 0;
+        for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
+        {
+            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
+            {
+                pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
+                for ( w = 0; w < nWords; w++ )
+                    if ( (pData[w] | pData2[w]) != ~0 )
+                        break;
+                if ( w == nWords )
+                {
+                    fBreak = 1;
+                    break;
+                }
+            }
+            if ( fBreak )
+                break;
+        }
+        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
+            return 0;
+
+        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
+        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) )
+        {
+            if ( fVeryVerbose )
+            printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
+            p->nNodesResub++;
+clk = clock();
+            // derive the function
+            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
+            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) );
+            Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) );
+            // update the network
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+            return 1;
         }
+        if ( p->nCexes >= p->pPars->nDivMax )
+            break;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
     return 0;
 }
 
@@ -250,25 +425,81 @@ int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin;
     int i;
+    // try replacing area critical fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
         if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 return 1;
         }
+    // try removing redundant edges
+    if ( !p->pPars->fArea )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+            if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
+            {
+                if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+                    return 1;
+            }
+    }
+    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
+        return 0;
+    // try replacing area critical fanins while adding two new fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
+            if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                 return 1;
         }
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin, * pFanin2;
+    int i, k;
+/*
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+                return 1;
+        }
+*/
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return 0;
+    // try replacing one area critical fanin and one other fanin while adding two new fanins
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            // consider second fanin to remove at the same time
+            Abc_ObjForEachFanin( pNode, pFanin2, k )
+            {
+                if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
+                    return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////