Version abc70706

32 files changed, 918 insertions, 592 deletions

diff --git a/abc.dsp b/abc.dsp
index e1ea15fb..c2fa926c 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1902,10 +1902,6 @@ SOURCE=.\src\opt\res\resStrash.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\opt\res\resUpdate.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\opt\res\resWin.c
 # End Source File
 # End Group
diff --git a/abc.rc b/abc.rc
index b9cb6ff4..57879554 100644
--- a/abc.rc
+++ b/abc.rc
@@ -143,14 +143,6 @@ alias qsA      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
 alias chnew    "st; haig_start; resyn2; haig_use"
 alias chnewrs  "st; haig_start; resyn2rs; haig_use"
 
-alias t0       "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
-alias t1       "read_dsd a*(b+(c*d)); clp -r; print_dsd"
-alias t2       "read_dsd 56BA(a,b,c,d); clp -r; print_dsd"
-alias t3       "read_dsd 56BA(a,b*c,e,d); clp -r; print_dsd"
-alias t4       "read_dsd 56BA(a,b*c,e+d,f); clp -r; print_dsd"
-alias t5       "read_dsd 56BA(a,CA(b,c,d),e,f); clp -r; print_dsd"
-alias t6       "read_dsd f*CA(b,c,d)*CA(e,a,g); clp -r; print_dsd"
-
 alias stdsd    "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
 alias trec     "rec_start; r c.blif; st; rec_add; rec_use"
 alias trec4    "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
@@ -166,12 +158,10 @@ alias tst4     "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4
 alias tst4n    "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec"
 alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"
 
-
-alias bug      "r pj1_if3.blif; lp"
-alias table    "r lutexp.baf; test"
-
 #alias t        "r c.blif; st; wc c.cnf"
 #alias t        "r test/dsdmap6.blif; lutpack -vw; cec"
 alias t        "r i10_if4.blif; lp"
+alias t1        "r pj1_if4.blif; lp"
+alias t2        "r pj1_if6.blif; lp"
 
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 30557259..faa2fe2e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -354,6 +354,7 @@ static inline Hop_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj )           { return pO
 static inline Abc_Obj_t * Abc_ObjCopyCond( Abc_Obj_t * pObj )        { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL;  }
 
 // setting data members of the network
+static inline void        Abc_ObjSetLevel( Abc_Obj_t * pObj, int Level )         { pObj->Level =  Level;    } 
 static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )  { pObj->pCopy =  pCopy;    } 
 static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData =  pData;    } 
 
@@ -852,11 +853,16 @@ extern void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
 extern float *            Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
 extern Abc_Time_t *       Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
 extern float              Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk );
+extern int                Abc_ObjLevelNew( Abc_Obj_t * pObj );
+extern int                Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
+extern int                Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
+extern int                Abc_ObjReverseLevel( Abc_Obj_t * pObj );
+extern void               Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
+extern void               Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
 extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
-extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
-extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
-extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
+extern void               Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern void               Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern void               Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
 /*=== abcUtil.c ==========================================================*/
 extern void *             Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f34a3e85..f2017549 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -923,7 +923,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
             {
                 assert( pFanout->fMarkB == 0 );
                 pFanout->fMarkB = 1;
-                Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
+                Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanout), pFanout );
             }
         }
 
@@ -1094,7 +1094,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
             if ( pNode == NULL )
                 continue;
             assert( Abc_ObjIsNode(pNode) );
-            assert( Abc_NodeReadReverseLevel(pNode) == i );
+            assert( Abc_ObjReverseLevel(pNode) == i );
             // clean the mark
             assert( pNode->fMarkB == 1 );
             pNode->fMarkB = 0;
@@ -1106,17 +1106,17 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
                 // get the new reverse level of this fanin
                 LevelNew = 0;
                 Abc_ObjForEachFanout( pFanin, pFanout, j )
-                    if ( LevelNew < Abc_NodeReadReverseLevel(pFanout) )
-                        LevelNew = Abc_NodeReadReverseLevel(pFanout);
+                    if ( LevelNew < Abc_ObjReverseLevel(pFanout) )
+                        LevelNew = Abc_ObjReverseLevel(pFanout);
                 LevelNew += 1;
                 assert( LevelNew > i );
-                if ( Abc_NodeReadReverseLevel(pFanin) == LevelNew ) // no change
+                if ( Abc_ObjReverseLevel(pFanin) == LevelNew ) // no change
                     continue;
                 // if the fanin is present in the data structure, pull it out
                 if ( pFanin->fMarkB )
                     Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin );
                 // update the reverse level
-                Abc_NodeSetReverseLevel( pFanin, LevelNew );
+                Abc_ObjSetReverseLevel( pFanin, LevelNew );
                 // add the fanin to the data structure to update its fanins
                 assert( pFanin->fMarkB == 0 );
                 pFanin->fMarkB = 1;
@@ -1173,7 +1173,7 @@ void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
     Abc_Obj_t * pTemp;
     int m;
     assert( pNode->fMarkB );
-    vVecTemp = Vec_VecEntry( vStruct, Abc_NodeReadReverseLevel(pNode) );
+    vVecTemp = Vec_VecEntry( vStruct, Abc_ObjReverseLevel(pNode) );
     Vec_PtrForEachEntry( vVecTemp, pTemp, m )
     {
         if ( pTemp != pNode )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 6167979c..7a995c71 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -447,7 +447,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
     if ( Num >= 0 )
         return Abc_NtkObj( pNtk, Num );
     // find the internal node
-    if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
+    if ( pName[0] != 'n' )
     {
         printf( "Name \"%s\" is not found among CO or node names (internal names often look as \"n<num>\").\n", pName );
         return NULL;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 53566b7d..cd67205c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2805,7 +2805,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     pPars->nWindow      = 62;
-    pPars->nGrowthLevel =  3;
+    pPars->nGrowthLevel =  1;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
     pPars->fArea        =  0;
@@ -2936,13 +2936,14 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
     pPars->nLutsOver    =  3; // (Q) the maximum number of LUTs not in the MFFC
     pPars->nVarsShared  =  0; // (S) the maximum number of shared variables (crossbars)
-    pPars->nGrowthLevel =  9; // (L) the maximum number of increased levels
+    pPars->nGrowthLevel =  1; // (L) the maximum number of increased levels
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
-    pPars->fVerbose     =  1;
+    pPars->fFirst       =  0;
+    pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2996,6 +2997,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fZeroCost ^= 1;
             break;
+        case 'f':
+            pPars->fFirst ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -3029,7 +3033,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szvwh]\n" );
+    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfvwh]\n" );
     fprintf( pErr, "\t           performs \"rewriting\" for LUT networks\n" );
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
@@ -3037,6 +3041,7 @@ usage:
     fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-s       : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
     fprintf( pErr, "\t-z       : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
+    fprintf( pErr, "\t-f       : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index f55dc435..f9b3384e 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective,
     // compute the required times
     if ( fSelective )
     {
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
         Abc_NtkMarkCriticalNodes( pNtk );
     }
     // perform balancing
@@ -600,7 +600,7 @@ void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     int i, Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 )
+        if ( Abc_ObjRequiredLevel(pNode) - pNode->Level <= 1 )
             pNode->fMarkA = 1, Counter++;
     printf( "The number of nodes on the critical paths = %6d  (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) );
 }
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 074b8ae8..a9c42ceb 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -263,10 +263,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
     }
     // set the level of the new node
-    {
-        extern int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
-        pNodeNew->Level = Res_UpdateNetworkLevelNew( pNodeNew );
-    }
+    pNodeNew->Level = Abc_ObjLevelNew( pNodeNew );
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 872ffaf0..210c0534 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -100,7 +100,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -187,7 +187,7 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     char * pSop;
     int Required;
 
-    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     p->nNodesConsidered++;
 
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index b9ffd932..326d1543 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -114,7 +114,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool f
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     // start the restructuring manager
     pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose );
@@ -324,7 +324,7 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
     p->nCutsConsidered++;
 
     // get the required time for the node
-    Required = p->fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY;
+    Required = p->fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
 
     // collect the leaves of the cut
     Vec_PtrClear( p->vLeaves );
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 243548fa..a954f2ce 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -159,7 +159,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     if ( Abc_NtkLatchNum(pNtk) )
         Abc_NtkForEachLatch(pNtk, pNode, i)
@@ -1617,7 +1617,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
     int Required;
     int clk;
 
-    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
 
     assert( nSteps >= 0 );
     assert( nSteps <= 3 );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 3d06dddf..7760b2d1 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -83,7 +83,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
         return 0;
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
     // start the cut manager
 clk = clock();
     pManCut = Abc_NtkStartCutManForRewrite( pNtk );
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 93fa3fa5..fd54f519 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -630,39 +630,133 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the AIG for the comptuation of required levels.]
+  Synopsis    [Computes the level of the node using its fanin levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjLevelNew( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, Abc_ObjLevel(pFanin) );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reverse level of the node using its fanout levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, LevelCur, Level = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        LevelCur = Abc_ObjReverseLevel( pFanout );
+        Level = ABC_MAX( Level, LevelCur );
+    }
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns required level of the node.]
+
+  Description [Converts the reverse levels of the node into its required 
+  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjRequiredLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    return pNtk->LevelMax + 1 - Abc_ObjReverseLevel(pObj);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjReverseLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares for the computation of required levels.]
 
   Description [This procedure should be called before the required times
   are used. It starts internal data structures, which records the level 
-  from the COs of the AIG nodes in reverse topologogical order.]
+  from the COs of the network nodes in reverse topologogical order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
+void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pFanout;
-    int i, k, nLevelsCur;
-//    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_Obj_t * pObj;
+    int i;
     // remember the maximum number of direct levels
-//    pNtk->LevelMax = Abc_AigLevel(pNtk);
-    pNtk->LevelMax = Abc_NtkLevel(pNtk);
+    pNtk->LevelMax = Abc_NtkLevel(pNtk) + nMaxLevelIncrease;
     // start the reverse levels
     pNtk->vLevelsR = Vec_IntAlloc( 0 );
-    Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
+    Vec_IntFill( pNtk->vLevelsR, 1 + Abc_NtkObjNumMax(pNtk), 0 );
     // compute levels in reverse topological order
     vNodes = Abc_NtkDfsReverse( pNtk );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        nLevelsCur = 0;
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-            if ( nLevelsCur < Vec_IntEntry(pNtk->vLevelsR, pFanout->Id) )
-                nLevelsCur = Vec_IntEntry(pNtk->vLevelsR, pFanout->Id);
-        Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, nLevelsCur + 1 );
-    }
+        Abc_ObjSetReverseLevel( pObj, Abc_ObjReverseLevelNew(pObj) );
     Vec_PtrFree( vNodes );
 }
 
@@ -688,64 +782,116 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets the reverse level of the node.]
+  Synopsis    [Incrementally updates level of the nodes.]
 
-  Description [The reverse level is the level of the node in reverse
-  topological order, starting from the COs.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
+void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
-    Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
+    Abc_Obj_t * pFanout, * pTemp;
+    int LevelOld, Lev, k, m;
+    // check if level has changed
+    LevelOld = Abc_ObjLevel(pObjNew);
+    if ( LevelOld == Abc_ObjLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( vLevels );
+    Vec_VecPush( vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        assert( Abc_ObjLevel(pTemp) == Lev );
+        Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
+        // if the level did not change, to need to check the fanout levels
+        if ( Abc_ObjLevel(pTemp) == Lev )
+            continue;
+        // schedule fanout for level update
+        Abc_ObjForEachFanout( pTemp, pFanout, m )
+        {
+            if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
+            {
+                Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
+                pFanout->fMarkA = 1;
+            }
+        }
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the reverse level of the node.]
+  Synopsis    [Incrementally updates level of the nodes.]
 
-  Description [The reverse level is the level of the node in reverse
-  topological order, starting from the COs.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
+void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
-    return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+    Abc_Obj_t * pFanin, * pTemp;
+    int LevelOld, Lev, k, m;
+    // check if level has changed
+    LevelOld = Abc_ObjReverseLevel(pObjNew);
+    if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( vLevels );
+    Vec_VecPush( vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        LevelOld = Abc_ObjReverseLevel(pTemp); 
+        assert( LevelOld == Lev );
+        Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) );
+        // if the level did not change, to need to check the fanout levels
+        if ( Abc_ObjReverseLevel(pTemp) == Lev )
+            continue;
+        // schedule fanins for level update
+        Abc_ObjForEachFanin( pTemp, pFanin, m )
+        {
+            if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA )
+            {
+                Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin );
+                pFanin->fMarkA = 1;
+            }
+        }
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns required level of the node.]
+  Synopsis    [Replaces the node and incrementally updates levels.]
 
-  Description [Converts the reverse levels of the node into its required 
-  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj )
+void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+    // replace the old node by the new node
+    pObjNew->Level = pObj->Level;
+    Abc_ObjReplace( pObj, pObjNew );
+    // update the level of the node
+    Abc_NtkUpdateLevel( pObjNew, vLevels );
+    Abc_NtkUpdateReverseLevel( pObjNew, vLevels );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index a4c67a8b..6ab2c552 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -705,7 +705,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     nErrors = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
         nErrors += (int)( pValues1[i] != pValues2[i] );
-    printf( "Verification failed for %d outputs: ", nErrors );
+    printf( "Verification failed for at least %d outputs: ", nErrors );
     // print the first 3 outputs
     nPrinted = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
@@ -860,7 +860,7 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
         return;
     }
 
-    printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
+    printf( "Verification failed for at least %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
     // print the first 3 outputs
     nPrinted = 0;
     Abc_NtkForEachPo( pNtk1, pObj1, o )
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index 12750d16..fae9382d 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -43,7 +43,7 @@
 ***********************************************************************/
 void Cmd_HistoryAddCommand(    Abc_Frame_t * p, char * command )
 {
-    char Buffer[500];
+    static char Buffer[MAX_STR];
     strcpy( Buffer, command );
     if ( command[strlen(command)-1] != '\n' )
         strcat( Buffer, "\n" );
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 09e476f9..55ffdf4f 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -77,6 +77,9 @@ struct Vec_Vec_t_
 #define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k )                              \
     for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- )                                           \
         Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryReverseStart( vGlob, pEntry, i, k, LevelStart )                    \
+    for ( i = LevelStart; i >= 0; i-- )                                                       \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 229b0bce..e9a389e0 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -121,7 +121,7 @@ struct Kit_DsdNtk_t_
     unsigned char  Root;            // the root of the tree
     unsigned *     pMem;            // memory for the truth tables (memory manager?)
     unsigned *     pSupps;          // supports of the nodes
-    Kit_DsdObj_t * pNodes[0];       // the nodes
+    Kit_DsdObj_t** pNodes;          // the nodes
 };
 
 // DSD manager
@@ -260,7 +260,15 @@ static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
     int w;
     for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
         if ( pIn[w] )
-            return Kit_WordFindFirstBit(pIn[w]);
+            return 32*w + Kit_WordFindFirstBit(pIn[w]);
+    return -1;
+}
+static inline int Kit_TruthFindFirstZero( unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
+        if ( ~pIn[w] )
+            return 32*w + Kit_WordFindFirstBit(~pIn[w]);
     return -1;
 }
 static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
@@ -444,12 +452,18 @@ extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
 /*=== kitDsd.c ==========================================================*/
+extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars );
+extern void            Kit_DsdManFree( Kit_DsdMan_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
-extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
+extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
 extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
+extern void            Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
 extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
+extern void            Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
+extern Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
+extern void            Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdGetSupports( Kit_DsdNtk_t * p );
@@ -510,10 +524,12 @@ extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, i
 extern void            Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
+extern int             Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
 extern void            Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
 extern unsigned        Kit_TruthHash( unsigned * pIn, int nWords );
 extern unsigned        Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
+extern char *          Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
 
 #ifdef __cplusplus
 }
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 8b6b6979..06377cba 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -91,6 +91,11 @@ Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
     pObj->nFans = nFans;
     pObj->Offset = Kit_DsdObjOffset( nFans );
     // add the object
+    if ( pNtk->nNodes == pNtk->nNodesAlloc )
+    {
+        pNtk->nNodesAlloc *= 2;
+        pNtk->pNodes = REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc ); 
+    }
     assert( pNtk->nNodes < pNtk->nNodesAlloc );
     pNtk->pNodes[pNtk->nNodes++] = pObj;
     return pObj;
@@ -126,10 +131,9 @@ void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
 Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
 {
     Kit_DsdNtk_t * pNtk;
-    int nSize = sizeof(Kit_DsdNtk_t) + sizeof(void *) * nVars;
-    // allocate the network
-    pNtk = (Kit_DsdNtk_t *)ALLOC( char, nSize );
-    memset( pNtk, 0, nSize );
+    pNtk = ALLOC( Kit_DsdNtk_t, 1 );
+    memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
+    pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars );
     pNtk->nVars = nVars;
     pNtk->nNodesAlloc = nVars;
     pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
@@ -154,6 +158,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
     Kit_DsdNtkForEachObj( pNtk, pObj, i )
         free( pObj );
     FREE( pNtk->pSupps );
+    free( pNtk->pNodes );
     free( pNtk->pMem );
     free( pNtk );
 }
@@ -275,7 +280,27 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
 {
     Kit_DsdNtk_t * pTemp;
     pTemp = Kit_DsdExpand( pNtk );
-    Kit_DsdPrint( stdout, pNtk );
+    Kit_DsdPrint( stdout, pTemp );
+    Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pTemp;
+    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
+    Kit_DsdVerify( pTemp, pTruth, nVars ); 
+    Kit_DsdPrintExpanded( pTemp );
     Kit_DsdNtkFree( pTemp );
 }
 
@@ -290,11 +315,11 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
+unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
 {
     Kit_DsdObj_t * pObj;
     unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
-    unsigned i, m, iLit, nMints, fCompl;
+    unsigned i, m, iLit, nMints, fCompl, fPartial = 0;
 
     // get the node with this ID
     pObj = Kit_DsdNtkObj( pNtk, Id );
@@ -304,6 +329,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     if ( pObj == NULL )
     {
         assert( Id < pNtk->nVars );
+        assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) );
         return pTruthRes;
     }
 
@@ -320,7 +346,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     {
         assert( pObj->nFans == 1 );
         iLit = pObj->pFans[0];
-        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+        assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
+        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
         if ( Kit_DsdLitIsCompl(iLit) )
             Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
         else
@@ -329,8 +356,22 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     }
 
     // collect the truth tables of the fanins
-    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
-        pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+    if ( uSupp )
+    {
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
+                pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+            else
+            {
+                pTruthFans[i] = NULL;
+                fPartial = 1;
+            }
+    }
+    else
+    {
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+    }
     // create the truth table
 
     // simple gates
@@ -338,7 +379,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     {
         Kit_TruthFill( pTruthRes, pNtk->nVars );
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
-            Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
+            if ( pTruthFans[i] )
+                Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
         return pTruthRes;
     }
     if ( pObj->Type == KIT_DSD_XOR )
@@ -347,8 +389,11 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         fCompl = 0;
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         {
-            Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
-            fCompl ^= Kit_DsdLitIsCompl(iLit);
+            if ( pTruthFans[i] )
+            {
+                Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
+                fCompl ^= Kit_DsdLitIsCompl(iLit);
+            }
         }
         if ( fCompl )
             Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -356,6 +401,16 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     }
     assert( pObj->Type == KIT_DSD_PRIME );
 
+    if ( uSupp && fPartial )
+    {
+        // find the only non-empty component
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            if ( pTruthFans[i] )
+                break;
+        assert( i < pObj->nFans );
+        return pTruthFans[i];
+    }
+
     // get the truth table of the prime node
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
@@ -387,16 +442,19 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
+unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
 {
     unsigned * pTruthRes;
     int i;
-    // assign elementary truth ables
+    // if support is specified, request that supports are available
+    if ( uSupp )
+        Kit_DsdGetSupports( pNtk );
+    // assign elementary truth tables
     assert( pNtk->nVars <= p->nVars );
     for ( i = 0; i < (int)pNtk->nVars; i++ )
         Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
     // compute truth table for each node
-    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
+    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
     // complement the truth table if needed
     if ( Kit_DsdLitIsCompl(pNtk->Root) )
         Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -419,13 +477,30 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
     Kit_DsdMan_t * p;
     unsigned * pTruth;
     p = Kit_DsdManAlloc( pNtk->nVars );
-    pTruth = Kit_DsdTruthCompute( p, pNtk );
+    pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
     Kit_DsdManFree( p );
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
+{
+    unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
+    Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of blocks of the given number of inputs.]
 
   Description []
@@ -1085,7 +1160,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
 {
     Kit_DsdObj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);
@@ -1168,11 +1243,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
             pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
             pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
             // call recursively
-            Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 );
-            Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
+            Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
+            Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
             return;
         }
-//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
 
         // create the new node
         pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
@@ -1214,7 +1288,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
             assert( 0 );
         // decompose the remainder
         assert( Kit_DsdObjTruth(pObj) == pTruth );
-        Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 );
+        Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux );
         return;
     }
     pObj->fMark = 1;
@@ -1234,7 +1308,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
         if ( uSupp0 == 0 || uSupp1 == 0 )
         {
             pObj->fMark = 0;
-            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
             return;
         }
         assert( uSupp0 && uSupp1 );
@@ -1275,7 +1349,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
                 if ( fEquals[1][0] && fEquals[1][1] )
                     pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
                 // decompose the remainder
-                Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+                Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
                 return;
             }
         }
@@ -1339,10 +1413,36 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
                 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             // decompose the remainder
-            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
             return;
         }
     }
+/*
+    // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
+    if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
+    {
+        int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] );
+        uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+        uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+        // perform MUX decomposition
+        pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+        pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+        for ( k = 0; k < pObj->nFans; k++ )
+            pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k];
+        Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );        
+        Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans ); 
+        // update the current one
+        assert( pObj->Type == KIT_DSD_PRIME );
+        pTruth[0] = 0xCACACACA;
+        pObj->nFans = 3;
+        pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
+        pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
+        pObj->pFans[2] = pObj->pFans[iBestVar];
+        // call recursively
+        Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
+        Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
+    }
+*/
 }
 
 /**Function*************************************************************
@@ -1356,7 +1456,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
   SeeAlso     []
 
 ***********************************************************************/
-Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+Kit_DsdNtk_t * Kit_DsdDecomposeInt( unsigned * pTruth, int nVars, int nDecMux )
 {
     Kit_DsdNtk_t * pNtk;
     Kit_DsdObj_t * pObj;
@@ -1389,7 +1489,7 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
         pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
         return pNtk;
     }
-    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
+    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux );
     return pNtk;
 }
 
@@ -1404,6 +1504,38 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+{
+    return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description [Uses MUXes to break-down large prime nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
+{
+    return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
 {
     Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
@@ -1489,7 +1621,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
@@ -1509,37 +1641,15 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
   SeeAlso     []
 
 ***********************************************************************/
-Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize )
+void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
 {
-//    Kit_DsdMan_t * p;
-    Kit_DsdNtk_t * pNtk;//, * pTemp;
-//    unsigned * pTruthC;
-//    int Result;
-
-    // decompose the function
-    pNtk = Kit_DsdDecompose( pTruth, nVars );
-
-//    pNtk = Kit_DsdExpand( pTemp = pNtk );
-//    Kit_DsdNtkFree( pTemp );
-
-//    Result = Kit_DsdCountLuts( pNtk, nLutSize );
-
-//    printf( "\n" );
-//    Kit_DsdPrint( stdout, pNtk );
-//    printf( "Eval = %d.\n", Result );
-
-/*
-    // recompute the truth table
+    Kit_DsdMan_t * p;
+    unsigned * pTruthC;
     p = Kit_DsdManAlloc( nVars );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
-*/
-
-//    Kit_DsdNtkFree( pNtk );
-//    return Result;
-    return pNtk;
 }
 
 /**Function*************************************************************
@@ -1578,7 +1688,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
 //    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
 //    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
     if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
@@ -1648,7 +1758,7 @@ void Kit_DsdPrecompute4Vars()
 */
 
         p = Kit_DsdManAlloc( 4 );
-        pTruthC = Kit_DsdTruthCompute( p, pNtk );
+        pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
         if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
             printf( "Verification failed.\n" );
         Kit_DsdManFree( p );
diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c
index 1123b90e..e2deb4ef 100644
--- a/src/opt/kit/kitGraph.c
+++ b/src/opt/kit/kitGraph.c
@@ -354,9 +354,10 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
     Kit_Graph_t * pGraph;
     int RetValue;
     // derive SOP
-    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); // tried 1 and found not useful in "renode"
+    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
     if ( RetValue == -1 )
         return NULL;
+//    printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
     assert( RetValue == 0 || RetValue == 1 );
     // derive factored form
     pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index dbf222c2..d41e5d4e 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -1061,6 +1061,48 @@ int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
 
 /**Function*************************************************************
 
+  Synopsis    [Find the best cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
+{
+    int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
+    if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
+        return -1;
+    // iterate through variables
+    iBestVar = -1;
+    nSuppSizeMin = KIT_INFINITY;
+    for ( i = 0; i < nVars; i++ )
+    {
+        // cofactor the functiona and get support sizes
+        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+        nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
+        nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
+        nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
+        // compare this variable with other variables
+        if ( nSuppSizeMin > nSuppSizeCur ) 
+        {
+            nSuppSizeMin = nSuppSizeCur;
+            iBestVar = i;
+        }
+    }
+    assert( iBestVar != -1 );
+    // cofactor w.r.t. this variable
+    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+    return iBestVar;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of 1's in each cofactor.]
 
   Description [The resulting numbers are stored in the array of shorts, 
@@ -1566,6 +1608,31 @@ void Kit_TruthCountMintermsPrecomp()
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Dumps truth table into a file.]
+
+  Description [Generates script file for reading into ABC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
+{
+    static char pFileName[100];
+    FILE * pFile;
+    sprintf( pFileName, "s%03d", nFile );
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "rt " );
+    Extra_PrintHexadecimal( pFile, pTruth, nVars );
+    fprintf( pFile, "; bdd; sop; ps\n" );
+    fclose( pFile );
+    return pFileName;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index 092b43e1..f1dcd528 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -47,6 +47,7 @@ struct Lpk_Par_t_
     int               nGrowthLevel;  // (L) the maximum increase in the node level after resynthesis
     int               fSatur;        // iterate till saturation
     int               fZeroCost;     // accept zero-cost replacements
+    int               fFirst;        // use root node and first cut only
     int               fVerbose;      // the verbosiness flag
     int               fVeryVerbose;  // additional verbose info printout
     // internal parameters
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index cbd971e3..aa0368a9 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -17,7 +17,7 @@
   Revision    [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #include "lpkInt.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -30,6 +30,54 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_IfManStart( Lpk_Man_t * p )
+{
+    If_Par_t * pPars;
+    assert( p->pIfMan == NULL );
+    // set defaults
+    pPars = ALLOC( If_Par_t, 1 );
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    =  p->pPars->nLutSize;
+    pPars->nCutsMax    = 16;
+    pPars->nFlowIters  =  0; // 1
+    pPars->nAreaIters  =  0; // 1 
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  0;
+    pPars->fArea       =  1;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; //
+    pPars->fLatchPaths =  0;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->fUsePerm    =  0; 
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->fUseBdds    =  0;
+    pPars->fUseSops    =  0;
+    pPars->fUseCnfs    =  0;
+    pPars->fUseMv      =  0;
+    // start the mapping manager and set its parameters
+    p->pIfMan = If_ManStart( pPars );
+    If_ManSetupSetAll( p->pIfMan, 1000 );
+    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if at least one entry has changed.]
 
   Description []
@@ -63,6 +111,112 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+    Kit_DsdObj_t * pRoot;
+    If_Obj_t * pDriver, * ppLeaves[16];
+    Abc_Obj_t * pLeaf, * pObjNew;
+    int nGain, i, clk;
+//    int nOldShared;
+
+    // check special cases
+    pRoot = Kit_DsdNtkRoot( pNtk );
+    if ( pRoot->Type == KIT_DSD_CONST1 )
+    {
+        if ( Kit_DsdLitIsCompl(pNtk->Root) )
+            pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
+        else
+            pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+        Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    if ( pRoot->Type == KIT_DSD_VAR )
+    {
+        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+        if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
+            pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
+        Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+    // start the mapping manager
+    if ( p->pIfMan == NULL )
+        Lpk_IfManStart( p );
+
+    // prepare the mapping manager
+    If_ManRestart( p->pIfMan );
+    // create the PI variables
+    for ( i = 0; i < p->pPars->nVarsMax; i++ )
+        ppLeaves[i] = If_ManCreateCi( p->pIfMan );
+    // set the arrival times
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+    // prepare the PI cuts
+    If_ManSetupCiCutSets( p->pIfMan );
+    // create the internal nodes
+    p->fCalledOnce = 0;
+    p->nCalledSRed = 0;
+    pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
+    if ( pDriver == NULL )
+        return 0;
+    // create the PO node
+    If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
+
+    // perform mapping
+    p->pIfMan->pPars->fAreaOnly = 1;
+clk = clock();
+    If_ManPerformMappingComb( p->pIfMan );
+p->timeMap += clock() - clk;
+
+    // compute the gain in area
+    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+    if ( p->pPars->fVeryVerbose )
+        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d. SReds = %d.\n", 
+            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level, p->nCalledSRed );
+
+    // quit if there is no gain
+    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+        return 0;
+
+    // quit if depth increases too much
+    if ( (int)p->pIfMan->RequiredGlo > Abc_ObjRequiredLevel(p->pObj) )
+        return 0;
+
+    // perform replacement
+    p->nGainTotal += nGain;
+    p->nChanges++;
+    if ( p->nCalledSRed )
+        p->nBenefited++;
+
+    // prepare the mapping manager
+    If_ManCleanNodeCopy( p->pIfMan );
+    If_ManCleanCutData( p->pIfMan );
+    // set the PIs of the cut
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+    // get the area of mapping
+    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+    // perform replacement
+    Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs resynthesis for one node.]
 
   Description []
@@ -74,13 +228,13 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
 ***********************************************************************/
 int Lpk_ResynthesizeNode( Lpk_Man_t * p )
 {
+    static int Count = 0;
+    char * pFileName;
     Kit_DsdNtk_t * pDsdNtk;
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
     void * pDsd = NULL;
-    int i, RetValue, clk;
-
-    Lpk_Cut_t * pCutMax;
+    int i, nSuppSize, RetValue, clk;
 
     // compute the cuts
 clk = clock();
@@ -91,17 +245,6 @@ p->timeCuts += clock() - clk;
     }
 p->timeCuts += clock() - clk;
 
-    // find the max volume cut
-    pCutMax = NULL;
-    for ( i = 0; i < p->nEvals; i++ )
-    {
-        pCut = p->pCuts + p->pEvals[i];
-        if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
-            pCutMax = pCut;
-    }
-    assert( pCutMax != NULL );
-    
-
     if ( p->pPars->fVeryVerbose )
     printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
     // try the good cuts
@@ -111,20 +254,34 @@ p->timeCuts += clock() - clk;
     {
         // get the cut
         pCut = p->pCuts + p->pEvals[i];
+        if ( p->pPars->fFirst && i == 1 )
+            break;
 
-        if ( pCut != pCutMax )
-            continue;
+        if ( p->pObj->Id == 8835 )
+        {
+            int x = 0;
+        }
 
         // compute the truth table
 clk = clock();
         pTruth = Lpk_CutTruth( p, pCut );
+        nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
 p->timeTruth += clock() - clk;
 
-clk = clock();
-        pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
-p->timeEval += clock() - clk;
+        pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); 
+//        Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); 
+        // skip 16-input non-DSD because ISOP will not work
+        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) 
+        {
+            Kit_DsdNtkFree( pDsdNtk );
+            continue;
+        }
 
-        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+        // if DSD has nodes that require splitting to fit them into LUTs
+        // we can skip those cuts that cannot lead to improvement
+        // (a full DSD network requires  V = Nmin * (K-1) + 1 for improvement)
+        if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > p->pPars->nLutSize && 
+             nSuppSize >= ((int)pCut->nNodes - (int)pCut->nNodesDup - 1) * (p->pPars->nLutSize - 1) + 1 )
         {
             Kit_DsdNtkFree( pDsdNtk );
             continue;
@@ -133,15 +290,18 @@ p->timeEval += clock() - clk;
         if ( p->pPars->fVeryVerbose )
         {
             printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
-                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+                i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
             Kit_DsdPrint( stdout, pDsdNtk );
+//            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+            printf( "Saved truth table in file \"%s\".\n", pFileName );
         }
 
         // update the network
 clk = clock();
-        RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
+        RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
+p->timeEval += clock() - clk;
         Kit_DsdNtkFree( pDsdNtk );
-p->timeMap += clock() - clk;
         if ( RetValue )
             break;
     }
@@ -187,16 +347,28 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
             pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
     }
  
-    // convert logic to AIGs
-    Abc_NtkToAig( pNtk );
+
+    // convert into the AIG
+    if ( !Abc_NtkToAig(pNtk) )
+    {
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        return 0;
+    }
+    assert( Abc_NtkHasAig(pNtk) );
+
+    // set the number of levels
+    Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // start the manager
     p = Lpk_ManStart( pPars );
     p->pNtk = pNtk;
     p->nNodesTotal = Abc_NtkNodeNum(pNtk);
-    p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+    p->vLevels = Vec_VecStart( pNtk->LevelMax ); 
     if ( p->pPars->fSatur )
         p->vVisited = Vec_VecStart( 0 );
+    if ( pPars->fVerbose )
+        p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
 
     // iterate over the network
     nNodesPrev = p->nNodesTotal;
@@ -213,8 +385,11 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
         Abc_NtkForEachNode( pNtk, pObj, i )
         {
             // skip all except the final node
-//            if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
-//                continue;
+            if ( pPars->fFirst )
+            {
+                if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
+                    continue;
+            }
 
             if ( i >= nNodes )
                 break;
@@ -227,8 +402,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
             p->pObj = pObj;
             Lpk_ResynthesizeNode( p );
 
-            if ( p->nChanges == 3 )
-                break;
+//            if ( p->nChanges == 3 )
+//                break;
         }
         if ( !pPars->fVeryVerbose )
             Extra_ProgressBarStop( pProgress );
@@ -241,19 +416,30 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
         if ( !p->pPars->fSatur )
             break;
 
-        break;
+        if ( pPars->fFirst )
+            break;
     }
+    Abc_NtkStopReverseLevels( pNtk );
 
     if ( pPars->fVerbose )
     {
-        printf( "N = %5d (%3d)  Cut = %5d (%4d)  Change = %5d  Gain = %5d  (%5.2f %%) Iter = %2d\n", 
-            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
-        printf( "Non_DSD blocks: " );
+        p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+        printf( "\n" );
+
+        printf( "Nodes = %5d (%3d)  Cuts = %5d (%4d)  Changes = %5d  Iter = %2d  Benefit = %d.\n", 
+            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
+        printf( "Non-DSD:" );
         for ( i = 3; i <= pPars->nVarsMax; i++ )
             if ( p->nBlocks[i] )
-                printf( "%d=%d  ", i, p->nBlocks[i] );
+                printf( " %d=%d", i, p->nBlocks[i] );
         printf( "\n" );
+
         p->timeTotal = clock() - clk;
+        p->timeEval  = p->timeEval  - p->timeMap;
         p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
         PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
         PRTP( "Truth ", p->timeTruth, p->timeTotal );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 251ec829..12dae15b 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -545,11 +545,11 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         pCut = p->pCuts + i;
         if ( pCut->nLeaves < 2 )
             continue;
-        // compute the number of LUTs neede to implement this cut
+        // compute the minimum number of LUTs needed to implement this cut
         // V = N * (K-1) + 1  ~~~~~  N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
         pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); 
         pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
-        if ( pCut->Weight <= 1.0 )
+        if ( pCut->Weight <= 1.001 )
             continue;
         pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
         if ( pCut->fHasDsd )
@@ -566,7 +566,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         {
             pCut = p->pCuts + p->pEvals[i];
             pCut2 = p->pCuts + p->pEvals[i+1];
-            if ( pCut->Weight >= pCut2->Weight )
+            if ( pCut->Weight >= pCut2->Weight - 0.001 )
                 continue;
             Temp = p->pEvals[i];
             p->pEvals[i] = p->pEvals[i+1];
@@ -574,6 +574,14 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
             fChanges = 1;
         }
     } while ( fChanges );
+/*
+    for ( i = 0; i < p->nEvals; i++ )
+    {
+        pCut = p->pCuts + p->pEvals[i];
+        printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
+    }
+    printf( "\n" );
+*/
     return 1;
 }
 
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index fe442302..683e7b92 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -87,6 +87,7 @@ struct Lpk_Man_t_
     // temporary variables
     int          fCofactoring;          // working in the cofactoring mode
     int          fCalledOnce;           // limits the depth of MUX cofactoring
+    int          nCalledSRed;           // the number of called to SRed
     int          pRefs[LPK_SIZE_MAX];   // fanin reference counters 
     int          pCands[LPK_SIZE_MAX];  // internal nodes pointing only to the leaves
     // truth table representation
@@ -94,6 +95,7 @@ struct Lpk_Man_t_
     Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
     // variable sets
     Vec_Int_t *  vSets[8];
+    Kit_DsdMan_t * pDsdMan;
     // statistics
     int          nNodesTotal;           // total number of nodes
     int          nNodesOver;            // nodes with cuts over the limit 
@@ -101,6 +103,9 @@ struct Lpk_Man_t_
     int          nCutsUseful;           // useful cuts 
     int          nGainTotal;            // the gain in LUTs
     int          nChanges;              // the number of changed nodes
+    int          nBenefited;            // the number of gainful that benefited from decomposition
+    int          nTotalNets;
+    int          nTotalNets2;
     // counter of non-DSD blocks
     int          nBlocks[17];
     // rutime
@@ -138,7 +143,6 @@ extern int            Lpk_NodeCuts( Lpk_Man_t * p );
 extern Lpk_Man_t *    Lpk_ManStart( Lpk_Par_t * pPars );
 extern void           Lpk_ManStop( Lpk_Man_t * p );
 /*=== lpkMap.c =========================================================*/
-extern int            Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
 extern If_Obj_t *     Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
 extern If_Obj_t *     Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
 /*=== lpkMulti.c =======================================================*/
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index da8b0e3a..5dd54450 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -54,6 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->vCover = Vec_IntAlloc( 1 << 12 );
     for ( i = 0; i < 8; i++ )
         p->vSets[i] = Vec_IntAlloc(100);
+    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
     return p;
 }
 
@@ -71,6 +72,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
 void Lpk_ManStop( Lpk_Man_t * p )
 {
     int i;
+    Kit_DsdManFree( p->pDsdMan );
     for ( i = 0; i < 8; i++ )
         Vec_IntFree(p->vSets[i]);
     if ( p->pIfMan )
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
index c647fdf7..698aeea1 100644
--- a/src/opt/lpk/lpkMap.c
+++ b/src/opt/lpk/lpkMap.c
@@ -24,62 +24,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_IfManStart( Lpk_Man_t * p )
-{
-    If_Par_t * pPars;
-    assert( p->pIfMan == NULL );
-    // set defaults
-    pPars = ALLOC( If_Par_t, 1 );
-    memset( pPars, 0, sizeof(If_Par_t) );
-    // user-controlable paramters
-    pPars->nLutSize    =  p->pPars->nLutSize;
-    pPars->nCutsMax    = 16;
-    pPars->nFlowIters  =  0; // 1
-    pPars->nAreaIters  =  0; // 1 
-    pPars->DelayTarget = -1;
-    pPars->fPreprocess =  0;
-    pPars->fArea       =  1;
-    pPars->fFancy      =  0;
-    pPars->fExpRed     =  0; //
-    pPars->fLatchPaths =  0;
-    pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
-    // internal parameters
-    pPars->fTruth      =  0;
-    pPars->fUsePerm    =  0; 
-    pPars->nLatches    =  0;
-    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
-    pPars->pTimesArr   =  NULL; 
-    pPars->pTimesArr   =  NULL;   
-    pPars->fUseBdds    =  0;
-    pPars->fUseSops    =  0;
-    pPars->fUseCnfs    =  0;
-    pPars->fUseMv      =  0;
-    // start the mapping manager and set its parameters
-    p->pIfMan = If_ManStart( pPars );
-    If_ManSetupSetAll( p->pIfMan, 1000 );
-    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Transforms the decomposition graph into the AIG.]
 
   Description []
@@ -154,122 +104,10 @@ If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
-{
-    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
-    Kit_DsdObj_t * pRoot;
-    If_Obj_t * pDriver, * ppLeaves[16];
-    Abc_Obj_t * pLeaf, * pObjNew;
-    int nGain, i;
-//    int nOldShared;
-
-    // check special cases
-    pRoot = Kit_DsdNtkRoot( pNtk );
-    if ( pRoot->Type == KIT_DSD_CONST1 )
-    {
-        if ( Kit_DsdLitIsCompl(pNtk->Root) )
-            pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
-        else
-            pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
-
-        // perform replacement
-        pObjNew->Level = p->pObj->Level;
-        Abc_ObjReplace( p->pObj, pObjNew );
-        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    if ( pRoot->Type == KIT_DSD_VAR )
-    {
-        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
-        if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
-            pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
-
-        // perform replacement
-        pObjNew->Level = p->pObj->Level;
-        Abc_ObjReplace( p->pObj, pObjNew );
-        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
-
-    // start the mapping manager
-    if ( p->pIfMan == NULL )
-        Lpk_IfManStart( p );
-
-    // prepare the mapping manager
-    If_ManRestart( p->pIfMan );
-    // create the PI variables
-    for ( i = 0; i < p->pPars->nVarsMax; i++ )
-        ppLeaves[i] = If_ManCreateCi( p->pIfMan );
-    // set the arrival times
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
-    // prepare the PI cuts
-    If_ManSetupCiCutSets( p->pIfMan );
-    // create the internal nodes
-    p->fCalledOnce = 0;
-    pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
-    if ( pDriver == NULL )
-        return 0;
-    // create the PO node
-    If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
-
-    // perform mapping
-    p->pIfMan->pPars->fAreaOnly = 1;
-    If_ManPerformMappingComb( p->pIfMan );
-
-    // compute the gain in area
-    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
-    if ( p->pPars->fVeryVerbose )
-        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", 
-            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
-
-    // quit if there is no gain
-    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
-        return 0;
-
-    // quit if depth increases too much
-    if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
-        return 0;
-
-    // perform replacement
-    p->nGainTotal += nGain;
-    p->nChanges++;
-
-    // prepare the mapping manager
-    If_ManCleanNodeCopy( p->pIfMan );
-    If_ManCleanCutData( p->pIfMan );
-    // set the PIs of the cut
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
-    // get the area of mapping
-    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
-    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
-
-    // perform replacement
-    pObjNew->Level = p->pObj->Level;
-    Abc_ObjReplace( p->pObj, pObjNew );
-    Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
 {
     Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjNew, * pFansNew[16];
+    If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
     unsigned i, iLitFanin;
 
     assert( iLit >= 0 );
@@ -325,20 +163,38 @@ If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLe
         if ( pFansNew[i] == NULL )
             return NULL;
     }
-/*
+/* 
     if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
     {
         pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
         return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
     }
 */
+/*
+    if ( (int)pObj->nFans > p->pPars->nLutSize )
+    {
+        pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+//        if ( pObjNew2 )
+//            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+    }
+*/
 
     // find best cofactoring variable
-    if ( pObj->nFans > 3 && !p->fCalledOnce )
-//        pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-        pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-    else
-        pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+    if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+    {
+        pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+        if ( pObjNew2 )
+            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+    }
+
+    pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+
+    // add choice
+    if ( pObjNew && pObjNew2 )
+    {
+        If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
+        If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
+    }
     return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
 }
 
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
index d9e013f0..7928f77e 100644
--- a/src/opt/lpk/lpkMux.c
+++ b/src/opt/lpk/lpkMux.c
@@ -39,18 +39,12 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
+int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
 {
-//    Kit_DsdNtk_t * ppNtks[2], * pTemp;
-    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
-    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
     int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
-//    int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
-
     // iterate through variables
     iBestVar = -1;
-    nSuppSizeMin = ABC_INFINITY;
-//    nPrimeSizeMin = ABC_INFINITY;
+    nSuppSizeMin = KIT_INFINITY;
     for ( i = 0; i < nVars; i++ )
     {
         // cofactor the functiona and get support sizes
@@ -59,44 +53,22 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
         nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
         nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
         nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
-/*
-        // check the size of the largest prime components
-        ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
-        ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
-        // compute the largest non-decomp block
-        nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
-        nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
-        nPrimeSizeCur  = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
-
-        printf( "Evaluating variable %c:\n", 'a'+i );
-//        Kit_DsdPrintExpanded( ppNtks[0] );
-//        Kit_DsdPrintExpanded( ppNtks[1] );
-
-        ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
-        Kit_DsdNtkFree( pTemp );
-
-        ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
-        Kit_DsdNtkFree( pTemp );
-
-        Kit_DsdPrint( stdout, ppNtks[0] );
-        Kit_DsdPrint( stdout, ppNtks[1] );
-
-//        Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
-
-        // free the networks
-        Kit_DsdNtkFree( ppNtks[0] );
-        Kit_DsdNtkFree( ppNtks[1] );
-*/
+        // skip cofactoring that goes above the limit
+        if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
+            continue;
         // compare this variable with other variables
-        if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
+        if ( nSuppSizeMin > nSuppSizeCur ) 
         {
             nSuppSizeMin = nSuppSizeCur;
-//            nPrimeSizeMin = nPrimeSizeCur;
             iBestVar = i;
         }
     }
-    printf( "\n" );
-    assert( iBestVar != -1 );
+    // cofactor w.r.t. this variable
+    if ( iBestVar != -1 )
+    {
+        Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+        Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+    }
     return iBestVar;
 }
 
@@ -113,18 +85,17 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
 ***********************************************************************/
 If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
 {
-    If_Obj_t * pObj0, * pObj1;
-    Kit_DsdNtk_t * ppNtks[2];
     unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
     unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+    If_Obj_t * pObj0, * pObj1;
+    Kit_DsdNtk_t * ppNtks[2];
     int iBestVar;
     assert( nVars > 3 );
     p->fCalledOnce = 1;
-
     // cofactor w.r.t. the best variable
-    iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
-    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
-    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+    iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
+    if ( iBestVar == -1 )
+        return NULL;
     // decompose the functions
     ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
     ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
@@ -158,7 +129,7 @@ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_O
 ***********************************************************************/
 If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
 {
-    Kit_DsdNtk_t * pNtkDec, * pNtkComp;
+    Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
     If_Obj_t * pObjNew;
     unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes,  0 );
     unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes,  1 );
@@ -172,80 +143,96 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
     unsigned * pCo0  = Vec_PtrEntry( p->vTtNodes,  9 );
     unsigned * pCo1  = Vec_PtrEntry( p->vTtNodes, 10 );
     unsigned * pCo   = Vec_PtrEntry( p->vTtNodes, 11 );
-    int TrueMint0, TrueMint1;
+    int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
     int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
 
     // determine if supp-red decomposition exists
     uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
     if ( uSubsets == 0 )
         return NULL;
+    p->nCalledSRed++;
 
-    // get the bound sets
-    uSubset0 = uSubsets & 0xFFFF;
-    uSubset1 = uSubsets >> 16;
     // get the cofactors
     Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
     Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
-    // find any true assignments of the cofactors
-    TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
-    TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
+
+    // get the bound sets
+    uSubset0 = uSubsets & 0xFFFF;
+    uSubset1 = uSubsets >> 16;
+
+    // compute the decomposed functions
+    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+    ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
+    ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
+    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
+    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
+    Kit_DsdNtkFree( ppNtks[0] );
+    Kit_DsdNtkFree( ppNtks[1] );
+//Kit_DsdPrintFromTruth( pDec0, nVars );
+//Kit_DsdPrintFromTruth( pDec1, nVars );
+    // get the decomposed function
+    Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
+
+    // find any true assignments of the decomposed functions
+    TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
+    TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
     assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
+    // find any false assignments of the decomposed functions
+    FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
+    FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
+    assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
+
     // cofactor the cofactors according to these minterms
-    Kit_TruthCopy( pDec0, pCof0, nVars );
-    Kit_TruthCopy( pDec1, pCof1, nVars );
+    Kit_TruthCopy( pCo00, pCof0, nVars );
+    Kit_TruthCopy( pCo01, pCof0, nVars );
     for ( i = 0; i < nVars; i++ )
-        if ( !(uSubset0 & (1 << i)) )
+        if ( uSubset0 & (1 << i) )
         {
+            if ( FalseMint0 & (1 << i) )
+                Kit_TruthCofactor1( pCo00, nVars, i );
+            else
+                Kit_TruthCofactor0( pCo00, nVars, i );
             if ( TrueMint0 & (1 << i) )
-                Kit_TruthCofactor1( pDec0, nVars, i );
+                Kit_TruthCofactor1( pCo01, nVars, i );
             else
-                Kit_TruthCofactor0( pDec0, nVars, i );
+                Kit_TruthCofactor0( pCo01, nVars, i );
         }
+    Kit_TruthCopy( pCo10, pCof1, nVars );
+    Kit_TruthCopy( pCo11, pCof1, nVars );
     for ( i = 0; i < nVars; i++ )
-        if ( !(uSubset1 & (1 << i)) )
+        if ( uSubset1 & (1 << i) )
         {
+            if ( FalseMint1 & (1 << i) )
+                Kit_TruthCofactor1( pCo10, nVars, i );
+            else
+                Kit_TruthCofactor0( pCo10, nVars, i );
             if ( TrueMint1 & (1 << i) )
-                Kit_TruthCofactor1( pDec1, nVars, i );
+                Kit_TruthCofactor1( pCo11, nVars, i );
             else
-                Kit_TruthCofactor0( pDec1, nVars, i );
+                Kit_TruthCofactor0( pCo11, nVars, i );
         }
-    // get the decomposed function
-    Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
 
-    // derive the remainders
-    Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
-    Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
-    Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
-    Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
-    // quantify bound set variables
-    for ( i = 0; i < nVars; i++ )
-        if ( uSubset0 & (1 << i) )
-        {
-            Kit_TruthExist( pCo00, nVars, i );
-            Kit_TruthExist( pCo01, nVars, i );
-        }
-    for ( i = 0; i < nVars; i++ )
-        if ( uSubset1 & (1 << i) )
-        {
-            Kit_TruthExist( pCo10, nVars, i );
-            Kit_TruthExist( pCo11, nVars, i );
-        }
     // derive the functions by composing them with the new variable (iVarReused)
     Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
     Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
+//Kit_DsdPrintFromTruth( pCo0, nVars );
+//Kit_DsdPrintFromTruth( pCo1, nVars );
     // derive the composition function
     Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
 
     // process the decomposed function
     pNtkDec = Kit_DsdDecompose( pDec, nVars );
-    Kit_DsdPrint( stdout, pNtkDec );
-    ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
-    Kit_DsdNtkFree( pNtkDec );
-
-    // process the composition function 
     pNtkComp = Kit_DsdDecompose( pCo, nVars );
-    Kit_DsdPrint( stdout, pNtkComp );
+//Kit_DsdPrint( stdout, pNtkDec );
+//Kit_DsdPrint( stdout, pNtkComp );
+//printf( "cofactored variable %c\n", 'a' + iVar );
+//printf( "reused variable %c\n", 'a' + iVarReused );
+
+    ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
     pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
+
+    Kit_DsdNtkFree( pNtkDec );
     Kit_DsdNtkFree( pNtkComp );
     return pObjNew;
 }
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index 721705cb..d0d56a86 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -104,7 +104,8 @@ unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
 ***********************************************************************/
 unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
 {
-    unsigned uSupport, Entry, i;
+    unsigned uSupport, Entry;
+    int Number, i;
     assert( p->nVars <= 16 );
     Vec_IntClear( vSets );
     Vec_IntPush( vSets, 0 );
@@ -120,8 +121,11 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
     assert( (uSupport & 0xFFFF0000) == 0 );
     Vec_IntPush( vSets, uSupport );
     // set the remaining variables
-    Vec_IntForEachEntry( vSets, Entry, i )
+    Vec_IntForEachEntry( vSets, Number, i )
+    {
+        Entry = Number;
         Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+    }
     return uSupport;
 }
 
@@ -157,10 +161,14 @@ void Lpk_PrintSetOne( int uSupport )
 ***********************************************************************/
 void Lpk_PrintSets( Vec_Int_t * vSets )
 {
-    unsigned uSupport, i;
+    unsigned uSupport;
+    int Number, i;
     printf( "Subsets(%d): ", Vec_IntSize(vSets) );
-    Vec_IntForEachEntry( vSets, uSupport, i )
+    Vec_IntForEachEntry( vSets, Number, i )
+    {
+        uSupport = Number;
         Lpk_PrintSetOne( uSupport );
+    }
     printf( "\n" );
 }
 
@@ -237,7 +245,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
         }
     }
 
-    // check if there are non-overlapping
+    // find the minimum overlap
     nMinOver = 1000;
     for ( s = 0; s < nUsed; s++ )
         if ( nMinOver > Over[Used[s]] )
@@ -267,7 +275,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
             // get the number of overlapping vars
             pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
             // get the support reduction
-            pEntry->SRed  = pEntry->Size - 1 - pEntry->Over;
+            pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
             assert( pEntry->SRed > 0 );
         }
 }
@@ -318,13 +326,21 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
     Vec_Int_t * vSets1 = p->vSets[1];
     unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
     unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
-    int nSets, i, SizeMax;
+    int nSets, i, SizeMax;//, SRedMax;
     unsigned Entry;
+    int fVerbose = p->pPars->fVeryVerbose;
+//    int fVerbose = 0;
 
     // collect decomposable subsets for each pair of cofactors
+    if ( fVerbose )
+    {
+        printf( "\nExploring support-reducing bound-sets of function:\n" );
+        Kit_DsdPrintFromTruth( pTruth, nVars );
+    }
     nSets = 0;
     for ( i = 0; i < nVars; i++ )
     {
+        if ( fVerbose )
         printf( "Evaluating variable %c:\n", 'a'+i );
         // evaluate the cofactor pair
         Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
@@ -334,13 +350,17 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
         ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
         ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
         ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
+        if ( fVerbose )
         Kit_DsdPrint( stdout, ppNtks[0] );
+        if ( fVerbose )
         Kit_DsdPrint( stdout, ppNtks[1] );
         // compute subsets
         Lpk_ComputeSets( ppNtks[0], vSets0 );
         Lpk_ComputeSets( ppNtks[1], vSets1 );
         // print subsets
+        if ( fVerbose )
         Lpk_PrintSets( vSets0 );
+        if ( fVerbose )
         Lpk_PrintSets( vSets1 );
         // free the networks
         Kit_DsdNtkFree( ppNtks[0] );
@@ -350,7 +370,9 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
     }
 
     // print the results
+    if ( fVerbose )
     printf( "\n" );
+    if ( fVerbose )
     for ( i = 0; i < nSets; i++ )
         Lpk_MapSuppPrintSet( pStore + i, i );
 
@@ -368,14 +390,33 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
             SizeMax = pSet->Size;
         }
     }
+/*
+    // if the best is not choosen, select the one with largest reduction
+    SRedMax = 0;
+    if ( pSetBest == NULL )
+    {
+        for ( i = 0; i < nSets; i++ )
+        {
+            pSet = pStore + i;
+            if ( SRedMax < pSet->SRed )
+            {
+                pSetBest = pSet;
+                SRedMax = pSet->SRed;
+            }
+        }
+    }
+*/
     if ( pSetBest == NULL )
     {
+        if ( fVerbose )
         printf( "Could not select a subset.\n" );
         return 0;
     }
     else
     {
+        if ( fVerbose )
         printf( "Selected the following subset:\n" );
+        if ( fVerbose )
         Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
     }
 
diff --git a/src/opt/res/module.make b/src/opt/res/module.make
index 85936f5b..52d8a315 100644
--- a/src/opt/res/module.make
+++ b/src/opt/res/module.make
@@ -4,5 +4,4 @@ SRC +=  src/opt/res/resCore.c \
     src/opt/res/resSat.c \
     src/opt/res/resSim.c \
     src/opt/res/resStrash.c \
-    src/opt/res/resUpdate.c \
     src/opt/res/resWin.c
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 1d0711f6..27e9b3ea 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -102,9 +102,9 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
     p->pSim = Res_SimAlloc( pPars->nSimWords );
     p->pMan = Int_ManAlloc( 512 );
     p->vMem = Vec_IntAlloc( 0 );
-    p->vResubs = Vec_VecStart( pPars->nCands );
+    p->vResubs  = Vec_VecStart( pPars->nCands );
     p->vResubsW = Vec_VecStart( pPars->nCands );
-    p->vLevels = Vec_VecStart( 32 );
+    p->vLevels  = Vec_VecStart( 32 );
     return p;
 }
 
@@ -123,6 +123,14 @@ void Res_ManFree( Res_Man_t * p )
 {
     if ( p->pPars->fVerbose )
     {
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nTotalNodes-p->nTotalNodes2, 
+            100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalNets-p->nTotalNets2, 
+            100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+        printf( "\n" );
+
         printf( "Winds = %d. ", p->nWins );
         printf( "Nodes = %d. (Ave = %5.1f)  ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
         printf( "Divs = %d. (Ave = %5.1f)  ",  p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
@@ -134,13 +142,6 @@ void Res_ManFree( Res_Man_t * p )
         printf( "Cands = %d. ", p->nCandSets );
         printf( "Proved = %d.", p->nProvedSets );
         printf( "\n" );
-        printf( "Reduction in nodes = %d. (%.2f %%) ", 
-            p->nTotalNodes-p->nTotalNodes2, 
-            100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
-        printf( "Reduction in nets = %d. (%.2f %%) ", 
-            p->nTotalNets-p->nTotalNets2, 
-            100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
-        printf( "\n" );
 
         PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
         PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
@@ -153,7 +154,7 @@ void Res_ManFree( Res_Man_t * p )
         PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
         PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
         PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
-        PRT( "TOTAL      ", p->timeTotal );
+        PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
     }
     Res_WinFree( p->pWin );
     if ( p->pAig ) Abc_NtkDelete( p->pAig );
@@ -169,6 +170,31 @@ void Res_ManFree( Res_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Incrementally updates level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
+{
+    Abc_Obj_t * pObjNew, * pFanin;
+    int k;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+    // update the level of the node
+    Abc_NtkUpdate( pObj, pObjNew, vLevels );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Entrace into the resynthesis package.]
 
   Description []
@@ -210,6 +236,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
 
     // set the number of levels
     Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // try resynthesizing nodes in the topological order
     nNodesOld = Abc_NtkObjNumMax(pNtk);
@@ -239,10 +266,10 @@ p->timeWin += clock() - clk;
                 Vec_PtrSize(p->pWin->vNodes), 
                 Vec_PtrSize(p->pWin->vRoots) );
         }
- 
+
         // collect the divisors
 clk = clock();
-        Res_WinDivisors( p->pWin, pObj->Level + pPars->nGrowthLevel - 1 );
+        Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
 p->timeDiv += clock() - clk;
 
         p->nWins++;
@@ -359,6 +386,7 @@ p->timeUpd += clock() - clk;
 //        printf( "\n" );
     }
     Extra_ProgressBarStop( pProgress );
+    Abc_NtkStopReverseLevels( pNtk );
 
 p->timeSatSim += p->pSim->timeSat;
 p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
deleted file mode 100644
index fb858658..00000000
--- a/src/opt/res/resUpdate.c
+++ /dev/null
@@ -1,123 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [resUpdate.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resynthesis package.]
-
-  Synopsis    [Updates the network after changes.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 15, 2007.]
-
-  Revision    [$Id: resUpdate.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "resInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the level of the node using its fanin levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
-{
-    Abc_Obj_t * pFanin;
-    int i, Level = 0;
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-        Level = ABC_MAX( Level, (int)pFanin->Level );
-    return Level + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Incrementally updates level of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
-{
-    Abc_Obj_t * pFanout, * pTemp;
-    int Lev, k, m;
-    // check if level has changed
-    if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
-        return;
-    // start the data structure for level update
-    Vec_VecClear( vLevels );
-    Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
-    pObjNew->fMarkA = 1;
-    // recursively update level
-    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
-    {
-        pTemp->fMarkA = 0;
-        pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
-        // if the level did not change, to need to check the fanout levels
-        if ( (int)pTemp->Level == Lev )
-            continue;
-        // schedule fanout for level update
-        Abc_ObjForEachFanout( pTemp, pFanout, m )
-            if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
-            {
-                Vec_VecPush( vLevels, pFanout->Level, pFanout );
-                pFanout->fMarkA = 1;
-            }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Incrementally updates level of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
-{
-    Abc_Obj_t * pObjNew, * pFanin;
-    int k;
-    // create the new node
-    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
-    pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( vFanins, pFanin, k )
-        Abc_ObjAddFanin( pObjNew, pFanin );
-    // replace the old node by the new node
-    pObjNew->Level = pObj->Level;
-    Abc_ObjReplace( pObj, pObjNew );
-    // update the level of the node
-    Res_UpdateNetworkLevel( pObjNew, vLevels );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 0b97843a..9696b027 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
 
     p->nNodesConsidered++;
     // get the required times
-    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     // get the node's cuts
 clk = clock();