Version abc70909

10 files changed, 818 insertions, 314 deletions

diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index f1dcd528..2a642db2 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -48,6 +48,7 @@ struct Lpk_Par_t_
     int               fSatur;        // iterate till saturation
     int               fZeroCost;     // accept zero-cost replacements
     int               fFirst;        // use root node and first cut only
+    int               fOldAlgo;      // use old algorithm
     int               fVerbose;      // the verbosiness flag
     int               fVeryVerbose;  // additional verbose info printout
     // internal parameters
diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c
index e9f8d0df..aa2d4bc0 100644
--- a/src/opt/lpk/lpkAbcDec.c
+++ b/src/opt/lpk/lpkAbcDec.c
@@ -39,17 +39,21 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
+Abc_Obj_t * Lpk_ImplementFun( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
 {
     extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
     unsigned * pTruth;
     Abc_Obj_t * pObjNew;
     int i;
+    if ( p->fMark )
+        pMan->nMuxes++;
+    else
+        pMan->nDsds++;
     // create the new node
     pObjNew = Abc_NtkCreateNode( pNtk );
     for ( i = 0; i < (int)p->nVars; i++ )
-        Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
-    Abc_ObjLevelNew( pObjNew );
+        Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(Vec_PtrEntry(vLeaves, p->pFanins[i])) );
+    Abc_ObjSetLevel( pObjNew, Abc_ObjLevelNew(pObjNew) );
     // assign the node's function
     pTruth = Lpk_FunTruth(p, 0);
     if ( p->nVars == 0 )
@@ -78,18 +82,48 @@ Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t *
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+Abc_Obj_t * Lpk_Implement_rec( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * pFun )
 {
-    Lpk_Fun_t * pFun;
-    Abc_Obj_t * pRes;
+    Abc_Obj_t * pFanin, * pRes;
     int i;
-    for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- )
+    // prepare the leaves of the function
+    for ( i = 0; i < (int)pFun->nVars; i++ )
     {
-        pFun = Vec_PtrEntry( vLeaves, i );
-        pRes = Lpk_ImplementFun( pNtk, vLeaves, pFun );
-        Vec_PtrWriteEntry( vLeaves, i, pRes );
-        Lpk_FunFree( pFun );
+        pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
+        if ( !Abc_ObjIsComplement(pFanin) )
+            Lpk_Implement_rec( pMan, pNtk, vLeaves, (Lpk_Fun_t *)pFanin );
+        pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
+        assert( Abc_ObjIsComplement(pFanin) );
     }
+    // construct the function
+    pRes = Lpk_ImplementFun( pMan, pNtk, vLeaves, pFun );
+    // replace the function
+    Vec_PtrWriteEntry( vLeaves, pFun->Id, Abc_ObjNot(pRes) );
+    Lpk_FunFree( pFun );
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the function.]
+
+  Description [Returns the node implementing this function.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_Implement( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+{
+    Abc_Obj_t * pFanin, * pRes;
+    int i;
+    assert( nLeavesOld < Vec_PtrSize(vLeaves) );
+    // mark implemented nodes
+    Vec_PtrForEachEntryStop( vLeaves, pFanin, i, nLeavesOld )
+        Vec_PtrWriteEntry( vLeaves, i, Abc_ObjNot(pFanin) );
+    // recursively construct starting from the first entry
+    pRes = Lpk_Implement_rec( pMan, pNtk, vLeaves, Vec_PtrEntry( vLeaves, nLeavesOld ) );
     Vec_PtrShrink( vLeaves, nLeavesOld );
     return pRes;
 }
@@ -107,10 +141,13 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld
   SeeAlso     []
 
 ***********************************************************************/
-int Lpk_Decompose_rec( Lpk_Fun_t * p )
+int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
 {
+    static Lpk_Res_t Res0, * pRes0 = &Res0;
     Lpk_Res_t * pResMux, * pResDsd;
     Lpk_Fun_t * p2;
+    int clk;
+
     // is only called for non-trivial blocks
     assert( p->nLutK >= 3 && p->nLutK <= 6 );
     assert( p->nVars > p->nLutK );
@@ -120,18 +157,37 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p )
     // skip if delay bound is exceeded
     if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim )
         return 0;
+
+    // compute supports if needed
+    if ( !p->fSupports )
+        Lpk_FunComputeCofSupps( p );
+
+    // check DSD decomposition
+clk = clock();
+    pResDsd = Lpk_DsdAnalize( pMan, p, pMan->pPars->nVarsShared );
+pMan->timeEvalDsdAn += clock() - clk;
+    if ( pResDsd && (pResDsd->nBSVars == (int)p->nLutK || pResDsd->nBSVars == (int)p->nLutK - 1) && 
+          pResDsd->AreaEst <= (int)p->nAreaLim && pResDsd->DelayEst <= (int)p->nDelayLim )
+    {
+clk = clock();
+        p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+pMan->timeEvalDsdSp += clock() - clk;
+        assert( p2->nVars <= (int)p->nLutK );
+        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
+            return 0;
+        return 1;
+    }
+
     // check MUX decomposition
-    pResMux = Lpk_MuxAnalize( p );
+clk = clock();
+    pResMux = Lpk_MuxAnalize( pMan, p );
+pMan->timeEvalMuxAn += clock() - clk;
+//    pResMux = NULL;
     assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) );
     // accept MUX decomposition if it is "good"
     if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK )
         pResDsd = NULL;
-    else
-    {
-        pResDsd = Lpk_DsdAnalize( p );
-        assert( !pResDsd || (pResDsd->DelayEst <= (int)p->nDelayLim && pResDsd->AreaEst <= (int)p->nAreaLim) );
-    }
-    if ( pResMux && pResDsd )
+    else if ( pResMux && pResDsd )
     {
         // compare two decompositions
         if ( pResMux->AreaEst < pResDsd->AreaEst || 
@@ -144,18 +200,22 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p )
     assert( pResMux == NULL || pResDsd == NULL );
     if ( pResMux )
     {
-        p2 = Lpk_MuxSplit( p, pResMux->pCofVars[0], pResMux->Polarity );
-        if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( p2 ) )
+clk = clock();
+        p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
+pMan->timeEvalMuxSp += clock() - clk;
+        if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p2 ) )
             return 0;
-        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
+        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
             return 0;
         return 1;
     }
     if ( pResDsd )
     {
-        p2 = Lpk_DsdSplit( p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+clk = clock();
+        p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+pMan->timeEvalDsdSp += clock() - clk;
         assert( p2->nVars <= (int)p->nLutK );
-        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
+        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
             return 0;
         return 1;
     }
@@ -193,17 +253,31 @@ void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim )
 {
     Lpk_Fun_t * pFun;
     Abc_Obj_t * pObjNew = NULL;
     int nLeaves = Vec_PtrSize( vLeaves );
     pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
+    if ( puSupps[0] || puSupps[1] )
+    {
+/*
+        int i;
+        Lpk_FunComputeCofSupps( pFun );
+        for ( i = 0; i < nLeaves; i++ )
+        {
+            assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] );
+            assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] );
+        }
+*/
+        memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves );
+        pFun->fSupports = 1;
+    }
     Lpk_FunSuppMinimize( pFun );
     if ( pFun->nVars <= pFun->nLutK )
-        pObjNew = Lpk_ImplementFun( pNtk, vLeaves, pFun );
-    else if ( Lpk_Decompose_rec(pFun) )
-        pObjNew = Lpk_Implement( pNtk, vLeaves, nLeaves );
+        pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun );
+    else if ( Lpk_Decompose_rec(p, pFun) )
+        pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves );
     Lpk_DecomposeClean( vLeaves, nLeaves );
     return pObjNew;
 }
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index f2e19945..f4095914 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -41,27 +41,37 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
+int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp )
 {
     int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
     assert( nTruths > 0 );
     VarBest = -1;
     Lpk_SuppForEachVar( p->uSupp, Var )
     {
+        if ( (uNonDecSupp & (1 << Var)) == 0 )
+            continue;
         nSuppMaxCur = 0;
         nSuppTotalCur = 0;
         for ( i = 0; i < nTruths; i++ )
         {
-            Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
-            Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
-            nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
-            nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+            if ( nTruths == 1 )
+            {
+                nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] );
+                nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] );
+            }
+            else
+            {
+                Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
+                Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
+                nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
+                nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+            }        
             nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
             nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
             nSuppTotalCur += nSuppSize0 + nSuppSize1;
         }
-        if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur ||
-             (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) )
+        if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur ||
+             (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) )
         {
             VarBest = Var;
             nSuppMaxMin = nSuppMaxCur;
@@ -175,6 +185,49 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the sets of subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Lpk_PrintSetOne( int uSupport )
+{
+    unsigned k;
+    for ( k = 0; k < 16; k++ )
+        if ( uSupport & (1<<k) )
+            printf( "%c", 'a'+k );
+    printf( " " );
+}
+/**Function*************************************************************
+
+  Synopsis    [Prints the sets of subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Lpk_PrintSets( Vec_Int_t * vSets )
+{
+    unsigned uSupport;
+    int Number, i;
+    printf( "Subsets(%d): ", Vec_IntSize(vSets) );
+    Vec_IntForEachEntry( vSets, Number, i )
+    {
+        uSupport = Number;
+        Lpk_PrintSetOne( uSupport );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Merges two bound sets.]
 
   Description []
@@ -196,7 +249,7 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
         Entry = Entry0 | Entry1;
         if ( (Entry & (Entry >> 16)) )
             continue;
-        if ( Kit_WordCountOnes(Entry) <= nSizeMax )
+        if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax )
             Vec_IntPush( vSets, Entry );
     }
     return vSets;
@@ -204,7 +257,7 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates truth tables for cofactors.]
+  Synopsis    [Performs DSD-based decomposition of the function.]
 
   Description []
                
@@ -213,39 +266,69 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes )
 {
-    int i;
-    assert( nCofDepth <= 4 );
-    ppTruths[0][0] = Lpk_FunTruth( p, 0 );
-    if ( nCofDepth >= 1 )
-    {
-        ppTruths[1][0] = Lpk_FunTruth( p, 1 );
-        ppTruths[1][1] = Lpk_FunTruth( p, 2 );
-    }
-    if ( nCofDepth >= 2 )
-    {
-        ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 );
-        for ( i = 1; i < 4; i++ )
-            ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i;
-    }
-    if ( nCofDepth >= 3 )
+    int fVerbose = 0;
+    unsigned uBoundSet;
+    int i, nVarsBS, nVarsRem, Delay, Area;
+
+    // compare the resulting boundsets
+    memset( pRes, 0, sizeof(Lpk_Res_t) );
+    Vec_IntForEachEntry( vBSets, uBoundSet, i )
     {
-        ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 );
-        for ( i = 1; i < 8; i++ )
-            ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i;
+        if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset
+            continue;
+        if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest
+            continue;
+        if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
+            continue;
+if ( fVerbose )
+Lpk_PrintSetOne( uBoundSet );
+        assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
+        nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
+        if ( nVarsBS == 1 )
+            continue;
+        assert( nVarsBS <= (int)p->nLutK - nCofDepth );
+        nVarsRem = p->nVars - nVarsBS + 1;
+        Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
+        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
+if ( fVerbose )
+printf( "area = %d limit = %d  delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim );
+        if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
+            continue;
+        if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
+        {
+            pRes->nBSVars = nVarsBS;
+            pRes->BSVars = (uBoundSet & 0xFFFF);
+            pRes->nSuppSizeS = nVarsBS + nCofDepth;
+            pRes->nSuppSizeL = nVarsRem;
+            pRes->DelayEst = Delay;
+            pRes->AreaEst = Area;
+        }
     }
-    if ( nCofDepth >= 4 )
+if ( fVerbose )
+{
+if ( pRes->BSVars )
+{
+printf( "Found bound set " );
+Lpk_PrintSetOne( pRes->BSVars );
+printf( "\n" );
+}
+else
+printf( "Did not find boundsets.\n" );
+printf( "\n" );
+}
+    if ( pRes->BSVars )
     {
-        ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 );
-        for ( i = 1; i < 16; i++ )
-            ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i;
+        assert( pRes->DelayEst <= (int)p->nDelayLim );
+        assert( pRes->AreaEst <= (int)p->nAreaLim );
     }
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Allocates truth tables for cofactors.]
+  Synopsis    [Finds late arriving inputs, which cannot be in the bound set.]
 
   Description []
                
@@ -254,14 +337,13 @@ void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p )
 {
-    if ( nCofDepth >= 2 )
-        free( ppTruths[2][0] );
-    if ( nCofDepth >= 3 )
-        free( ppTruths[3][0] );
-    if ( nCofDepth >= 4 )
-        free( ppTruths[4][0] );
+    unsigned i, uLateArrSupp = 0;
+    Lpk_SuppForEachVar( p->uSupp, i )
+        if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
+            uLateArrSupp |= (1 << i);  
+    return uLateArrSupp;
 }
 
 /**Function*************************************************************
@@ -275,58 +357,73 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
+int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes )
 {
-    unsigned * ppTruths[5][16];
+    int fVerbose = 0;
     Vec_Int_t * pvBSets[4][8];
-    Kit_DsdNtk_t * pNtkDec, * pTemp;
-    unsigned uBoundSet;
-    int i, k, nVarsBS, nVarsRem, Delay, Area;
-    assert( nCofDepth >= 0 && nCofDepth < 4 );
+    unsigned uNonDecSupp, uLateArrSupp;
+    int i, k, nNonDecSize, nNonDecSizeMax;
+    assert( nCofDepth >= 1 && nCofDepth <= 3 );
     assert( nCofDepth < (int)p->nLutK - 1 );
-    Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
-    // find the best cofactors
-    memset( pRes, 0, sizeof(Lpk_Res_t) );
-    pRes->nCofVars = nCofDepth;
-    for ( i = 0; i < nCofDepth; i++ )
-        pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+1] );
+    assert( p->fSupports );
+
+    // find the support of the largest non-DSD block
+    nNonDecSizeMax = 0;
+    uNonDecSupp = p->uSupp;
+    for ( i = 0; i < (1<<(nCofDepth-1)); i++ )
+    {
+        nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] );
+        if ( nNonDecSizeMax < nNonDecSize )
+        {
+            nNonDecSizeMax = nNonDecSize;
+            uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] );
+        }
+        else if ( nNonDecSizeMax == nNonDecSize )
+            uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] );
+    }
+
+    // remove those variables that cannot be used because of delay constraints
+    // if variables arrival time is more than p->DelayLim - 2, it cannot be used
+    uLateArrSupp = Lpk_DsdLateArriving( p );
+    if ( (uNonDecSupp & ~uLateArrSupp) == 0 )
+    {
+        memset( pRes, 0, sizeof(Lpk_Res_t) );
+        return 0;
+    }
+
+    // find the next cofactoring variable
+    pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp );
+
     // derive decomposed networks
     for ( i = 0; i < (1<<nCofDepth); i++ )
     {
-        pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars );
-        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
-        pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth );
-        Kit_DsdNtkFree( pNtkDec );
+        if ( pNtks[i] )
+            Kit_DsdNtkFree( pNtks[i] );
+        pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars );
+if ( fVerbose )
+Kit_DsdPrint( stdout, pNtks[i] );
+        pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!!
     }
+
     // derive the set of feasible boundsets
     for ( i = nCofDepth - 1; i >= 0; i-- )
         for ( k = 0; k < (1<<i); k++ )
             pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
-    // compare the resulting boundsets
-    Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
+    // compare bound-sets
+    Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
+    // free the bound sets
+    for ( i = nCofDepth; i >= 0; i-- )
+        for ( k = 0; k < (1<<i); k++ )
+            Vec_IntFree( pvBSets[i][k] );
+ 
+    // copy the cofactoring variables
+    if ( pRes->BSVars )
     {
-        if ( uBoundSet == 0 )
-            continue;
-        assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
-        nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
-        assert( nVarsBS <= (int)p->nLutK - nCofDepth );
-        nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
-        Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
-        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
-        if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
-            continue;
-        if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
-        {
-            pRes->nBSVars = nVarsBS;
-            pRes->BSVars = uBoundSet;
-            pRes->nSuppSizeS = nVarsBS;
-            pRes->nSuppSizeL = nVarsRem;
-            pRes->DelayEst = Delay;
-            pRes->AreaEst = Area;
-        }
+        pRes->nCofVars = nCofDepth;
+        for ( i = 0; i < nCofDepth; i++ )
+            pRes->pCofVars[i] = pCofVars[i];
     }
-    // free cofactor storage
-    Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
+    return 1;
 }
 
 /**Function*************************************************************
@@ -340,47 +437,105 @@ void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
   SeeAlso     []
 
 ***********************************************************************/
-Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
-{
+Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
+{ 
     static Lpk_Res_t Res0, * pRes0 = &Res0;
     static Lpk_Res_t Res1, * pRes1 = &Res1;
     static Lpk_Res_t Res2, * pRes2 = &Res2;
     static Lpk_Res_t Res3, * pRes3 = &Res3;
-    memset( pRes0, 0, sizeof(Lpk_Res_t) );
-    memset( pRes1, 0, sizeof(Lpk_Res_t) );
-    memset( pRes2, 0, sizeof(Lpk_Res_t) );
-    memset( pRes3, 0, sizeof(Lpk_Res_t) );
+    int fUseBackLooking = 1;
+    Lpk_Res_t * pRes = NULL;
+    Vec_Int_t * vBSets;
+    Kit_DsdNtk_t * pNtks[8] = {NULL};
+    char pCofVars[5];
+    int i;
+
+    assert( p->nLutK >= 3 );
+    assert( nShared >= 0 && nShared <= 3 );
     assert( p->uSupp == Kit_BitMask(p->nVars) );
 
     // try decomposition without cofactoring
-    Lpk_DsdAnalizeOne( p, 0, pRes0 );
-    if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim )
-        return pRes0;
+    pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
+    if ( pMan->pPars->fVerbose )
+        pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
+    vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
+    Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
+    Vec_IntFree( vBSets );
+
+    // check the result
+    if ( pRes0->nBSVars == (int)p->nLutK )
+        { pRes = pRes0; goto finish; }
+    if ( pRes0->nBSVars == (int)p->nLutK - 1 )
+        { pRes = pRes0; goto finish; }
+    if ( nShared == 0 )
+        goto finish;
+
+    // prepare storage
+    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
 
     // cofactor 1 time
-    if ( p->nLutK >= 3 ) 
-        Lpk_DsdAnalizeOne( p, 1, pRes1 );
+    if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
+        goto finish;
     assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
-    if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim )
-        return pRes1;
+    if ( pRes1->nBSVars == (int)p->nLutK - 1 )
+        { pRes = pRes1; goto finish; }
+    if ( pRes0->nBSVars == (int)p->nLutK - 2 )
+        { pRes = pRes0; goto finish; }
+    if ( pRes1->nBSVars == (int)p->nLutK - 2 )
+        { pRes = pRes1; goto finish; }
+    if ( nShared == 1 )
+        goto finish;
 
     // cofactor 2 times
     if ( p->nLutK >= 4 ) 
-        Lpk_DsdAnalizeOne( p, 2, pRes2 );
-    assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
-    if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim )
-        return pRes2;
+    {
+        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
+            goto finish;
+        assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
+        if ( pRes2->nBSVars == (int)p->nLutK - 2 )
+            { pRes = pRes2; goto finish; }
+        if ( fUseBackLooking )
+        {
+            if ( pRes0->nBSVars == (int)p->nLutK - 3 )
+                { pRes = pRes0; goto finish; }
+            if ( pRes1->nBSVars == (int)p->nLutK - 3 )
+                { pRes = pRes1; goto finish; }
+        }
+        if ( pRes2->nBSVars == (int)p->nLutK - 3 )
+            { pRes = pRes2; goto finish; }
+        if ( nShared == 2 )
+            goto finish;
+        assert( nShared == 3 );
+    }
 
     // cofactor 3 times
     if ( p->nLutK >= 5 ) 
-        Lpk_DsdAnalizeOne( p, 3, pRes3 );
-    assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
-    if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim )
-        return pRes3;
+    {
+        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
+            goto finish;
+        assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
+        if ( pRes3->nBSVars == (int)p->nLutK - 3 )
+            { pRes = pRes3; goto finish; }
+        if ( fUseBackLooking )
+        {
+            if ( pRes0->nBSVars == (int)p->nLutK - 4 )
+                { pRes = pRes0; goto finish; }
+            if ( pRes1->nBSVars == (int)p->nLutK - 4 )
+                { pRes = pRes1; goto finish; }
+            if ( pRes2->nBSVars == (int)p->nLutK - 4 )
+                { pRes = pRes2; goto finish; }
+        }
+        if ( pRes3->nBSVars == (int)p->nLutK - 4 )
+            { pRes = pRes3; goto finish; }
+    }
 
+finish:
+    // free the networks
+    for ( i = 0; i < (1<<nShared); i++ )
+        if ( pNtks[i] )
+            Kit_DsdNtkFree( pNtks[i] );
     // choose the best under these conditions
-
-    return NULL;
+    return pRes;
 }
 
 /**Function*************************************************************
@@ -394,62 +549,50 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
+Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
 {
     Lpk_Fun_t * pNew;
-    Kit_DsdMan_t * pDsdMan;
-    Kit_DsdNtk_t * pNtkDec, * pTemp;
-    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
-    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
-    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    unsigned * ppTruths[5][16];
-    char pBSVars[5];
-    int i, k, nVars, iVacVar, nCofs;
-    // get the bound set variables
-    nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
+    Kit_DsdNtk_t * pNtkDec;
+    int i, k, iVacVar, nCofs;
+    // prepare storage
+    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
     // get the vacuous variable
-    iVacVar = pBSVars[0];
+    iVacVar = Kit_WordFindFirstBit( uBoundSet );
     // compute the cofactors
-    Lpk_FunAllocTruthTables( p, nCofVars + 1, ppTruths );
     for ( i = 0; i < nCofVars; i++ )
         for ( k = 0; k < (1<<i); k++ )
         {
-            Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->nVars, pCofVars[i] );
-            Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] );
+            Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
+            Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
         }
     // decompose each cofactor w.r.t. the bound set
     nCofs = (1<<nCofVars);
-    pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 2 );
     for ( k = 0; k < nCofs; k++ )
     {
-        pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
-        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
-        Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, iVacVar, ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
+        pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
+        Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
         Kit_DsdNtkFree( pNtkDec );
     }
-    Kit_DsdManFree( pDsdMan );
-    // compute the composition/decomposition functions (they will be in pTruth0/pTruth1)
+    // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
     for ( i = nCofVars; i >= 1; i-- )
         for ( k = 0; k < (1<<i); k++ )
-            Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i-1] );
+            Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );
 
-    // derive the new component
-    pNew = Lpk_FunDup( p, pTruth1 );
-    // update the old component
-    Kit_TruthCopy( pTruth, pTruth0, p->nVars );
-    p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+    // derive the new component (decomposition function)
+    pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
+    // update the old component (composition function)
+    Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
+    p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
     p->pFanins[iVacVar] = pNew->Id;
     p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
     // support minimize both
+    p->fSupports = 0;
     Lpk_FunSuppMinimize( p );
     Lpk_FunSuppMinimize( pNew );
     // update delay and area requirements
     pNew->nDelayLim = p->pDelays[iVacVar];
     pNew->nAreaLim = 1;
     p->nAreaLim = p->nAreaLim - 1;
-
-    // free cofactor storage
-    Lpk_FunFreeTruthTables( p, nCofVars + 1, ppTruths );
     return pNew;
 }
 
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
index 159cae96..d6f579ee 100644
--- a/src/opt/lpk/lpkAbcMux.c
+++ b/src/opt/lpk/lpkAbcMux.c
@@ -30,51 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Computes cofactors w.r.t. the given var.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar )
-{
-    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
-    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
-    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar );
-    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes cofactors w.r.t. each variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
-{
-    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
-    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
-    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    int Var;
-    Lpk_SuppForEachVar( p->uSupp, Var )
-    {
-        Lpk_FunComputeCofs( p, Var );
-        puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
-        puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Checks the possibility of MUX decomposition.]
 
   Description [Returns the best variable to use for MUX decomposition.]
@@ -84,65 +39,68 @@ void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
   SeeAlso     []
 
 ***********************************************************************/
-Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p )
+Lpk_Res_t * Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p )
 {
     static Lpk_Res_t Res, * pRes = &Res;
-    unsigned puSupps[32];
-    int nSuppSize0, nSuppSize1, nSuppSizeBest;
+    int nSuppSize0, nSuppSize1, nSuppSizeS, nSuppSizeL;
     int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB;
     memset( pRes, 0, sizeof(Lpk_Res_t) );
     assert( p->uSupp == Kit_BitMask(p->nVars) );
-    // get cofactor supports for each variable
-    Lpk_FunComputeCofSupps( p, puSupps );
+    assert( p->fSupports );
     // derive the delay and area after MUX-decomp with each var - and find the best var
     pRes->Variable = -1;
     Lpk_SuppForEachVar( p->uSupp, Var )
     {
-        nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]);
-        nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]);
+        nSuppSize0 = Kit_WordCountOnes(p->puSupps[2*Var+0]);
+        nSuppSize1 = Kit_WordCountOnes(p->puSupps[2*Var+1]);
+        assert( nSuppSize0 < (int)p->nVars );
+        assert( nSuppSize1 < (int)p->nVars );
+        if ( nSuppSize0 < 1 || nSuppSize1 < 1 )
+            continue;
+//printf( "%d %d    ", nSuppSize0, nSuppSize1 );
         if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
         {
             // include cof var into 0-block
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
             Delay0 = ABC_MAX( DelayA, DelayB + 1 );
             // include cof var into 1-block
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
             Delay1 = ABC_MAX( DelayA, DelayB + 1 );
             // get the best delay
             Delay = ABC_MIN( Delay0, Delay1 );
             Area = 2;
-            Polarity = (int)(Delay1 == Delay);
+            Polarity = (int)(Delay == Delay1);
         }
         else if ( nSuppSize0 <= (int)p->nLutK - 2 )
         {
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
             Delay = ABC_MAX( DelayA, DelayB + 1 );
             Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
             Polarity = 0;
         }
         else if ( nSuppSize1 <= (int)p->nLutK - 2 )
         {
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
             Delay = ABC_MAX( DelayA, DelayB + 1 );
             Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
             Polarity = 1;
         }
         else if ( nSuppSize0 <= (int)p->nLutK )
         {
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
             Delay = ABC_MAX( DelayA, DelayB + 1 );
             Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
             Polarity = 1;
         }
         else if ( nSuppSize1 <= (int)p->nLutK )
         {
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
             Delay = ABC_MAX( DelayA, DelayB + 1 );
             Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
             Polarity = 0;
@@ -150,12 +108,12 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p )
         else
         {
             // include cof var into 0-block
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
             Delay0 = ABC_MAX( DelayA, DelayB + 1 );
             // include cof var into 1-block
-            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
             Delay1 = ABC_MAX( DelayA, DelayB + 1 );
             // get the best delay
             Delay = ABC_MIN( Delay0, Delay1 );
@@ -163,20 +121,27 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p )
                 Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
             else
                 Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
-            Polarity = (int)(Delay1 == Delay);
+            Polarity = (int)(Delay == Delay1);
         }
         // find the best variable
         if ( Delay > (int)p->nDelayLim )
             continue;
         if ( Area > (int)p->nAreaLim )
             continue;
-        if ( pRes->Variable == -1 || pRes->AreaEst > Area || (pRes->AreaEst == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
+        nSuppSizeS = ABC_MIN( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
+        nSuppSizeL = ABC_MAX( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
+        if ( nSuppSizeL > (int)p->nVars )
+            continue;
+        if ( pRes->Variable == -1 || pRes->AreaEst > Area || 
+            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL > nSuppSizeS + nSuppSizeL) || 
+            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL == nSuppSizeS + nSuppSizeL && pRes->DelayEst > Delay) )
         {
             pRes->Variable = Var;
             pRes->Polarity = Polarity;
             pRes->AreaEst  = Area;
             pRes->DelayEst = Delay;
-            nSuppSizeBest  = nSuppSize0+nSuppSize1;
+            pRes->nSuppSizeS = nSuppSizeS;
+            pRes->nSuppSizeL = nSuppSizeL;
         }
     }
     return pRes->Variable == -1 ? NULL : pRes;
@@ -193,16 +158,27 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol )
+Lpk_Fun_t * Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol )
 {
     Lpk_Fun_t * pNew;
     unsigned * pTruth  = Lpk_FunTruth( p, 0 );
     unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
     unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    int iVarVac;
+//    unsigned uSupp;
+    int iVarVac; 
     assert( Var >= 0 && Var < (int)p->nVars );
     assert( p->nAreaLim >= 2 );
-    Lpk_FunComputeCofs( p, Var );
+    assert( p->uSupp == Kit_BitMask(p->nVars) );
+    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
+    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
+/*
+uSupp = Kit_TruthSupport( pTruth, p->nVars );
+Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
+uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
+uSupp = Kit_TruthSupport( pTruth1, p->nVars );
+Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n\n" );
+*/
     // derive the new component
     pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 );
     // update the support of the old component
@@ -211,29 +187,32 @@ Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol )
     // update the truth table of the old component
     iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
     assert( iVarVac < (int)p->nVars );
-    Kit_TruthIthVar( pTruth, p->nVars, Var );
+    p->uSupp |= (1 << iVarVac);
+    Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
     if ( Pol )
-        Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, iVarVac );
+        Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, Var );
     else
-        Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, iVarVac );
+        Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, Var );
+    assert( p->uSupp == Kit_TruthSupport(pTruth, p->nVars) );
     // set the decomposed variable
     p->pFanins[iVarVac] = pNew->Id;
     p->pDelays[iVarVac] = p->nDelayLim - 1;
     // support minimize both
+    p->fSupports = 0;
     Lpk_FunSuppMinimize( p );
     Lpk_FunSuppMinimize( pNew );
     // update delay and area requirements
     pNew->nDelayLim = p->nDelayLim - 1;
-    if ( p->nVars <= p->nLutK )
-    {
-        pNew->nAreaLim = p->nAreaLim - 1;
-        p->nAreaLim = 1;
-    }
-    else if ( pNew->nVars <= pNew->nLutK )
+    if ( pNew->nVars <= pNew->nLutK )
     {
         pNew->nAreaLim = 1;
         p->nAreaLim = p->nAreaLim - 1;
     }
+    else if ( p->nVars <= p->nLutK )
+    {
+        pNew->nAreaLim = p->nAreaLim - 1;
+        p->nAreaLim = 1;
+    }
     else if ( p->nVars < pNew->nVars )
     {
         pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
@@ -244,7 +223,8 @@ Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol )
         pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
         p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
     }
-    return p;
+    pNew->fMark = 1;
+    return pNew;
 }
 
 
diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c
index 681ec092..3f917ce2 100644
--- a/src/opt/lpk/lpkAbcUtil.c
+++ b/src/opt/lpk/lpkAbcUtil.c
@@ -123,7 +123,7 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
     memcpy( pNew->pFanins, p->pFanins, 16 );
     memcpy( pNew->pDelays, p->pDelays, 16 );
     Vec_PtrPush( p->vNodes, pNew );
-    return p;
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -137,12 +137,15 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
+int Lpk_FunSuppMinimize( Lpk_Fun_t * p )
 {
     int i, k, nVarsNew;
     // compress the truth table
     if ( p->uSupp == Kit_BitMask(p->nVars) )
-        return;
+        return 0;
+    // invalidate support info
+    p->fSupports = 0;
+//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" );
     // minimize support
     nVarsNew = Kit_WordCountOnes(p->uSupp);
     Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
@@ -151,11 +154,48 @@ void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
     {
         p->pFanins[k] = p->pFanins[i];
         p->pDelays[k] = p->pDelays[i];
+/*
+        if ( p->fSupports )
+        {
+            p->puSupps[2*k+0] = p->puSupps[2*i+0];
+            p->puSupps[2*k+1] = p->puSupps[2*i+1];
+        }
+*/
         k++;
     }
     assert( k == nVarsNew );
     p->nVars = k;
     p->uSupp = Kit_BitMask(p->nVars);
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cofactors w.r.t. each variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunComputeCofSupps( Lpk_Fun_t * p )
+{
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    int Var;
+    assert( p->fSupports == 0 );
+//    Lpk_SuppForEachVar( p->uSupp, Var )
+    for ( Var = 0; Var < (int)p->nVars; Var++ )
+    {
+        Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
+        Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
+        p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
+        p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
+    }
+    p->fSupports = 1;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 37bfd956..6ea975aa 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
  
 #include "lpkInt.h"
+#include "cloud.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -127,6 +128,7 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
     If_Obj_t * pDriver, * ppLeaves[16];
     Abc_Obj_t * pLeaf, * pObjNew;
     int nGain, i, clk;
+    int nNodesBef;
 //    int nOldShared;
 
     // check special cases
@@ -201,6 +203,7 @@ p->timeMap += clock() - clk;
     if ( p->nCalledSRed )
         p->nBenefited++;
 
+    nNodesBef = Abc_NtkNodeNum(p->pNtk);
     // prepare the mapping manager
     If_ManCleanNodeCopy( p->pIfMan );
     If_ManCleanCutData( p->pIfMan );
@@ -212,6 +215,7 @@ p->timeMap += clock() - clk;
     pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
     // perform replacement
     Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
     return 1;
 }
 
@@ -232,8 +236,7 @@ int Lpk_ResynthesizeNode( Lpk_Man_t * p )
     Kit_DsdNtk_t * pDsdNtk;
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
-    void * pDsd = NULL;
-    int i, nSuppSize, RetValue, clk;
+    int i, k, nSuppSize, nCutNodes, RetValue, clk;
 
     // compute the cuts
 clk = clock();
@@ -258,9 +261,22 @@ p->timeCuts += clock() - clk;
         if ( p->pPars->fFirst && i == 1 )
             break;
 
+        // skip bad cuts        
+//        printf( "Mffc size = %d.  ", Abc_NodeMffcLabel(p->pObj) );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
+        nCutNodes = Abc_NodeMffcLabel(p->pObj);
+//        printf( "Mffc with cut = %d.  ", nCutNodes );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
+//        printf( "Mffc cut = %d.  ", (int)pCut->nNodes - (int)pCut->nNodesDup );
+//        printf( "\n" );
+        if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
+            continue;
+
         // compute the truth table
 clk = clock();
-        pTruth = Lpk_CutTruth( p, pCut );
+        pTruth = Lpk_CutTruth( p, pCut, 0 );
         nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
 p->timeTruth += clock() - clk;
 
@@ -289,7 +305,7 @@ p->timeTruth += clock() - clk;
             printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
                 i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
             Kit_DsdPrint( stdout, pDsdNtk );
-//            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
 //            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
 //            printf( "Saved truth table in file \"%s\".\n", pFileName );
         }
@@ -305,6 +321,32 @@ p->timeEval += clock() - clk;
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes supports of the cofactors of the function.]
+
+  Description [This procedure should be called after Lpk_CutTruth(p,pCut,0)]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth )
+{
+    unsigned * pTruthInv;
+    int RetValue1, RetValue2;
+    pTruthInv = Lpk_CutTruth( p, pCut, 1 );
+    RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir );
+    RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv );
+    if ( RetValue1 && RetValue2 )
+        Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps ); 
+    else
+        p->puSupps[0] = p->puSupps[1] = 0;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Performs resynthesis for one node.]
@@ -319,12 +361,13 @@ p->timeEval += clock() - clk;
 int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
 {
     static int Count = 0;
-    Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pObjNew;
+    Abc_Obj_t * pObjNew, * pLeaf;
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
-    void * pDsd = NULL;
+    int nNodesBef, nNodesAft, nCutNodes;
     int i, k, clk;
+    int Required = Abc_ObjRequiredLevel(p->pObj);
+//    CloudNode * pFun2;//, * pFun1;
 
     // compute the cuts
 clk = clock();
@@ -336,8 +379,8 @@ p->timeCuts += clock() - clk;
 p->timeCuts += clock() - clk;
 
     if ( p->pPars->fVeryVerbose )
-    printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
-    vLeaves = Vec_PtrAlloc( 32 );
+        printf( "Node %5d : Mffc size = %5d. Cuts = %5d.  Level = %2d. Req = %2d.\n", 
+            p->pObj->Id, p->nMffc, p->nEvals, p->pObj->Level, Required );
     // try the good cuts
     p->nCutsTotal  += p->nCuts;
     p->nCutsUseful += p->nEvals;
@@ -347,16 +390,48 @@ p->timeCuts += clock() - clk;
         pCut = p->pCuts + p->pEvals[i];
         if ( p->pPars->fFirst && i == 1 )
             break;
+//        if ( pCut->Weight < 1.05 )
+//            continue;
+
+        // skip bad cuts        
+//        printf( "Mffc size = %d.  ", Abc_NodeMffcLabel(p->pObj) );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
+        nCutNodes = Abc_NodeMffcLabel(p->pObj);
+//        printf( "Mffc with cut = %d.  ", nCutNodes );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
+//        printf( "Mffc cut = %d.  ", (int)pCut->nNodes - (int)pCut->nNodesDup );
+//        printf( "\n" );
+        if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
+            continue;
 
         // collect nodes into the array
-        Vec_PtrClear( vLeaves );
+        Vec_PtrClear( p->vLeaves );
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) );
+            Vec_PtrPush( p->vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[k]) );
 
         // compute the truth table
 clk = clock();
-        pTruth = Lpk_CutTruth( p, pCut );
+        pTruth = Lpk_CutTruth( p, pCut, 0 );
 p->timeTruth += clock() - clk;
+clk = clock();
+        Lpk_ComputeSupports( p, pCut, pTruth );        
+p->timeSupps += clock() - clk;
+//clk = clock();
+//        pFun1 = Lpk_CutTruthBdd( p, pCut );
+//p->timeTruth2 += clock() - clk;
+/*
+clk = clock();
+        Cloud_Restart( p->pDsdMan->dd );
+        pFun2 = Kit_TruthToCloud( p->pDsdMan->dd, pTruth, pCut->nLeaves );
+        RetValue = Kit_CreateCloud( p->pDsdMan->dd, pFun2, p->vBddNodes );
+p->timeTruth3 += clock() - clk;
+*/
+//        if ( pFun1 != pFun2 )
+//            printf( "Truth tables do not agree!\n" );
+//        else
+//            printf( "Fine!\n" );
 
         if ( p->pPars->fVeryVerbose )
         {
@@ -364,22 +439,51 @@ p->timeTruth += clock() - clk;
             int nSuppSize = Extra_TruthSupportSize( pTruth, pCut->nLeaves );
             printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
                 i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+            Vec_PtrForEachEntry( p->vLeaves, pLeaf, k )
+                printf( "%c=%d ", 'a'+k, Abc_ObjLevel(pLeaf) );
+            printf( "\n" );
             Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
 //            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
 //            printf( "Saved truth table in file \"%s\".\n", pFileName );
         }
+        if ( p->pObj->Id == 33 && i == 0 )
+        {
+            int x = 0;
+        }
 
         // update the network
+        nNodesBef = Abc_NtkNodeNum(p->pNtk);
 clk = clock();
-        pObjNew = Lpk_Decompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize,
-            (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) );
+        pObjNew = Lpk_Decompose( p, p->pNtk, p->vLeaves, pTruth, p->puSupps, p->pPars->nLutSize,
+            (int)pCut->nNodes - (int)pCut->nNodesDup - 1 + (int)(p->pPars->fZeroCost > 0), Required );
 p->timeEval += clock() - clk;
+        nNodesAft = Abc_NtkNodeNum(p->pNtk);
 
         // perform replacement
         if ( pObjNew )
+        {
+            int nGain = (int)pCut->nNodes - (int)pCut->nNodesDup - (nNodesAft - nNodesBef);
+            assert( nGain >= 1 - p->pPars->fZeroCost );
+            assert( Abc_ObjLevel(pObjNew) <= Required );
+/*
+            if ( nGain <= 0 )
+            {
+                int x = 0;
+            }
+            if ( Abc_ObjLevel(pObjNew) > Required )
+            {
+                int x = 0;
+            }
+*/
+            p->nGainTotal += nGain;
+            p->nChanges++;
+            if ( p->pPars->fVeryVerbose )
+                printf( "Performed resynthesis: Gain = %2d. Level = %2d. Req = %2d.\n", nGain, Abc_ObjLevel(pObjNew), Required );
             Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
+            break;
+        }
     }
-    Vec_PtrFree( vLeaves );
     return 1;
 }
 
@@ -443,7 +547,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     if ( p->pPars->fSatur )
         p->vVisited = Vec_VecStart( 0 );
     if ( pPars->fVerbose )
+    {
         p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
+        p->nTotalNodes = Abc_NtkNodeNum(pNtk);
+    }
 
     // iterate over the network
     nNodesPrev = p->nNodesTotal;
@@ -465,7 +572,6 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
                 if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
                     continue;
             }
-
             if ( i >= nNodes )
                 break;
             if ( !pPars->fVeryVerbose )
@@ -475,10 +581,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
                 continue;
             // resynthesize
             p->pObj = pObj;
-            Lpk_ResynthesizeNode( p );
-
-//            if ( p->nChanges == 3 )
-//                break;
+            if ( p->pPars->fOldAlgo )
+                Lpk_ResynthesizeNode( p );
+            else
+                Lpk_ResynthesizeNodeNew( p );
         }
         if ( !pPars->fVeryVerbose )
             Extra_ProgressBarStop( pProgress );
@@ -498,15 +604,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
 
     if ( pPars->fVerbose )
     {
+//        Cloud_PrintInfo( p->pDsdMan->dd );
         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->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
+        printf( "Node gain = %5d. (%.2f %%)  ", 
+            p->nTotalNodes-p->nTotalNodes2, 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+        printf( "Edge gain = %5d. (%.2f %%)  ", 
             p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+        printf( "Muxes = %4d. Dsds = %4d.", p->nMuxes, p->nDsds );
         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] )
@@ -518,7 +627,13 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
         p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
         PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
         PRTP( "Truth ", p->timeTruth, p->timeTotal );
+        PRTP( "CSupps", p->timeSupps, p->timeTotal );
         PRTP( "Eval  ", p->timeEval,  p->timeTotal );
+        PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval );
+        PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval );
+        PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval );
+        PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval );
+        PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval );
         PRTP( "Map   ", p->timeMap,   p->timeTotal );
         PRTP( "Other ", p->timeOther, p->timeTotal );
         PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index f5c0c66c..b2a743bd 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "lpkInt.h"
+#include "cloud.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -39,7 +40,99 @@
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
+CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars )
+{
+    CloudNode * pTruth, * pTruth0, * pTruth1;
+    assert( !Hop_IsComplement(pObj) );
+    if ( pObj->pData )
+    {
+        assert( ((unsigned)pObj->pData) & 0xffff0000 );
+        return pObj->pData;
+    }
+    // get the plan for a new truth table
+    if ( Hop_ObjIsConst1(pObj) )
+        pTruth = dd->one;
+    else
+    {
+        assert( Hop_ObjIsAnd(pObj) );
+        // compute the truth tables of the fanins
+        pTruth0 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin0(pObj), nVars );
+        pTruth1 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin1(pObj), nVars );
+        pTruth0 = Cloud_NotCond( pTruth0, Hop_ObjFaninC0(pObj) );
+        pTruth1 = Cloud_NotCond( pTruth1, Hop_ObjFaninC1(pObj) );
+        // creat the truth table of the node
+        pTruth = Cloud_bddAnd( dd, pTruth0, pTruth1 );
+    }
+    pObj->pData = pTruth;
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the factoring is correct.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+    CloudManager * dd = p->pDsdMan->dd;
+    Hop_Man_t * pManHop = p->pNtk->pManFunc;
+    Hop_Obj_t * pObjHop;
+    Abc_Obj_t * pObj, * pFanin;
+    CloudNode * pTruth;
+    int i, k, iCount = 0;
+
+//    return NULL;
+//    Lpk_NodePrintCut( p, pCut );
+    // initialize the leaves
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)dd->vars[pCut->nLeaves-1-i];
+
+    // construct truth table in the topological order
+    Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
+    {
+        // get the local AIG
+        pObjHop = Hop_Regular(pObj->pData);
+        // clean the data field of the nodes in the AIG subgraph
+        Hop_ObjCleanData_rec( pObjHop );
+        // set the initial truth tables at the fanins
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
+            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
+        }
+        // compute the truth table of internal nodes
+        pTruth = Lpk_CutTruthBdd_rec( dd, pManHop, pObjHop, pCut->nLeaves );
+        if ( Hop_IsComplement(pObj->pData) )
+            pTruth = Cloud_Not(pTruth);
+        // set the truth table at the node
+        pObj->pCopy = (Abc_Obj_t *)pTruth;
+        
+    }
+
+//    Cloud_bddPrint( dd, pTruth );
+//    printf( "Bdd size = %d. Total nodes = %d.\n", Cloud_DagSize( dd, pTruth ), dd->nNodesCur-dd->nVars-1 );
+    return pTruth;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * piCount )
 {
     unsigned * pTruth, * pTruth0, * pTruth1;
     assert( !Hop_IsComplement(pObj) );
@@ -49,17 +142,17 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
         return pObj->pData;
     }
     // get the plan for a new truth table
-    pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
+    pTruth = Vec_PtrEntry( vTtNodes, (*piCount)++ );
     if ( Hop_ObjIsConst1(pObj) )
-        Extra_TruthFill( pTruth, nVars );
+        Kit_TruthFill( pTruth, nVars );
     else
     {
         assert( Hop_ObjIsAnd(pObj) );
         // compute the truth tables of the fanins
-        pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
-        pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
+        pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, piCount );
+        pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, piCount );
         // creat the truth table of the node
-        Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
+        Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
     }
     pObj->pData = pTruth;
     return pTruth;
@@ -76,7 +169,7 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
 {
     Hop_Man_t * pManHop = p->pNtk->pManFunc;
     Hop_Obj_t * pObjHop;
@@ -84,10 +177,11 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
     unsigned * pTruth;
     int i, k, iCount = 0;
 //    Lpk_NodePrintCut( p, pCut );
+    assert( pCut->nNodes > 0 );
 
     // initialize the leaves
     Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
+        pObj->pCopy = Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );
 
     // construct truth table in the topological order
     Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
@@ -105,14 +199,22 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
         // compute the truth table of internal nodes
         pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
         if ( Hop_IsComplement(pObj->pData) )
-            Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
+            Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
         // set the truth table at the node
         pObj->pCopy = (Abc_Obj_t *)pTruth;
     }
 
+    // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!)
+    if ( fInv == 0 )
+    {
+        pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ );
+        Kit_TruthCopy( pTruth, (unsigned *)pObj->pCopy, pCut->nLeaves );
+    }
+    assert( iCount <= Vec_PtrSize(p->vTtNodes) );
     return pTruth;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if at least one entry has changed.]
@@ -535,8 +637,10 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         // 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 = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); 
+//        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax;
         pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
         if ( pCut->Weight <= 1.001 )
+//        if ( pCut->Weight <= 0.999 )
             continue;
         pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
         if ( pCut->fHasDsd )
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 32fb05b3..960599e4 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -90,12 +90,18 @@ struct Lpk_Man_t_
     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
+    Vec_Ptr_t *  vLeaves;
     // truth table representation
     Vec_Ptr_t *  vTtElems;              // elementary truth tables
     Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
+    Vec_Int_t *  vMemory;
+    Vec_Int_t *  vBddDir;
+    Vec_Int_t *  vBddInv;
+    unsigned     puSupps[32];           // the supports of the cofactors
+    unsigned *   ppTruths[5][16];
     // variable sets
     Vec_Int_t *  vSets[8];
-    Kit_DsdMan_t * pDsdMan;
+    Kit_DsdMan_t* pDsdMan;
     // statistics
     int          nNodesTotal;           // total number of nodes
     int          nNodesOver;            // nodes with cuts over the limit 
@@ -104,17 +110,30 @@ struct Lpk_Man_t_
     int          nGainTotal;            // the gain in LUTs
     int          nChanges;              // the number of changed nodes
     int          nBenefited;            // the number of gainful that benefited from decomposition
+    int          nMuxes;
+    int          nDsds;
     int          nTotalNets;
     int          nTotalNets2;
+    int          nTotalNodes;
+    int          nTotalNodes2;
     // counter of non-DSD blocks
     int          nBlocks[17];
-    // rutime
+    // runtime
     int          timeCuts;
     int          timeTruth;
+    int          timeSupps;
+    int          timeTruth2;
+    int          timeTruth3;
     int          timeEval;
     int          timeMap;
     int          timeOther;
     int          timeTotal;
+    // runtime of eval
+    int          timeEvalMuxAn;
+    int          timeEvalMuxSp;
+    int          timeEvalDsdAn;
+    int          timeEvalDsdSp;
+ 
 };
 
 
@@ -122,32 +141,35 @@ struct Lpk_Man_t_
 typedef struct Lpk_Fun_t_ Lpk_Fun_t;
 struct Lpk_Fun_t_
 {
-    Vec_Ptr_t *   vNodes;           // the array of leaves and decomposition nodes
-    unsigned int  Id         :  8;  // the ID of this node
-    unsigned int  nVars      :  5;  // the number of variables
-    unsigned int  nLutK      :  4;  // the number of LUT inputs
-    unsigned int  nAreaLim   :  5;  // the area limit (the largest allowed)
-    unsigned int  nDelayLim  : 10;  // the delay limit (the largest allowed)
-    char          pDelays[16];      // the delays of the inputs
-    char          pFanins[16];      // the fanins of this function
-    unsigned      uSupp;            // the support of this component
-    unsigned      pTruth[0];        // the truth table (contains room for three truth tables)    
+    Vec_Ptr_t *  vNodes;           // the array of leaves and decomposition nodes
+    unsigned     Id         :  7;  // the ID of this node
+    unsigned     nVars      :  5;  // the number of variables
+    unsigned     nLutK      :  4;  // the number of LUT inputs
+    unsigned     nAreaLim   :  5;  // the area limit (the largest allowed)
+    unsigned     nDelayLim  :  9;  // the delay limit (the largest allowed)
+    unsigned     fSupports  :  1;  // supports of cofactors were precomputed
+    unsigned     fMark      :  1;  // marks the MUX-based dec
+    unsigned     uSupp;            // the support of this component
+    unsigned     puSupps[32];      // the supports of the cofactors
+    char         pDelays[16];      // the delays of the inputs
+    char         pFanins[16];      // the fanins of this function
+    unsigned     pTruth[0];        // the truth table (contains room for three truth tables)    
 };
 
 // preliminary decomposition result
 typedef struct Lpk_Res_t_ Lpk_Res_t;
 struct Lpk_Res_t_
 {
-    int           nBSVars;          // the number of bound set variables
-    unsigned      BSVars;           // the bound set
-    int           nCofVars;         // the number of cofactoring variables
-    char          pCofVars[4];      // the cofactoring variables
-    int           nSuppSizeS;       // support size of the smaller (decomposed) function 
-    int           nSuppSizeL;       // support size of the larger (composition) function
-    int           DelayEst;         // estimated delay of the decomposition
-    int           AreaEst;          // estimated area of the decomposition
-    int           Variable;         // variable in MUX decomposition
-    int           Polarity;         // polarity in MUX decomposition
+    int          nBSVars;          // the number of bound set variables
+    unsigned     BSVars;           // the bound set
+    int          nCofVars;         // the number of cofactoring variables
+    char         pCofVars[4];      // the cofactoring variables
+    int          nSuppSizeS;       // support size of the smaller (decomposed) function 
+    int          nSuppSizeL;       // support size of the larger (composition) function
+    int          DelayEst;         // estimated delay of the decomposition
+    int          AreaEst;          // estimated area of the decomposition
+    int          Variable;         // variable in MUX decomposition
+    int          Polarity;         // polarity in MUX decomposition
 };
 
 static inline int        Lpk_LutNumVars( int nLutsLim, int nLutK ) { return  nLutsLim * (nLutK - 1) + 1;                                            }
@@ -177,25 +199,26 @@ static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num )    { assert( Num
 ////////////////////////////////////////////////////////////////////////
 
 /*=== lpkAbcDec.c ============================================================*/
-extern Abc_Obj_t *    Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+extern Abc_Obj_t *    Lpk_Decompose( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim );
 /*=== lpkAbcDsd.c ============================================================*/
-extern Lpk_Res_t *    Lpk_DsdAnalize( Lpk_Fun_t * p );
-extern Lpk_Fun_t *    Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
+extern Lpk_Res_t *    Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared );
+extern Lpk_Fun_t *    Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
 /*=== lpkAbcMux.c ============================================================*/
-extern Lpk_Res_t *    Lpk_MuxAnalize( Lpk_Fun_t * p );
-extern Lpk_Fun_t *    Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol );
+extern Lpk_Res_t *    Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p );
+extern Lpk_Fun_t *    Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol );
 /*=== lpkAbcUtil.c ============================================================*/
 extern Lpk_Fun_t *    Lpk_FunAlloc( int nVars );
 extern void           Lpk_FunFree( Lpk_Fun_t * p );
 extern Lpk_Fun_t *    Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
 extern Lpk_Fun_t *    Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth );
-extern void           Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern int            Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern void           Lpk_FunComputeCofSupps( Lpk_Fun_t * p );
 extern int            Lpk_SuppDelay( unsigned uSupp, char * pDelays );
 extern int            Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
 
 
 /*=== lpkCut.c =========================================================*/
-extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
+extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv );
 extern int            Lpk_NodeCuts( Lpk_Man_t * p );
 /*=== lpkMap.c =========================================================*/
 extern Lpk_Man_t *    Lpk_ManStart( Lpk_Par_t * pPars );
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index 5be198d7..af6a5307 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -42,9 +42,9 @@
 Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
 {
     Lpk_Man_t * p;
-    int i;
+    int i, nWords;
     assert( pPars->nLutsMax <= 16 );
-    assert( pPars->nVarsMax > 0 );
+    assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
     p = ALLOC( Lpk_Man_t, 1 );
     memset( p, 0, sizeof(Lpk_Man_t) );
     p->pPars = pPars;
@@ -52,9 +52,28 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
     p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
     p->vCover = Vec_IntAlloc( 1 << 12 );
+    p->vLeaves = Vec_PtrAlloc( 32 );
     for ( i = 0; i < 8; i++ )
         p->vSets[i] = Vec_IntAlloc(100);
     p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
+    p->vMemory = Vec_IntAlloc( 1024 * 32 );
+    p->vBddDir = Vec_IntAlloc( 256 );
+    p->vBddInv = Vec_IntAlloc( 256 );
+    // allocate temporary storage for truth tables
+    nWords = Kit_TruthWordNum(pPars->nVarsMax);
+    p->ppTruths[0][0] = ALLOC( unsigned, 32 * nWords );
+    p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
+    for ( i = 1; i < 2; i++ )
+        p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
+    p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords;
+    for ( i = 1; i < 4; i++ )
+        p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords;
+    p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords; 
+    for ( i = 1; i < 8; i++ )
+        p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords;
+    p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords; 
+    for ( i = 1; i < 16; i++ )
+        p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords;
     return p;
 }
 
@@ -72,6 +91,10 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
 void Lpk_ManStop( Lpk_Man_t * p )
 {
     int i;
+    free( p->ppTruths[0][0] );
+    Vec_IntFree( p->vBddDir );
+    Vec_IntFree( p->vBddInv );
+    Vec_IntFree( p->vMemory );
     Kit_DsdManFree( p->pDsdMan );
     for ( i = 0; i < 8; i++ )
         Vec_IntFree(p->vSets[i]);
@@ -85,6 +108,7 @@ void Lpk_ManStop( Lpk_Man_t * p )
         Vec_VecFree( p->vLevels );
     if ( p->vVisited )
         Vec_VecFree( p->vVisited );
+    Vec_PtrFree( p->vLeaves );
     Vec_IntFree( p->vCover );
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index d0d56a86..90e46863 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -140,7 +140,7 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_PrintSetOne( int uSupport )
+static void Lpk_PrintSetOne( int uSupport )
 {
     unsigned k;
     for ( k = 0; k < 16; k++ )
@@ -159,7 +159,7 @@ void Lpk_PrintSetOne( int uSupport )
   SeeAlso     []
 
 ***********************************************************************/
-void Lpk_PrintSets( Vec_Int_t * vSets )
+static void Lpk_PrintSets( Vec_Int_t * vSets )
 {
     unsigned uSupport;
     int Number, i;