Version abc80707

5 files changed, 788 insertions, 427 deletions

diff --git a/abc.dsp b/abc.dsp
index 9c8c84ff..c7755203 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3322,6 +3322,10 @@ SOURCE=.\src\aig\nwk\nwkMerge.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\nwk\nwkMerge.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\nwk\nwkObj.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 0eb6cd81..e3d0a061 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -108,21 +108,6 @@ struct Nwk_Obj_t_
     Nwk_Obj_t **       pFanio;         // fanins/fanouts
 };
 
-
-// the LUT merging parameters
-typedef struct Nwk_LMPars_t_  Nwk_LMPars_t;
-struct Nwk_LMPars_t_
-{
-    int  nMaxLutSize;       // the max LUT size for merging (N=5)
-    int  nMaxSuppSize;      // the max total support size after merging (S=5)
-    int  nMaxDistance;      // the max number of nodes separating LUTs
-    int  nMaxLevelDiff;     // the max difference in levels
-    int  nMaxFanout;        // the max number of fanouts to traverse
-    int  fUseTfiTfo;        // enables the use of TFO/TFO nodes as candidates
-    int  fVeryVerbose;      // enables additional verbose output
-    int  fVerbose;          // enables verbose output
-};
-
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkMerge.c b/src/aig/nwk/nwkMerge.c
index 57de7f04..1a5255d3 100644
--- a/src/aig/nwk/nwkMerge.c
+++ b/src/aig/nwk/nwkMerge.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "nwk.h"
+#include "nwkMerge.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,192 +31,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the fanins of the node with the current trav ID.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Nwk_ManMarkFanins_rec( Nwk_Obj_t * pLut, int nLevMin )
-{
-    Nwk_Obj_t * pNext;
-    int i;
-    if ( !Nwk_ObjIsNode(pLut) )
-        return;
-    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
-        return;
-    Nwk_ObjSetTravIdCurrent( pLut );
-    if ( Nwk_ObjLevel(pLut) < nLevMin )
-        return;
-    Nwk_ObjForEachFanin( pLut, pNext, i )
-        Nwk_ManMarkFanins_rec( pNext, nLevMin );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the fanouts of the node with the current trav ID.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Nwk_ManMarkFanouts_rec( Nwk_Obj_t * pLut, int nLevMax, int nFanMax )
-{
-    Nwk_Obj_t * pNext;
-    int i;
-    if ( !Nwk_ObjIsNode(pLut) )
-        return;
-    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
-        return;
-    Nwk_ObjSetTravIdCurrent( pLut );
-    if ( Nwk_ObjLevel(pLut) > nLevMax )
-        return;
-    if ( Nwk_ObjFanoutNum(pLut) > nFanMax )
-        return;
-    Nwk_ObjForEachFanout( pLut, pNext, i )
-        Nwk_ManMarkFanouts_rec( pNext, nLevMax, nFanMax );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the circle of nodes around the given set.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Nwk_ManCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax )
-{
-    Nwk_Obj_t * pObj, * pNext;
-    int i, k;
-    Vec_PtrClear( vNext );
-    Vec_PtrForEachEntry( vStart, pObj, i )
-    {
-        Nwk_ObjForEachFanin( pObj, pNext, k )
-        {
-            if ( !Nwk_ObjIsNode(pNext) )
-                continue;
-            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
-                continue;
-            Nwk_ObjSetTravIdCurrent( pNext );
-            Vec_PtrPush( vNext, pNext );
-        }
-        Nwk_ObjForEachFanout( pObj, pNext, k )
-        {
-            if ( !Nwk_ObjIsNode(pNext) )
-                continue;
-            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
-                continue;
-            Nwk_ObjSetTravIdCurrent( pNext );
-            if ( Nwk_ObjFanoutNum(pNext) > nFanMax )
-                continue;
-            Vec_PtrPush( vNext, pNext );
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the circle of nodes removes from the given one.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Nwk_ManCollectNonOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
-{
-    Vec_Ptr_t * vTemp;
-    Nwk_Obj_t * pObj;
-    int i, k;
-    Vec_PtrClear( vCands );
-    if ( pPars->nMaxSuppSize - Nwk_ObjFaninNum(pLut) <= 1 )
-        return;
-
-    // collect nodes removed by this distance
-    assert( pPars->nMaxDistance > 0 );
-    Vec_PtrClear( vStart );
-    Vec_PtrPush( vStart, pLut );
-    Nwk_ManIncrementTravId( pLut->pMan );
-    Nwk_ObjSetTravIdCurrent( pLut );
-    for ( i = 1; i < pPars->nMaxDistance; i++ )
-    {
-        Nwk_ManCollectCircle( vStart, vNext, pPars->nMaxFanout );
-        vTemp = vStart;
-        vStart = vNext;
-        vNext = vTemp;
-        // collect the nodes in vStart
-        Vec_PtrForEachEntry( vStart, pObj, k )
-            Vec_PtrPush( vCands, pObj );
-    }
-
-    // mark the TFI/TFO nodes
-    Nwk_ManIncrementTravId( pLut->pMan );
-    if ( pPars->fUseTfiTfo )
-        Nwk_ObjSetTravIdCurrent( pLut );
-    else
-    {
-        Nwk_ObjSetTravIdPrevious( pLut );
-        Nwk_ManMarkFanins_rec( pLut, Nwk_ObjLevel(pLut) - pPars->nMaxDistance );
-        Nwk_ObjSetTravIdPrevious( pLut );
-        Nwk_ManMarkFanouts_rec( pLut, Nwk_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout );
-    }
-
-    // collect nodes satisfying the following conditions:
-    // - they are close enough in terms of distance
-    // - they are not in the TFI/TFO of the LUT
-    // - they have no more than the given number of fanins
-    // - they have no more than the given diff in delay
-    k = 0;
-    Vec_PtrForEachEntry( vCands, pObj, i )
-    {
-        if ( Nwk_ObjIsTravIdCurrent(pObj) )
-            continue;
-        if ( Nwk_ObjFaninNum(pLut) + Nwk_ObjFaninNum(pObj) > pPars->nMaxSuppSize )
-            continue;
-        if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
-             Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
-             continue;
-        Vec_PtrWriteEntry( vCands, k++, pObj );
-    }
-    Vec_PtrShrink( vCands, k );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Count the total number of fanins.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand )
-{
-    Nwk_Obj_t * pFanin;
-    int i, nCounter = Nwk_ObjFaninNum(pLut);
-    Nwk_ObjForEachFanin( pCand, pFanin, i )
-        nCounter += !pFanin->MarkC;
-    return nCounter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects overlapping candidates.]
+  Synopsis    [Allocates the graph.]
 
   Description []
                
@@ -224,94 +40,19 @@ int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwl_ManCollectOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+Nwk_Grf_t * Nwk_ManGraphAlloc( int nVertsMax )
 {
-    Nwk_Obj_t * pFanin, * pObj;
-    int i, k;
-    // mark fanins of pLut
-    Nwk_ObjForEachFanin( pLut, pFanin, i )
-        pFanin->MarkC = 1;
-    // collect the matching fanouts of each fanin of the node
-    Vec_PtrClear( vCands );
-    Nwk_ManIncrementTravId( pLut->pMan );
-    Nwk_ObjSetTravIdCurrent( pLut );
-    Nwk_ObjForEachFanin( pLut, pFanin, i )
-    {
-        if ( !Nwk_ObjIsNode(pFanin) )
-            continue;
-        if ( Nwk_ObjFanoutNum(pFanin) > pPars->nMaxFanout )
-            continue;
-        Nwk_ObjForEachFanout( pFanin, pObj, k )
-        {
-            if ( !Nwk_ObjIsNode(pObj) )
-                continue;
-            if ( Nwk_ObjIsTravIdCurrent( pObj ) )
-                continue;
-            Nwk_ObjSetTravIdCurrent( pObj );
-            // check the difference in delay
-            if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
-                 Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
-                 continue;
-            // check the total number of fanins of the node
-            if ( Nwk_ManCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize )
-                continue;
-            Vec_PtrPush( vCands, pObj );
-        }
-    }
-    // unmark fanins of pLut
-    Nwk_ObjForEachFanin( pLut, pFanin, i )
-        pFanin->MarkC = 0;
+    Nwk_Grf_t * p;
+    p = ALLOC( Nwk_Grf_t, 1 );
+    memset( p, 0, sizeof(Nwk_Grf_t) );
+    p->nVertsMax = nVertsMax;
+    p->nEdgeHash = Aig_PrimeCudd( 3 * nVertsMax );
+    p->pEdgeHash = CALLOC( Nwk_Edg_t *, p->nEdgeHash );
+    p->pMemEdges = Aig_MmFixedStart( sizeof(Nwk_Edg_t), p->nEdgeHash );
+    p->vPairs    = Vec_IntAlloc( 1000 );
+    return p;
 }
 
-
-
-#define MAX_LIST  16
-
-// edge of the graph
-typedef struct Nwk_Edg_t_  Nwk_Edg_t;
-struct Nwk_Edg_t_
-{
-    int             iNode1;      // the first node
-    int             iNode2;      // the second node
-    Nwk_Edg_t *     pNext;       // the next edge
-};
-
-// vertex of the graph
-typedef struct Nwk_Vrt_t_  Nwk_Vrt_t;
-struct Nwk_Vrt_t_
-{
-    int             Id;          // the vertex number
-    int             iPrev;       // the previous vertex in the list
-    int             iNext;       // the next vertex in the list
-    int             nEdges;      // the number of edges
-    int             pEdges[0];   // the array of edges
-};
-
-// the connectivity graph
-typedef struct Nwk_Grf_t_  Nwk_Grf_t;
-struct Nwk_Grf_t_
-{
-    // preliminary graph representation
-    int             nObjs;       // the number of objects
-    int             nVertsPre;   // the upper bound on the number of vertices
-    int             nEdgeHash;   // approximate number of edges
-    Nwk_Edg_t **    pEdgeHash;   // hash table for edges
-    Aig_MmFixed_t * pMemEdges;   // memory for edges
-    // graph representation
-    int             nEdges;      // the number of edges
-    int             nVerts;      // the number of vertices
-    Nwk_Vrt_t **    pVerts;      // the array of vertices
-    Aig_MmFlex_t *  pMemVerts;   // memory for vertices
-    // intermediate data
-    int             pLists1[MAX_LIST+1];
-    int             pLists2[MAX_LIST+1];
-    // the results of matching
-    Vec_Int_t *     vPairs;
-    // mappings graph into LUTs and back
-    int *           pMapLut2Id;
-    int *           pMapId2Lut;
-};
-
 /**Function*************************************************************
 
   Synopsis    [Deallocates the graph.]
@@ -328,8 +69,8 @@ void Nwk_ManGraphFree( Nwk_Grf_t * p )
     if ( p->vPairs )    Vec_IntFree( p->vPairs );
     if ( p->pMemEdges ) Aig_MmFixedStop( p->pMemEdges, 0 );
     if ( p->pMemVerts ) Aig_MmFlexStop( p->pMemVerts, 0 );
-    FREE( p->pEdgeHash );
     FREE( p->pVerts );
+    FREE( p->pEdgeHash );
     FREE( p->pMapLut2Id );
     FREE( p->pMapId2Lut );
     free( p );
@@ -337,7 +78,7 @@ void Nwk_ManGraphFree( Nwk_Grf_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates the graph.]
+  Synopsis    [Prepares the graph for solving the problem.]
 
   Description []
                
@@ -346,41 +87,20 @@ void Nwk_ManGraphFree( Nwk_Grf_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Nwk_Grf_t * Nwk_ManGraphAlloc( int nObjs, int nVertsPre )
+void Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p )
 {
-    Nwk_Grf_t * p;
-    p = ALLOC( Nwk_Grf_t, 1 );
-    memset( p, 0, sizeof(Nwk_Grf_t) );
-    p->nObjs      = nObjs;
-    p->nVertsPre  = nVertsPre;
-    p->nEdgeHash  = Aig_PrimeCudd(10 * nVertsPre);
-    p->pEdgeHash  = CALLOC( Nwk_Edg_t *, p->nEdgeHash );
-    p->pMemEdges  = Aig_MmFixedStart( sizeof(Nwk_Edg_t), p->nEdgeHash );
-    p->pMapLut2Id = ALLOC( int, nObjs );
-    p->pMapId2Lut = ALLOC( int, nVertsPre );
-    p->vPairs     = Vec_IntAlloc( 1000 );
-    memset( p->pMapLut2Id, 0xff, sizeof(int) * nObjs );
-    memset( p->pMapId2Lut, 0xff, sizeof(int) * nVertsPre );
-    return p;
+    p->nMemBytes1 = 
+        sizeof(Nwk_Grf_t) +
+        sizeof(void *) * p->nEdgeHash + 
+        sizeof(int) * (p->nObjs + p->nVertsMax) +
+        sizeof(Nwk_Edg_t) * p->nEdges;
+    p->nMemBytes2 = 
+        sizeof(Nwk_Vrt_t) * p->nVerts + 
+        sizeof(int) * 2 * p->nEdges;
+    printf( "Memory usage stats:  Preprocessing = %.2f Mb.  Solving = %.2f Mb.\n",
+        1.0 * p->nMemBytes1 / (1<<20), 1.0 * p->nMemBytes2 / (1<<20) );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Finds or adds the edge to the graph.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Nwk_ManGraphSetMapping( Nwk_Grf_t * p, int iLut )
-{
-    p->nVerts++;
-    p->pMapId2Lut[p->nVerts] = iLut;
-    p->pMapLut2Id[iLut] = p->nVerts;
-}
 
 /**Function*************************************************************
 
@@ -393,10 +113,10 @@ static inline void Nwk_ManGraphSetMapping( Nwk_Grf_t * p, int iLut )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 )
+void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 )
 {
     Nwk_Edg_t * pEntry;
-    int Key;
+    unsigned Key;
     if ( iLut1 == iLut2 )
         return;
     if ( iLut1 > iLut2 )
@@ -406,7 +126,9 @@ static inline void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 )
         iLut2 = Key;
     }
     assert( iLut1 < iLut2 );
-    Key = (741457 * iLut1 + 4256249 * iLut2) % p->nEdgeHash;
+    if ( p->nObjs < iLut2 )
+        p->nObjs = iLut2;
+    Key = (unsigned)(741457 * iLut1 + 4256249 * iLut2) % p->nEdgeHash;
     for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext )
         if ( pEntry->iNode1 == iLut1 && pEntry->iNode2 == iLut2 )
             return;
@@ -420,7 +142,7 @@ static inline void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 )
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the graph for solving the problem.]
+  Synopsis    [Adds one entry to the list.]
 
   Description []
                
@@ -444,7 +166,7 @@ static inline void Nwk_ManGraphListAdd( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the graph for solving the problem.]
+  Synopsis    [Deletes one entry from the list.]
 
   Description []
                
@@ -457,9 +179,15 @@ static inline void Nwk_ManGraphListDelete( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t
 {
     assert( *pList );
     if ( pVertex->iPrev )
+    {
+//        assert( p->pVerts[pVertex->iPrev]->iNext == pVertex->Id );
         p->pVerts[pVertex->iPrev]->iNext = pVertex->iNext;
+    }
     if ( pVertex->iNext )
-        p->pVerts[pVertex->iNext]->iNext = pVertex->iPrev;
+    {
+//        assert( p->pVerts[pVertex->iNext]->iPrev == pVertex->Id );
+        p->pVerts[pVertex->iNext]->iPrev = pVertex->iPrev;
+    }
     if ( *pList == pVertex->Id )
         *pList = pVertex->iNext;
     pVertex->iPrev = pVertex->iNext = 0;
@@ -480,20 +208,21 @@ static inline void Nwk_ManGraphListInsert( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex )
 {
     Nwk_Vrt_t * pNext;
     assert( pVertex->nEdges > 0 );
+
     if ( pVertex->nEdges == 1 )
     {
         pNext = p->pVerts[ pVertex->pEdges[0] ];
-        if ( pNext->nEdges >= MAX_LIST )
-            Nwk_ManGraphListAdd( p, p->pLists1 + MAX_LIST, pVertex );
+        if ( pNext->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListAdd( p, p->pLists1 + NWK_MAX_LIST, pVertex );
         else
             Nwk_ManGraphListAdd( p, p->pLists1 + pNext->nEdges, pVertex );
     }
     else
     {
-        if ( pVertex->nEdges >= MAX_LIST )
-            Nwk_ManGraphListAdd( p, p->pLists1 + MAX_LIST, pVertex );
+        if ( pVertex->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListAdd( p, p->pLists2 + NWK_MAX_LIST, pVertex );
         else
-            Nwk_ManGraphListAdd( p, p->pLists1 + pVertex->nEdges, pVertex );
+            Nwk_ManGraphListAdd( p, p->pLists2 + pVertex->nEdges, pVertex );
     }
 }
 
@@ -512,20 +241,21 @@ static inline void Nwk_ManGraphListExtract( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex )
 {
     Nwk_Vrt_t * pNext;
     assert( pVertex->nEdges > 0 );
+
     if ( pVertex->nEdges == 1 )
     {
         pNext = p->pVerts[ pVertex->pEdges[0] ];
-        if ( pNext->nEdges >= MAX_LIST )
-            Nwk_ManGraphListDelete( p, p->pLists1 + MAX_LIST, pVertex );
+        if ( pNext->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListDelete( p, p->pLists1 + NWK_MAX_LIST, pVertex );
         else
             Nwk_ManGraphListDelete( p, p->pLists1 + pNext->nEdges, pVertex );
     }
     else
     {
-        if ( pVertex->nEdges >= MAX_LIST )
-            Nwk_ManGraphListDelete( p, p->pLists1 + MAX_LIST, pVertex );
+        if ( pVertex->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListDelete( p, p->pLists2 + NWK_MAX_LIST, pVertex );
         else
-            Nwk_ManGraphListDelete( p, p->pLists1 + pVertex->nEdges, pVertex );
+            Nwk_ManGraphListDelete( p, p->pLists2 + pVertex->nEdges, pVertex );
     }
 }
 
@@ -544,23 +274,45 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
 {
     Nwk_Edg_t * pEntry;
     Nwk_Vrt_t * pVertex;
-    int * pnEdges, Key, nBytes, i;
-    // count the edges
-    pnEdges = CALLOC( int, p->nVerts );
-    for ( Key = 0; Key < p->nEdgeHash; Key++ )
-        for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext )
+    int * pnEdges, nBytes, i;
+    // allocate memory for the present objects
+    p->pMapLut2Id = ALLOC( int, p->nObjs+1 );
+    p->pMapId2Lut = ALLOC( int, p->nVertsMax+1 );
+    memset( p->pMapLut2Id, 0xff, sizeof(int) * (p->nObjs+1) );
+    memset( p->pMapId2Lut, 0xff, sizeof(int) * (p->nVertsMax+1) );
+    // mark present objects
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        assert( pEntry->iNode1 <= p->nObjs );
+        assert( pEntry->iNode2 <= p->nObjs );
+        p->pMapLut2Id[ pEntry->iNode1 ] = 0;
+        p->pMapLut2Id[ pEntry->iNode2 ] = 0;
+    }
+    // map objects
+    p->nVerts = 0;
+    for ( i = 0; i <= p->nObjs; i++ )
+    {
+        if ( p->pMapLut2Id[i] == 0 )
         {
-            // translate into vertices
-            assert( pEntry->iNode1 < p->nObjs );
-            assert( pEntry->iNode2 < p->nObjs );
-            pEntry->iNode1 = p->pMapLut2Id[pEntry->iNode1];
-            pEntry->iNode2 = p->pMapLut2Id[pEntry->iNode2];
-            // count the edges
-            assert( pEntry->iNode1 < p->nVerts );
-            assert( pEntry->iNode2 < p->nVerts );
-            pnEdges[pEntry->iNode1]++;
-            pnEdges[pEntry->iNode2]++;
+            p->pMapLut2Id[i] = ++p->nVerts;
+            p->pMapId2Lut[p->nVerts] = i;
         }
+    }
+    // count the edges and mark present objects
+    pnEdges = CALLOC( int, p->nVerts+1 );
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        // translate into vertices
+        assert( pEntry->iNode1 <= p->nObjs );
+        assert( pEntry->iNode2 <= p->nObjs );
+        pEntry->iNode1 = p->pMapLut2Id[pEntry->iNode1];
+        pEntry->iNode2 = p->pMapLut2Id[pEntry->iNode2];
+        // count the edges
+        assert( pEntry->iNode1 <= p->nVerts );
+        assert( pEntry->iNode2 <= p->nVerts );
+        pnEdges[pEntry->iNode1]++;
+        pnEdges[pEntry->iNode2]++;
+    }
     // allocate the real graph
     p->pMemVerts  = Aig_MmFlexStart();
     p->pVerts = ALLOC( Nwk_Vrt_t *, p->nVerts + 1 );
@@ -574,14 +326,13 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
         p->pVerts[i]->Id = i;
     }
     // add edges to the real graph
-    for ( Key = 0; Key < p->nEdgeHash; Key++ )
-        for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext )
-        {
-            pVertex = p->pVerts[pEntry->iNode1];
-            pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode2;
-            pVertex = p->pVerts[pEntry->iNode2];
-            pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode1;
-        }
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        pVertex = p->pVerts[pEntry->iNode1];
+        pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode2;
+        pVertex = p->pVerts[pEntry->iNode2];
+        pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode1;
+    }
     // put vertices into the data structure
     for ( i = 1; i <= p->nVerts; i++ )
     {
@@ -591,7 +342,7 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
     // clean up
     Aig_MmFixedStop( p->pMemEdges, 0 ); p->pMemEdges = NULL;
     FREE( p->pEdgeHash );
-    p->nEdgeHash = 0;
+//    p->nEdgeHash = 0;
     free( pnEdges );
 }
 
@@ -606,37 +357,116 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Nwk_ManGraphCheckLists( Nwk_Grf_t * p )
+{
+    Nwk_Vrt_t * pVertex, * pNext;
+    int i, j;
+    assert( p->pLists1[0] == 0 );
+    for ( i = 1; i <= NWK_MAX_LIST; i++ )
+        if ( p->pLists1[i] )
+        {
+            pVertex = p->pVerts[ p->pLists1[i] ];
+            assert( pVertex->nEdges == 1 );
+            pNext = p->pVerts[ pVertex->pEdges[0] ];
+            assert( pNext->nEdges == i || pNext->nEdges > NWK_MAX_LIST );
+        }
+    // find the next vertext to extract
+    assert( p->pLists2[0] == 0 );
+    assert( p->pLists2[1] == 0 );
+    for ( j = 2; j <= NWK_MAX_LIST; j++ )
+        if ( p->pLists2[j] )
+        {
+            pVertex = p->pVerts[ p->pLists2[j] ];
+            assert( pVertex->nEdges == j || pVertex->nEdges > NWK_MAX_LIST );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts the edge from one of the linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphVertexRemoveEdge( Nwk_Vrt_t * pThis, Nwk_Vrt_t * pNext )
+{
+    int k;
+    for ( k = 0; k < pThis->nEdges; k++ )
+        if ( pThis->pEdges[k] == pNext->Id )
+            break;
+    assert( k < pThis->nEdges );
+    pThis->nEdges--;
+    for ( ; k < pThis->nEdges; k++ )
+        pThis->pEdges[k] = pThis->pEdges[k+1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the problem after pulling out one edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Nwk_ManGraphUpdate( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex, Nwk_Vrt_t * pNext )
 {
-    Nwk_Vrt_t * pChanged;
+    Nwk_Vrt_t * pChanged, * pOther;
     int i, k;
-    // update neibors of pVertex
-    for ( i = 0; i < pVertex->nEdges; i++ )
+//    Nwk_ManGraphCheckLists( p );
+    Nwk_ManGraphListExtract( p, pVertex );
+    Nwk_ManGraphListExtract( p, pNext );
+    // update neihbors of pVertex
+    Nwk_VertexForEachAdjacent( p, pVertex, pChanged, i )
     {
-        pChanged = p->pVerts[ pVertex->pEdges[i] ];
+        if ( pChanged == pNext )
+            continue;
         Nwk_ManGraphListExtract( p, pChanged );
-        for ( k = 0; k < pChanged->nEdges; k++ )
-            if ( pChanged->pEdges[k] == pVertex->Id )
-                break;
-        assert( k < pChanged->nEdges );
-        pChanged->nEdges--;
-        for ( ; k < pChanged->nEdges; k++ )
-            pChanged->pEdges[k] = pChanged->pEdges[k+1];
+        // move those that use this one
+        if ( pChanged->nEdges > 1 )
+        Nwk_VertexForEachAdjacent( p, pChanged, pOther, k )
+        {
+            if ( pOther == pVertex || pOther->nEdges > 1 )
+                continue;
+            assert( pOther->nEdges == 1 );
+            Nwk_ManGraphListExtract( p, pOther );
+            pChanged->nEdges--;
+            Nwk_ManGraphListInsert( p, pOther );
+            pChanged->nEdges++;
+        }
+        // remove the edge
+        Nwk_ManGraphVertexRemoveEdge( pChanged, pVertex );
+        // add the changed vertex back
         if ( pChanged->nEdges > 0 )
             Nwk_ManGraphListInsert( p, pChanged );
     }
-    // update neibors of pNext
-    for ( i = 0; i < pNext->nEdges; i++ )
+    // update neihbors of pNext
+    Nwk_VertexForEachAdjacent( p, pNext, pChanged, i )
     {
-        pChanged = p->pVerts[ pNext->pEdges[i] ];
+        if ( pChanged == pVertex )
+            continue;
         Nwk_ManGraphListExtract( p, pChanged );
-        for ( k = 0; k < pChanged->nEdges; k++ )
-            if ( pChanged->pEdges[k] == pNext->Id )
-                break;
-        assert( k < pChanged->nEdges );
-        pChanged->nEdges--;
-        for ( ; k < pChanged->nEdges; k++ )
-            pChanged->pEdges[k] = pChanged->pEdges[k+1];
+        // move those that use this one
+        if ( pChanged->nEdges > 1 )
+        Nwk_VertexForEachAdjacent( p, pChanged, pOther, k )
+        {
+            if ( pOther == pNext || pOther->nEdges > 1 )
+                continue;
+            assert( pOther->nEdges == 1 );
+            Nwk_ManGraphListExtract( p, pOther );
+            pChanged->nEdges--;
+            Nwk_ManGraphListInsert( p, pOther );
+            pChanged->nEdges++;
+        }
+        // remove the edge
+        Nwk_ManGraphVertexRemoveEdge( pChanged, pNext );
+        // add the changed vertex back
         if ( pChanged->nEdges > 0 )
             Nwk_ManGraphListInsert( p, pChanged );
     }
@@ -651,11 +481,93 @@ void Nwk_ManGraphUpdate( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex, Nwk_Vrt_t * pNext )
         Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); 
         Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); 
     }
+//    Nwk_ManGraphCheckLists( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Solves the problem.]
+  Synopsis    [Counts the number of entries in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGraphListLength( Nwk_Grf_t * p, int List )
+{
+    Nwk_Vrt_t * pThis;
+    int fVerbose = 0;
+    int Counter = 0;
+    Nwk_ListForEachVertex( p, List, pThis )
+    {
+        if ( fVerbose && Counter < 20 )
+            printf( "%d ", p->pVerts[pThis->pEdges[0]]->nEdges );
+        Counter++;
+    }
+    if ( fVerbose )
+        printf( "\n" );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the adjacent vertex with the mininum number of edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Vrt_t * Nwk_ManGraphListFindMinEdge( Nwk_Grf_t * p, Nwk_Vrt_t * pVert )
+{
+    Nwk_Vrt_t * pThis, * pMinCost = NULL;
+    int k;
+    Nwk_VertexForEachAdjacent( p, pVert, pThis, k )
+    {
+        if ( pMinCost == NULL || pMinCost->nEdges > pThis->nEdges )
+            pMinCost = pThis;
+    }
+    return pMinCost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the best vertext in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Vrt_t * Nwk_ManGraphListFindMin( Nwk_Grf_t * p, int List )
+{
+    Nwk_Vrt_t * pThis, * pMinCost = NULL;
+    int k, Counter = 10000, BestCost = 1000000;
+    Nwk_ListForEachVertex( p, List, pThis )
+    {
+        for ( k = 0; k < pThis->nEdges; k++ )
+        {
+            if ( pMinCost == NULL || BestCost > p->pVerts[pThis->pEdges[k]]->nEdges )
+            {
+                BestCost = p->pVerts[pThis->pEdges[k]]->nEdges;
+                pMinCost = pThis;
+            }
+        }
+        if ( --Counter == 0 )
+            break;
+    }
+    return pMinCost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the problem by extracting one edge at a time.]
 
   Description []
                
@@ -668,34 +580,337 @@ void Nwk_ManGraphSolve( Nwk_Grf_t * p )
 {
     Nwk_Vrt_t * pVertex, * pNext;
     int i, j;
+    Nwk_ManGraphPrepare( p );
     while ( 1 )
     {
-        // find the next vertext to extract
-        for ( i = 1; i <= MAX_LIST; i++ )
+        // find the next vertex to extract
+        assert( p->pLists1[0] == 0 );
+        for ( i = 1; i <= NWK_MAX_LIST; i++ )
             if ( p->pLists1[i] )
             {
+//                printf( "%d ", i );
+//                printf( "ListA = %2d. Length = %5d.\n", i, Nwk_ManGraphListLength(p,p->pLists1[i]) );
                 pVertex = p->pVerts[ p->pLists1[i] ];
                 assert( pVertex->nEdges == 1 );
                 pNext = p->pVerts[ pVertex->pEdges[0] ];
-                // update the data-structures
                 Nwk_ManGraphUpdate( p, pVertex, pNext );
                 break;
             }
-        // find the next vertext to extract
-        for ( j = 2; j <= MAX_LIST; j++ )
+        if ( i < NWK_MAX_LIST + 1 )
+            continue;
+        // find the next vertex to extract
+        assert( p->pLists2[0] == 0 );
+        assert( p->pLists2[1] == 0 );
+        for ( j = 2; j <= NWK_MAX_LIST; j++ )
             if ( p->pLists2[j] )
             {
-                pVertex = p->pVerts[ p->pLists2[j] ];
-                assert( pVertex->nEdges == j || j == MAX_LIST );
-                // update the data-structures
+//                printf( "***%d ", j );
+//                printf( "ListB = %2d. Length = %5d.\n", j, Nwk_ManGraphListLength(p,p->pLists2[j]) );
+                pVertex = Nwk_ManGraphListFindMin( p, p->pLists2[j] ); 
+                assert( pVertex->nEdges == j || j == NWK_MAX_LIST );
+                pNext = Nwk_ManGraphListFindMinEdge( p, pVertex );
                 Nwk_ManGraphUpdate( p, pVertex, pNext );
                 break;
             }
-        if ( i == MAX_LIST + 1 && j == MAX_LIST + 1 )
+        if ( j == NWK_MAX_LIST + 1 )
             break;
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reads graph from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Grf_t * Nwk_ManLutMergeReadGraph( char * pFileName )
+{
+    Nwk_Grf_t * p;
+    FILE * pFile;
+    char Buffer[100];
+    int nNodes, nEdges, iNode1, iNode2;
+    pFile = fopen( pFileName, "r" );
+    fscanf( pFile, "%s %d", Buffer, &nNodes );
+    fscanf( pFile, "%s %d", Buffer, &nEdges );
+    p = Nwk_ManGraphAlloc( nNodes );
+    while ( fscanf( pFile, "%s %d %d", Buffer, &iNode1, &iNode2 ) == 3 )
+        Nwk_ManGraphHashEdge( p, iNode1, iNode2 );
+    assert( p->nEdges == nEdges );
+    fclose( pFile );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the graph coming from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLutMergeGraphTest( char * pFileName )
+{
+    int nPairs;
+    Nwk_Grf_t * p;
+    int clk = clock();
+    p = Nwk_ManLutMergeReadGraph( pFileName );
+    PRT( "Reading", clock() - clk );
+    clk = clock();
+    Nwk_ManGraphSolve( p );
+    printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
+        p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+    PRT( "Solving", clock() - clk );
+    nPairs = Vec_IntSize(p->vPairs)/2;
+    Nwk_ManGraphReportMemoryUsage( p );
+    Nwk_ManGraphFree( p );
+    return nPairs;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanins of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkFanins_rec( Nwk_Obj_t * pLut, int nLevMin )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( !Nwk_ObjIsNode(pLut) )
+        return;
+    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pLut );
+    if ( Nwk_ObjLevel(pLut) < nLevMin )
+        return;
+    Nwk_ObjForEachFanin( pLut, pNext, i )
+        Nwk_ManMarkFanins_rec( pNext, nLevMin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanouts of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkFanouts_rec( Nwk_Obj_t * pLut, int nLevMax, int nFanMax )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( !Nwk_ObjIsNode(pLut) )
+        return;
+    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pLut );
+    if ( Nwk_ObjLevel(pLut) > nLevMax )
+        return;
+    if ( Nwk_ObjFanoutNum(pLut) > nFanMax )
+        return;
+    Nwk_ObjForEachFanout( pLut, pNext, i )
+        Nwk_ManMarkFanouts_rec( pNext, nLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes around the given set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax )
+{
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k;
+    Vec_PtrClear( vNext );
+    Vec_PtrForEachEntry( vStart, pObj, i )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+        {
+            if ( !Nwk_ObjIsNode(pNext) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pNext );
+            Vec_PtrPush( vNext, pNext );
+        }
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+        {
+            if ( !Nwk_ObjIsNode(pNext) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pNext );
+            if ( Nwk_ObjFanoutNum(pNext) > nFanMax )
+                continue;
+            Vec_PtrPush( vNext, pNext );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes removes from the given one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCollectNonOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Vec_Ptr_t * vTemp;
+    Nwk_Obj_t * pObj;
+    int i, k;
+    Vec_PtrClear( vCands );
+    if ( pPars->nMaxSuppSize - Nwk_ObjFaninNum(pLut) <= 1 )
+        return;
+
+    // collect nodes removed by this distance
+    assert( pPars->nMaxDistance > 0 );
+    Vec_PtrClear( vStart );
+    Vec_PtrPush( vStart, pLut );
+    Nwk_ManIncrementTravId( pLut->pMan );
+    Nwk_ObjSetTravIdCurrent( pLut );
+    for ( i = 1; i <= pPars->nMaxDistance; i++ )
+    {
+        Nwk_ManCollectCircle( vStart, vNext, pPars->nMaxFanout );
+        vTemp  = vStart;
+        vStart = vNext;
+        vNext  = vTemp;
+        // collect the nodes in vStart
+        Vec_PtrForEachEntry( vStart, pObj, k )
+            Vec_PtrPush( vCands, pObj );
+    }
+
+    // mark the TFI/TFO nodes
+    Nwk_ManIncrementTravId( pLut->pMan );
+    if ( pPars->fUseTfiTfo )
+        Nwk_ObjSetTravIdCurrent( pLut );
+    else
+    {
+        Nwk_ObjSetTravIdPrevious( pLut );
+        Nwk_ManMarkFanins_rec( pLut, Nwk_ObjLevel(pLut) - pPars->nMaxDistance );
+        Nwk_ObjSetTravIdPrevious( pLut );
+        Nwk_ManMarkFanouts_rec( pLut, Nwk_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout );
+    }
+
+    // collect nodes satisfying the following conditions:
+    // - they are close enough in terms of distance
+    // - they are not in the TFI/TFO of the LUT
+    // - they have no more than the given number of fanins
+    // - they have no more than the given diff in delay
+    k = 0;
+    Vec_PtrForEachEntry( vCands, pObj, i )
+    {
+        if ( Nwk_ObjIsTravIdCurrent(pObj) )
+            continue;
+        if ( Nwk_ObjFaninNum(pLut) + Nwk_ObjFaninNum(pObj) > pPars->nMaxSuppSize )
+            continue;
+        if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+             Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+             continue;
+        Vec_PtrWriteEntry( vCands, k++, pObj );
+    }
+    Vec_PtrShrink( vCands, k );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count the total number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand )
+{
+    Nwk_Obj_t * pFanin;
+    int i, nCounter = Nwk_ObjFaninNum(pLut);
+    Nwk_ObjForEachFanin( pCand, pFanin, i )
+        nCounter += !pFanin->MarkC;
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects overlapping candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwl_ManCollectOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Nwk_Obj_t * pFanin, * pObj;
+    int i, k;
+    // mark fanins of pLut
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->MarkC = 1;
+    // collect the matching fanouts of each fanin of the node
+    Vec_PtrClear( vCands );
+    Nwk_ManIncrementTravId( pLut->pMan );
+    Nwk_ObjSetTravIdCurrent( pLut );
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+    {
+        if ( !Nwk_ObjIsNode(pFanin) )
+            continue;
+        if ( Nwk_ObjFanoutNum(pFanin) > pPars->nMaxFanout )
+            continue;
+        Nwk_ObjForEachFanout( pFanin, pObj, k )
+        {
+            if ( !Nwk_ObjIsNode(pObj) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pObj );
+            // check the difference in delay
+            if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+                 Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+                 continue;
+            // check the total number of fanins of the node
+            if ( Nwk_ManCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize )
+                continue;
+            Vec_PtrPush( vCands, pObj );
+        }
+    }
+    // unmark fanins of pLut
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->MarkC = 0;
+}
 
 /**Function*************************************************************
 
@@ -714,32 +929,35 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars )
     Vec_Int_t * vResult;
     Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
     Nwk_Obj_t * pLut, * pCand;
-    int i, k, nVertsPre;
+    int i, k, nVertsMax, nCands, clk = clock();
     // count the number of vertices
-    nVertsPre = 0;
+    nVertsMax = 0;
     Nwk_ManForEachNode( pNtk, pLut, i )
-        nVertsPre += (int)(Nwk_ObjFaninNum(pLut) <= pPars->nMaxLutSize);
-    p = Nwk_ManGraphAlloc( Nwk_ManObjNumMax(pNtk), nVertsPre );
+        nVertsMax += (int)(Nwk_ObjFaninNum(pLut) <= pPars->nMaxLutSize);
+    p = Nwk_ManGraphAlloc( nVertsMax );
     // create graph
     vStart  = Vec_PtrAlloc( 1000 );
     vNext   = Vec_PtrAlloc( 1000 );
     vCands1 = Vec_PtrAlloc( 1000 );
     vCands2 = Vec_PtrAlloc( 1000 );
+    nCands  = 0;
     Nwk_ManForEachNode( pNtk, pLut, i )
     {
         if ( Nwk_ObjFaninNum(pLut) > pPars->nMaxLutSize )
             continue;
         Nwl_ManCollectOverlapCands( pLut, vCands1, pPars );
-        Nwk_ManCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars );
+        if ( pPars->fUseDiffSupp )
+            Nwk_ManCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars );
         if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 )
             continue;
+        nCands += Vec_PtrSize(vCands1) + Vec_PtrSize(vCands2);
         // save candidates
-        Nwk_ManGraphSetMapping( p, Nwk_ObjId(pLut) );
         Vec_PtrForEachEntry( vCands1, pCand, k )
             Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) );
         Vec_PtrForEachEntry( vCands2, pCand, k )
             Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) );
         // print statistics about this node
+        if ( pPars->fVeryVerbose )
         printf( "Node %6d : Fanins = %d. Fanouts = %3d.  Cand1 = %3d. Cand2 = %3d.\n",
             Nwk_ObjId(pLut), Nwk_ObjFaninNum(pLut), Nwk_ObjFaninNum(pLut), 
             Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) );
@@ -748,9 +966,21 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars )
     Vec_PtrFree( vNext );
     Vec_PtrFree( vCands1 );
     Vec_PtrFree( vCands2 );
+    if ( pPars->fVerbose )
+    {
+        printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
+        PRT( "Deriving graph", clock() - clk );
+    }
     // solve the graph problem
-    Nwk_ManGraphPrepare( p );
+    clk = clock();
     Nwk_ManGraphSolve( p );
+    if ( pPars->fVerbose )
+    {
+        printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
+            p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+        PRT( "Solving", clock() - clk );
+        Nwk_ManGraphReportMemoryUsage( p );
+    }
     vResult = p->vPairs; p->vPairs = NULL;
     Nwk_ManGraphFree( p );
     return vResult;
diff --git a/src/aig/nwk/nwkMerge.h b/src/aig/nwk/nwkMerge.h
new file mode 100644
index 00000000..3763e4b2
--- /dev/null
+++ b/src/aig/nwk/nwkMerge.h
@@ -0,0 +1,149 @@
+/**CFile****************************************************************
+
+  FileName    [nwkMerge.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkMerge.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NWK_MERGE_H__
+#define __NWK_MERGE_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define NWK_MAX_LIST  16
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the LUT merging parameters
+typedef struct Nwk_LMPars_t_  Nwk_LMPars_t;
+struct Nwk_LMPars_t_
+{
+    int    nMaxLutSize;    // the max LUT size for merging (N=5)
+    int    nMaxSuppSize;   // the max total support size after merging (S=5)
+    int    nMaxDistance;   // the max number of nodes separating LUTs
+    int    nMaxLevelDiff;  // the max difference in levels
+    int    nMaxFanout;     // the max number of fanouts to traverse
+    int    fUseDiffSupp;   // enables the use of nodes with different support
+    int    fUseTfiTfo;     // enables the use of TFO/TFO nodes as candidates
+    int    fVeryVerbose;   // enables additional verbose output
+    int    fVerbose;       // enables verbose output
+};
+
+// edge of the graph
+typedef struct Nwk_Edg_t_  Nwk_Edg_t;
+struct Nwk_Edg_t_
+{
+    int             iNode1;      // the first node
+    int             iNode2;      // the second node
+    Nwk_Edg_t *     pNext;       // the next edge
+};
+
+// vertex of the graph
+typedef struct Nwk_Vrt_t_  Nwk_Vrt_t;
+struct Nwk_Vrt_t_
+{
+    int             Id;          // the vertex number
+    int             iPrev;       // the previous vertex in the list
+    int             iNext;       // the next vertex in the list
+    int             nEdges;      // the number of edges
+    int             pEdges[0];   // the array of edges
+};
+
+// the connectivity graph
+typedef struct Nwk_Grf_t_  Nwk_Grf_t;
+struct Nwk_Grf_t_
+{
+    // preliminary graph representation
+    int             nObjs;       // the number of objects
+    int             nVertsMax;   // the upper bound on the number of vertices
+    int             nEdgeHash;   // an approximate number of edges
+    Nwk_Edg_t **    pEdgeHash;   // hash table for edges
+    Aig_MmFixed_t * pMemEdges;   // memory for edges
+    // graph representation
+    int             nEdges;      // the number of edges
+    int             nVerts;      // the number of vertices
+    Nwk_Vrt_t **    pVerts;      // the array of vertices
+    Aig_MmFlex_t *  pMemVerts;   // memory for vertices
+    // intermediate data
+    int pLists1[NWK_MAX_LIST+1]; // lists of nodes with one edge
+    int pLists2[NWK_MAX_LIST+1]; // lists of nodes with more than one edge
+    // the results of matching
+    Vec_Int_t *     vPairs;      // pairs matched in the graph
+    // object mappings
+    int *           pMapLut2Id;  // LUT numbers into vertex IDs
+    int *           pMapId2Lut;  // vertex IDs into LUT numbers
+    // other things
+    int             nMemBytes1;  // memory usage in bytes
+    int             nMemBytes2;  // memory usage in bytes
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Nwk_GraphForEachEdge( p, pEdge, k )             \
+    for ( k = 0; k < p->nEdgeHash; k++ )                \
+        for ( pEdge = p->pEdgeHash[k]; pEdge; pEdge = pEdge->pNext )
+
+#define Nwk_ListForEachVertex( p, List, pVrt )          \
+    for ( pVrt = List? p->pVerts[List] : NULL;  pVrt;   \
+          pVrt = pVrt->iNext? p->pVerts[pVrt->iNext] : NULL )
+
+#define Nwk_VertexForEachAdjacent( p, pVrt, pNext, k )  \
+    for ( k = 0; (k < pVrt->nEdges) && (((pNext) = p->pVerts[pVrt->pEdges[k]]), 1); k++ )
+
+////////////////////////////////////////////////////////////////////////
+///                      INLINED FUNCTIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         ITERATORS                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== nwkMerge.c ==========================================================*/
+extern ABC_DLL Nwk_Grf_t *   Nwk_ManGraphAlloc( int nVertsMax );
+extern ABC_DLL void          Nwk_ManGraphFree( Nwk_Grf_t * p );
+extern ABC_DLL void          Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p );
+extern ABC_DLL void          Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 );
+extern ABC_DLL void          Nwk_ManGraphSolve( Nwk_Grf_t * p );
+extern ABC_DLL int           Nwk_ManLutMergeGraphTest( char * pFileName );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4fed39ab..aa8d6b30 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -33,6 +33,7 @@
 #include "mfx.h"
 #include "fra.h"
 #include "saig.h"
+#include "nwkMerge.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -7578,13 +7579,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    Abc_Ntk_t * pNtkRes;
+//    Abc_Ntk_t * pNtkRes;
     int c;
     int fBmc;
     int nFrames;
     int nLevels;
     int fVerbose;
     int fVeryVerbose;
+    char * pFileName;
+
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@@ -7605,13 +7608,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
 
 
-
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-    printf( "This command is temporarily disabled.\n" );
-    return 0;
+//    printf( "This command is temporarily disabled.\n" );
+//    return 0;
 
     // set defaults
     fVeryVerbose = 0;
@@ -7789,6 +7791,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_NtkDarPartition( pNtk );
 //Abc_NtkDarTest( pNtk );
 
+/*
 //    pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
     pNtkRes = Abc_NtkDarHaigRecord( pNtk, 3, 3000, 0, 0, 0, 0 );
     if ( pNtkRes == NULL )
@@ -7798,12 +7801,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    pFileName = argv[globalUtilOptind];
+    Nwk_ManLutMergeGraphTest( pFileName );
     return 0;
 usage:
-    fprintf( pErr, "usage: test [-bvwh]\n" );
+    fprintf( pErr, "usage: test [-h] <file_name>\n" );
     fprintf( pErr, "\t         testbench for new procedures\n" );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
+//    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+//    fprintf( pErr, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -17321,21 +17329,6 @@ usage:
 }
 
 
-//#include "nwk.h"
-
-// the LUT merging parameters
-typedef struct Nwk_LMPars_t_  Nwk_LMPars_t;
-struct Nwk_LMPars_t_
-{
-    int  nMaxLutSize;       // the max LUT size for merging (N=5)
-    int  nMaxSuppSize;      // the max total support size after merging (S=5)
-    int  nMaxDistance;      // the max number of nodes separating LUTs
-    int  nMaxLevelDiff;     // the max difference in levels
-    int  nMaxFanout;        // the max number of fanouts to traverse
-    int  fUseTfiTfo;        // enables the use of TFO/TFO nodes as candidates
-    int  fVeryVerbose;      // enables additional verbose output
-    int  fVerbose;          // enables verbose output
-};
 
 /**Function*************************************************************
 
@@ -17353,11 +17346,6 @@ int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv )
     Nwk_LMPars_t Pars, * pPars = &Pars;
     Vec_Int_t * vResult;
     int c;
-    int fUseLutLib = 0;
-    int Percentage = 100;
-    int Degree = 5;
-    int fVerbose = 0;
-    int fVeryVerbose = 0;
     extern Vec_Int_t * Nwk_ManLutMerge( void * pNtk, Nwk_LMPars_t * pPars );
 
     // set defaults
@@ -17367,11 +17355,12 @@ int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nMaxDistance   = 3;   // the max number of nodes separating LUTs
     pPars->nMaxLevelDiff  = 2;   // the max difference in levels
     pPars->nMaxFanout     = 100; // the max number of fanouts to traverse
+    pPars->fUseDiffSupp   = 0;   // enables the use of nodes with different support
     pPars->fUseTfiTfo     = 0;   // enables the use of TFO/TFO nodes as candidates
     pPars->fVeryVerbose   = 0;   // enables additional verbose output
     pPars->fVerbose       = 1;   // enables verbose output
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFcvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFscvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17430,6 +17419,9 @@ int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nMaxFanout < 2 ) 
                 goto usage;
             break;
+        case 's':
+            pPars->fUseDiffSupp ^= 1;
+            break;
         case 'c':
             pPars->fUseTfiTfo ^= 1;
             break;
@@ -17456,13 +17448,14 @@ int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *merge [-NSDLF num] [-cwvh]\n" );
+    fprintf( stdout, "usage: *merge [-NSDLF num] [-scwvh]\n" );
     fprintf( stdout, "\t           creates pairs of topologically-related LUTs\n" );
     fprintf( stdout, "\t-N <num> : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize );
     fprintf( stdout, "\t-S <num> : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize );
     fprintf( stdout, "\t-D <num> : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance );
     fprintf( stdout, "\t-L <num> : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff );
     fprintf( stdout, "\t-F <num> : the max number of fanouts to stop traversal (0 < num) [default = %d]\n", pPars->nMaxFanout );
+    fprintf( stdout, "\t-s       : toggle the use of nodes without support overlap [default = %s]\n", pPars->fUseDiffSupp? "yes" : "no" );
     fprintf( stdout, "\t-c       : toggle the use of TFI/TFO nodes as candidates [default = %s]\n", pPars->fUseTfiTfo? "yes" : "no" );
     fprintf( stdout, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( stdout, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );