Version abc70909

20 files changed, 2765 insertions, 352 deletions

diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
new file mode 100644
index 00000000..6e6691f0
--- /dev/null
+++ b/src/aig/kit/cloud.c
@@ -0,0 +1,987 @@
+/**CFile****************************************************************
+
+  FileName    [cloudCore.c]
+
+  PackageName [Fast application-specific BDD package.]
+
+  Synopsis    [The package core.]
+
+  Author      [Alan Mishchenko <alanmi@ece.pdx.edu>]
+  
+  Affiliation [ECE Department. Portland State University, Portland, Oregon.]
+
+  Date        [Ver. 1.0. Started - June 10, 2002.]
+
+  Revision    [$Id: cloudCore.c,v 1.0 2002/06/10 03:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cloud.h"
+
+// the number of operators using cache
+static int CacheOperNum = 4;
+
+// the ratio of cache size to the unique table size for each operator
+static int CacheLogRatioDefault[4] = {
+    2, // CLOUD_OPER_AND, 
+    8, // CLOUD_OPER_XOR, 
+    8, // CLOUD_OPER_BDIFF, 
+    8  // CLOUD_OPER_LEQ 
+};
+
+// the ratio of cache size to the unique table size for each operator
+static int CacheSize[4] = {
+    2, // CLOUD_OPER_AND, 
+    2, // CLOUD_OPER_XOR, 
+    2, // CLOUD_OPER_BDIFF, 
+    2  // CLOUD_OPER_LEQ 
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       FUNCTION DECLARATIONS                      ///
+////////////////////////////////////////////////////////////////////////
+
+// static functions
+static CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
+static void        cloudCacheAllocate( CloudManager * dd, CloudOper oper );
+
+////////////////////////////////////////////////////////////////////////
+///                       FUNCTION DEFINITIONS                       ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function********************************************************************
+
+  Synopsis    [Starts the cloud manager.]
+
+  Description [The first arguments is the number of elementary variables used.
+  The second arguments is the number of bits of the unsigned integer used to 
+  represent nodes in the unique table. If the second argument is 0, the package 
+  assumes 23 to represent nodes, which is equivalent to 2^23 = 8,388,608 nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudManager * Cloud_Init( int nVars, int nBits )
+{
+    CloudManager * dd;
+    int i;
+    int clk1, clk2;
+
+    assert( nVars <= 100000 );
+    assert( nBits < 32 );
+
+    // assign the defaults
+    if ( nBits == 0 )
+        nBits = CLOUD_NODE_BITS;
+
+    // start the manager
+    dd = CALLOC( CloudManager, 1 );
+    dd->nMemUsed          += sizeof(CloudManager);
+
+    // variables
+    dd->nVars             = nVars;              // the number of variables allocated
+    // bits
+    dd->bitsNode          = nBits;              // the number of bits used for the node
+    for ( i = 0; i < CacheOperNum; i++ )
+        dd->bitsCache[i]  = nBits - CacheLogRatioDefault[i];
+    // shifts
+    dd->shiftUnique       = 8*sizeof(unsigned) - (nBits + 1); // gets node index in the hash table
+    for ( i = 0; i < CacheOperNum; i++ )
+        dd->shiftCache[i] = 8*sizeof(unsigned) - dd->bitsCache[i];
+    // nodes
+    dd->nNodesAlloc       = (1 << (nBits + 1)); // 2 ^ (nBits + 1)
+    dd->nNodesLimit       = (1 << nBits);       // 2 ^  nBits
+
+    // unique table
+clk1 = clock();
+    dd->tUnique           = CALLOC( CloudNode, dd->nNodesAlloc );
+    dd->nMemUsed         += sizeof(CloudNode) * dd->nNodesAlloc;
+clk2 = clock();
+//PRT( "calloc() time", clk2 - clk1 ); 
+
+    // set up the constant node (the only node that is not in the hash table)
+    dd->nSignCur          = 1;
+    dd->tUnique[0].s      = dd->nSignCur;
+    dd->tUnique[0].v      = CLOUD_CONST_INDEX;
+    dd->tUnique[0].e      = CLOUD_VOID;
+    dd->tUnique[0].t      = CLOUD_VOID;
+    dd->one               = dd->tUnique;
+    dd->zero              = Cloud_Not(dd->one);
+    dd->nNodesCur         = 1;
+
+    // special nodes
+    dd->pNodeStart        = dd->tUnique + 1;
+    dd->pNodeEnd          = dd->tUnique + dd->nNodesAlloc;
+
+    // set up the elementary variables
+    dd->vars              = ALLOC( CloudNode *, dd->nVars );
+    dd->nMemUsed         += sizeof(CloudNode *) * dd->nVars;
+    for ( i = 0; i < dd->nVars; i++ )
+        dd->vars[i]   = cloudMakeNode( dd, i, dd->one, dd->zero );
+
+    return dd;
+};
+
+/**Function********************************************************************
+
+  Synopsis    [Stops the cloud manager.]
+
+  Description [The first arguments tells show many elementary variables are used.
+  The second arguments tells how many bits of the unsigned integer are used
+  to represent regular nodes in the unique table.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cloud_Quit( CloudManager * dd )
+{
+    int i;
+    FREE( dd->ppNodes );
+    free( dd->tUnique ); 
+    free( dd->vars ); 
+    for ( i = 0; i < 4; i++ )
+        FREE( dd->tCaches[i] );
+    free( dd ); 
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Prepares the manager for another run.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cloud_Restart( CloudManager * dd )
+{
+    int i;
+    assert( dd->one->s == dd->nSignCur );
+    dd->nSignCur++;
+    dd->one->s++;
+    for ( i = 0; i < dd->nVars; i++ )
+        dd->vars[i]->s++;
+    dd->nNodesCur = 1 + dd->nVars;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [This optional function allocates operation cache of the given size.]
+
+  Description [Cache for each operation is allocated independently when the first 
+  operation of the given type is performed. The user can allocate cache of his/her 
+  preferred size by calling Cloud_CacheAllocate before the first operation of the 
+  given type is performed, but this call is optional. Argument "logratio" gives
+  the binary logarithm of the ratio of the size of the unique table to that of cache.
+  For example, if "logratio" is equal to 3, and the unique table will be 2^3=8 times
+  larger than cache; so, if unique table is 2^23 = 8,388,608 nodes, the cache size 
+  will be 2^3=8 times smaller and equal to 2^20 = 1,048,576 entries.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int logratio )
+{
+    assert( logratio > 0 );            // cache cannot be larger than the unique table 
+    assert( logratio < dd->bitsNode ); // cache cannot be smaller than 2 entries
+
+    if ( logratio )
+    {
+        dd->bitsCache[oper]  = dd->bitsNode - logratio;
+        dd->shiftCache[oper] = 8*sizeof(unsigned) - dd->bitsCache[oper];
+    }
+    cloudCacheAllocate( dd, oper );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Internal cache allocation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void cloudCacheAllocate( CloudManager * dd, CloudOper oper )
+{
+    int nCacheEntries = (1 << dd->bitsCache[oper]);
+
+    if ( CacheSize[oper] == 1 )
+    {
+        dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry1, nCacheEntries );
+        dd->nMemUsed     += sizeof(CloudCacheEntry1) * nCacheEntries;
+    }
+    else if ( CacheSize[oper] == 2 )
+    {
+        dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry2, nCacheEntries );
+        dd->nMemUsed     += sizeof(CloudCacheEntry2) * nCacheEntries;
+    }
+    else if ( CacheSize[oper] == 3 )
+    {
+        dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry3, nCacheEntries );
+        dd->nMemUsed     += sizeof(CloudCacheEntry3) * nCacheEntries;
+    }
+}
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns or creates a new node]
+
+  Description [Checks the unique table for the existance of the node. If the node is 
+  present, returns the node. If the node is absent, creates a new node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
+{
+    CloudNode * pRes;
+    CLOUD_ASSERT(t); 
+    CLOUD_ASSERT(e);
+    assert( v < Cloud_V(t) && v < Cloud_V(e) );       // variable should be above in the order
+    if ( Cloud_IsComplement(t) )
+    {
+        pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
+        if ( pRes != CLOUD_VOID )
+            pRes = Cloud_Not(pRes);            
+    }
+    else
+        pRes = cloudMakeNode( dd, v, t, e );
+    return pRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns or creates a new node]
+
+  Description [Checks the unique table for the existance of the node. If the node is 
+  present, returns the node. If the node is absent, creates a new node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
+{
+    CloudNode * entryUnique;
+
+    CLOUD_ASSERT(t); 
+    CLOUD_ASSERT(e);
+
+    assert( ((int)v) >= 0 && ((int)v) < dd->nVars );  // the variable must be in the range
+    assert( v < Cloud_V(t) && v < Cloud_V(e) );       // variable should be above in the order
+    assert( !Cloud_IsComplement(t) );                 // the THEN edge must not be complemented
+
+    // make sure we are not searching for the constant node
+    assert( t && e );
+
+    // get the unique entry
+    entryUnique = dd->tUnique + cloudHashCudd3(v, t, e, dd->shiftUnique);
+    while ( entryUnique->s == dd->nSignCur )
+    {
+        // compare the node
+        if ( entryUnique->v == v && entryUnique->t == t && entryUnique->e == e )
+        { // the node is found
+            dd->nUniqueHits++;
+            return entryUnique;  // returns the node
+        }
+        // increment the hash value modulus the hash table size
+        if ( ++entryUnique - dd->tUnique == dd->nNodesAlloc )
+            entryUnique = dd->tUnique + 1;
+        // increment the number of steps through the table
+        dd->nUniqueSteps++;
+    }
+    dd->nUniqueMisses++;
+
+    // check if the new node can be created
+    if ( ++dd->nNodesCur == dd->nNodesLimit ) 
+    { // initiate the restart
+        printf( "Cloud needs restart!\n" );
+//        fflush( stdout );
+//        exit(1);
+        return CLOUD_VOID;
+    }
+    // create the node
+    entryUnique->s   = dd->nSignCur;
+    entryUnique->v   = v;
+    entryUnique->t   = t;
+    entryUnique->e   = e;
+    return entryUnique;  // returns the node
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the AND or two BDDs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
+{
+    CloudNode * F, * G, * r;
+    CloudCacheEntry2 * cacheEntry;
+    CloudNode * fv, * fnv, * gv, * gnv, * t, * e;
+    CloudVar  var;
+
+    assert( f <= g );
+
+    // terminal cases
+    F = Cloud_Regular(f);
+    G = Cloud_Regular(g);
+    if ( F == G )
+    {
+        if ( f == g )
+            return f;
+        else
+            return dd->zero;
+    }
+    if ( F == dd->one )
+    {
+        if ( f == dd->one )
+            return g;
+        else
+            return f;
+    }
+
+    // check cache
+    cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
+//    cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
+    r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g );
+    if ( r != CLOUD_VOID )
+    {
+        dd->nCacheHits++;
+        return r;
+    }
+    dd->nCacheMisses++;
+
+
+    // compute cofactors
+    if ( cloudV(F) <= cloudV(G) )
+    {
+        var = cloudV(F);
+        if ( Cloud_IsComplement(f) )
+        {
+            fnv = Cloud_Not(cloudE(F));
+            fv  = Cloud_Not(cloudT(F));
+        }
+        else
+        {
+            fnv = cloudE(F);
+            fv  = cloudT(F);
+        }
+    }
+    else
+    {
+        var = cloudV(G);
+        fv  = fnv = f;
+    }
+
+    if ( cloudV(G) <= cloudV(F) )
+    {
+        if ( Cloud_IsComplement(g) )
+        {
+            gnv = Cloud_Not(cloudE(G));
+            gv  = Cloud_Not(cloudT(G));
+        }
+        else
+        {
+            gnv = cloudE(G);
+            gv  = cloudT(G);
+        }
+    }
+    else
+    {
+        gv = gnv = g;
+    }
+
+    if ( fv <= gv )
+        t = cloudBddAnd( dd, fv, gv );
+    else
+        t = cloudBddAnd( dd, gv, fv );
+
+    if ( t == CLOUD_VOID )
+        return CLOUD_VOID;
+
+    if ( fnv <= gnv )
+        e = cloudBddAnd( dd, fnv, gnv );
+    else
+        e = cloudBddAnd( dd, gnv, fnv );
+
+    if ( e == CLOUD_VOID )
+        return CLOUD_VOID;
+
+    if ( t == e )
+        r = t;
+    else
+    {
+        if ( Cloud_IsComplement(t) )
+        {
+            r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
+            if ( r == CLOUD_VOID )
+                return CLOUD_VOID;
+            r = Cloud_Not(r);
+        }
+        else
+        {
+            r = cloudMakeNode( dd, var, t, e );
+            if ( r == CLOUD_VOID )
+                return CLOUD_VOID;
+        }
+    }
+    cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
+    return r;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the AND or two BDDs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, CloudNode * g )
+{
+    if ( f <= g )
+        return cloudBddAnd(dd,f,g);
+    else
+        return cloudBddAnd(dd,g,f);
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the AND or two BDDs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
+{
+    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
+        return CLOUD_VOID;
+    CLOUD_ASSERT(f);
+    CLOUD_ASSERT(g);
+    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
+        cloudCacheAllocate( dd, CLOUD_OPER_AND );
+    return cloudBddAnd_gate( dd, f, g );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the OR or two BDDs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
+{
+    CloudNode * res;
+    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
+        return CLOUD_VOID;
+    CLOUD_ASSERT(f);
+    CLOUD_ASSERT(g);
+    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
+        cloudCacheAllocate( dd, CLOUD_OPER_AND );
+    res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
+    res = Cloud_NotCond( res, res != CLOUD_VOID );
+    return res;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the XOR or two BDDs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g )
+{
+    CloudNode * t0, * t1, * r;
+    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
+        return CLOUD_VOID;
+    CLOUD_ASSERT(f);
+    CLOUD_ASSERT(g);
+    if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
+        cloudCacheAllocate( dd, CLOUD_OPER_AND );
+    t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
+    if ( t0 == CLOUD_VOID )
+        return CLOUD_VOID;
+    t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
+    if ( t1 == CLOUD_VOID )
+        return CLOUD_VOID;
+    r  = Cloud_bddOr( dd, t0, t1 );
+    return r;
+}
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a DFS from f, clearing the LSB of the next
+  pointers.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [cloudSupport cloudDagSize]
+
+******************************************************************************/
+static void cloudClearMark( CloudManager * dd, CloudNode * n )
+{
+    if ( !cloudNodeIsMarked(n) )
+        return;
+    // clear visited flag
+    cloudNodeUnmark(n);
+    if ( cloudIsConstant(n) )
+        return;
+    cloudClearMark( dd, cloudT(n) );
+    cloudClearMark( dd, Cloud_Regular(cloudE(n)) );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Cloud_Support.]
+
+  Description [Performs the recursive step of Cloud_Support. Performs a
+  DFS from f. The support is accumulated in supp as a side effect. Uses
+  the LSB of the then pointer as visited flag.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+static void cloudSupport( CloudManager * dd, CloudNode * n, int * support )
+{
+    if ( cloudIsConstant(n) || cloudNodeIsMarked(n) )
+        return;
+    // set visited flag
+    cloudNodeMark(n);
+    support[cloudV(n)] = 1;
+    cloudSupport( dd, cloudT(n), support );
+    cloudSupport( dd, Cloud_Regular(cloudE(n)), support );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Finds the variables on which a DD depends.]
+
+  Description [Finds the variables on which a DD depends.
+  Returns a BDD consisting of the product of the variables if
+  successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n )
+{
+    CloudNode * res;
+    int * support, i;
+
+    CLOUD_ASSERT(n);
+
+    // allocate and initialize support array for cloudSupport
+    support = CALLOC( int, dd->nVars );
+
+    // compute support and clean up markers
+    cloudSupport( dd, Cloud_Regular(n), support );
+    cloudClearMark( dd, Cloud_Regular(n) );
+
+    // transform support from array to cube
+    res = dd->one;
+    for ( i = dd->nVars - 1; i >= 0; i-- ) // for each level bottom-up 
+        if ( support[i] == 1 )
+        {
+            res = Cloud_bddAnd( dd, res, dd->vars[i] );
+            if ( res == CLOUD_VOID )
+                break;
+        }
+    FREE( support );
+    return res;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Counts the variables on which a DD depends.]
+
+  Description [Counts the variables on which a DD depends.
+  Returns the number of the variables if successful; Cloud_OUT_OF_MEM
+  otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cloud_SupportSize( CloudManager * dd, CloudNode * n )
+{
+    int * support, i, count;
+
+    CLOUD_ASSERT(n);
+
+    // allocate and initialize support array for cloudSupport
+    support = CALLOC( int, dd->nVars );
+
+    // compute support and clean up markers
+    cloudSupport( dd, Cloud_Regular(n), support );
+    cloudClearMark( dd, Cloud_Regular(n) );
+
+    // count support variables
+    count = 0;
+    for ( i = 0; i < dd->nVars; i++ )
+    {
+        if ( support[i] == 1 )
+            count++;
+    }
+
+    FREE( support );
+    return count;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Cloud_DagSize.]
+
+  Description [Performs the recursive step of Cloud_DagSize. Returns the
+  number of nodes in the graph rooted at n.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int cloudDagSize( CloudManager * dd, CloudNode * n )
+{
+    int tval, eval;
+    if ( cloudNodeIsMarked(n) )
+        return 0;
+    // set visited flag
+    cloudNodeMark(n);
+    if ( cloudIsConstant(n) )
+        return 1;
+    tval = cloudDagSize( dd, cloudT(n) );
+    eval = cloudDagSize( dd, Cloud_Regular(cloudE(n)) );
+    return tval + eval + 1;
+
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Counts the number of nodes in a DD.]
+
+  Description [Counts the number of nodes in a DD. Returns the number
+  of nodes in the graph rooted at node.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cloud_DagSize( CloudManager * dd, CloudNode * n )
+{
+    int res;
+    res = cloudDagSize( dd, Cloud_Regular( n ) );
+    cloudClearMark( dd, Cloud_Regular( n ) );
+    return res;
+
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Cloud_DagSize.]
+
+  Description [Performs the recursive step of Cloud_DagSize. Returns the
+  number of nodes in the graph rooted at n.]
+
+  SideEffects [None]
+
+******************************************************************************/
+static int Cloud_DagCollect_rec( CloudManager * dd, CloudNode * n, int * pCounter )
+{
+    int tval, eval;
+    if ( cloudNodeIsMarked(n) )
+        return 0;
+    // set visited flag
+    cloudNodeMark(n);
+    if ( cloudIsConstant(n) )
+    {
+        dd->ppNodes[(*pCounter)++] = n;
+        return 1;
+    }
+    tval = Cloud_DagCollect_rec( dd, cloudT(n), pCounter );
+    eval = Cloud_DagCollect_rec( dd, Cloud_Regular(cloudE(n)), pCounter );
+    dd->ppNodes[(*pCounter)++] = n;
+    return tval + eval + 1;
+
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Counts the number of nodes in a DD.]
+
+  Description [Counts the number of nodes in a DD. Returns the number
+  of nodes in the graph rooted at node.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cloud_DagCollect( CloudManager * dd, CloudNode * n )
+{
+    int res, Counter = 0;
+    if ( dd->ppNodes == NULL )
+        dd->ppNodes = ALLOC( CloudNode *, dd->nNodesLimit );
+    res = Cloud_DagCollect_rec( dd, Cloud_Regular( n ), &Counter );
+    cloudClearMark( dd, Cloud_Regular( n ) );
+    assert( res == Counter );
+    return res;
+
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Counts the number of nodes in an array of DDs.]
+
+  Description [Counts the number of nodes in a DD. Returns the number
+  of nodes in the graph rooted at node.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Cloud_SharingSize( CloudManager * dd, CloudNode ** pn, int nn )
+{
+    int res, i;
+    res = 0;
+    for ( i = 0; i < nn; i++ )
+        res += cloudDagSize( dd, Cloud_Regular( pn[i] ) );
+    for ( i = 0; i < nn; i++ )
+        cloudClearMark( dd, Cloud_Regular( pn[i] ) );
+    return res;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns one cube contained in the given BDD.]
+
+  Description []
+
+  SideEffects []
+
+******************************************************************************/
+CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
+{
+    CloudNode * bFunc0, * bFunc1, * res;
+
+    if ( Cloud_IsConstant(bFunc) )
+        return bFunc;
+
+    // cofactor
+    if ( Cloud_IsComplement(bFunc) )
+    {
+        bFunc0 = Cloud_Not( cloudE(bFunc) );
+        bFunc1 = Cloud_Not( cloudT(bFunc) );
+    }
+    else
+    {
+        bFunc0 = cloudE(bFunc);
+        bFunc1 = cloudT(bFunc);
+    }
+
+    // try to find the cube with the negative literal
+    res = Cloud_GetOneCube( dd, bFunc0 );
+    if ( res == CLOUD_VOID )
+        return CLOUD_VOID;
+
+    if ( res != dd->zero )
+    {
+        res = Cloud_bddAnd( dd, res, Cloud_Not(dd->vars[Cloud_V(bFunc)]) );
+    }
+    else
+    {
+        // try to find the cube with the positive literal
+        res = Cloud_GetOneCube( dd, bFunc1 );
+        if ( res == CLOUD_VOID )
+            return CLOUD_VOID;
+        assert( res != dd->zero );
+        res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
+    }
+    return res;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Prints the BDD as a set of disjoint cubes to the standard output.]
+
+  Description []
+
+  SideEffects []
+
+******************************************************************************/
+void Cloud_bddPrint( CloudManager * dd, CloudNode * Func )
+{
+    CloudNode * Cube;
+    int fFirst = 1;
+
+    if ( Func == dd->zero )
+        printf( "Constant 0." );
+    else if ( Func == dd->one )
+        printf( "Constant 1." );
+    else
+    {
+        while ( 1 )
+        {
+            Cube = Cloud_GetOneCube( dd, Func );
+            if ( Cube == CLOUD_VOID || Cube == dd->zero )
+                break;
+            if ( fFirst )       fFirst = 0;
+            else                printf( " + " );
+            Cloud_bddPrintCube( dd, Cube );
+            Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) );
+        } 
+    }
+    printf( "\n" );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Prints one cube.]
+
+  Description []
+
+  SideEffects []
+
+******************************************************************************/
+void Cloud_bddPrintCube( CloudManager * dd, CloudNode * bCube )
+{
+    CloudNode * bCube0, * bCube1;
+
+    assert( !Cloud_IsConstant(bCube) );
+    while ( 1 )
+    {
+        // get the node structure
+        if ( Cloud_IsConstant(bCube) )
+            break;
+
+        // cofactor the cube
+        if ( Cloud_IsComplement(bCube) )
+        {
+            bCube0 = Cloud_Not( cloudE(bCube) );
+            bCube1 = Cloud_Not( cloudT(bCube) );
+        }
+        else
+        {
+            bCube0 = cloudE(bCube);
+            bCube1 = cloudT(bCube);
+        }
+
+        if ( bCube0 != dd->zero )
+        {
+            assert( bCube1 == dd->zero );
+            printf( "[%d]'", cloudV(bCube) );
+            bCube = bCube0;
+        }
+        else
+        {
+            assert( bCube1 != dd->zero );
+            printf( "[%d]", cloudV(bCube) );
+            bCube = bCube1;
+        }
+    }
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints info.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cloud_PrintInfo( CloudManager * dd )
+{
+    if ( dd == NULL ) return;
+    printf( "The number of unique table nodes allocated = %12d.\n", dd->nNodesAlloc );
+    printf( "The number of unique table nodes present   = %12d.\n", dd->nNodesCur );
+    printf( "The number of unique table hits            = %12d.\n", dd->nUniqueHits );
+    printf( "The number of unique table misses          = %12d.\n", dd->nUniqueMisses );
+    printf( "The number of unique table steps           = %12d.\n", dd->nUniqueSteps );
+    printf( "The number of cache hits                   = %12d.\n", dd->nCacheHits );
+    printf( "The number of cache misses                 = %12d.\n", dd->nCacheMisses );
+    printf( "The current signature                      = %12d.\n", dd->nSignCur );
+    printf( "The total memory in use                    = %12d.\n", dd->nMemUsed );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Prints the state of the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Cloud_PrintHashTable( CloudManager * dd )
+{
+    int i;
+
+    for ( i = 0; i < dd->nNodesAlloc; i++ )
+        if ( dd->tUnique[i].v == CLOUD_CONST_INDEX )
+            printf( "-" );
+        else
+            printf( "+" );
+    printf( "\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h
new file mode 100644
index 00000000..ac9d45f4
--- /dev/null
+++ b/src/aig/kit/cloud.h
@@ -0,0 +1,269 @@
+/**CFile****************************************************************
+
+  FileName    [cloud.h]
+
+  PackageName [Fast application-specific BDD package.]
+
+  Synopsis    [Interface of the package.]
+
+  Author      [Alan Mishchenko <alanmi@ece.pdx.edu>]
+  
+  Affiliation [ECE Department. Portland State University, Portland, Oregon.]
+
+  Date        [Ver. 1.0. Started - June 10, 2002.]
+
+  Revision    [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CLOUD_H__
+#define __CLOUD_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <time.h>
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+////////////////////////////////////////////////////////////////////////
+//  n |  2^n ||  n |    2^n ||  n |        2^n ||  n |           2^n  //
+//====================================================================//
+//  1 |    2 ||  9 |    512 || 17 |    131,072 || 25 |    33,554,432  //
+//  2 |    4 || 10 |  1,024 || 18 |    262,144 || 26 |    67,108,864  // 
+//  3 |    8 || 11 |  2,048 || 19 |    524,288 || 27 |   134,217,728  //
+//  4 |   16 || 12 |  4,096 || 20 |  1,048,576 || 28 |   268,435,456  //
+//  5 |   32 || 13 |  8,192 || 21 |  2,097,152 || 29 |   536,870,912  //
+//  6 |   64 || 14 | 16,384 || 22 |  4,194,304 || 30 | 1,073,741,824  //
+//  7 |  128 || 15 | 32,768 || 23 |  8,388,608 || 31 | 2,147,483,648  //
+//  8 |  256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296  //
+////////////////////////////////////////////////////////////////////////
+
+// data structure typedefs
+typedef struct cloudManager       CloudManager;
+typedef unsigned                  CloudVar;
+typedef unsigned                  CloudSign;
+typedef struct cloudNode          CloudNode;
+typedef struct cloudCacheEntry1   CloudCacheEntry1;
+typedef struct cloudCacheEntry2   CloudCacheEntry2;
+typedef struct cloudCacheEntry3   CloudCacheEntry3;
+
+// operation codes used to set up the cache
+typedef enum { 
+    CLOUD_OPER_AND, 
+    CLOUD_OPER_XOR, 
+    CLOUD_OPER_BDIFF, 
+    CLOUD_OPER_LEQ 
+} CloudOper;
+
+/*
+// the number of operators using cache
+static int CacheOperNum = 4;
+
+// the ratio of cache size to the unique table size for each operator
+static int CacheLogRatioDefault[4] = {
+    4, // CLOUD_OPER_AND, 
+    8, // CLOUD_OPER_XOR, 
+    8, // CLOUD_OPER_BDIFF, 
+    8  // CLOUD_OPER_LEQ 
+};
+
+// the ratio of cache size to the unique table size for each operator
+static int CacheSize[4] = {
+    2, // CLOUD_OPER_AND, 
+    2, // CLOUD_OPER_XOR, 
+    2, // CLOUD_OPER_BDIFF, 
+    2  // CLOUD_OPER_LEQ 
+};
+*/
+
+// data structure definitions
+struct cloudManager            // the fast bdd manager     
+{
+    // variables
+    int nVars;                 // the number of variables allocated
+    // bits
+    int bitsNode;              // the number of bits used for the node
+    int bitsCache[4];          // default: bitsNode - CacheSizeRatio[i]
+    // shifts
+    int shiftUnique;           // 8*sizeof(unsigned) - (bitsNode + 1)
+    int shiftCache[4];         // 8*sizeof(unsigned) -  bitsCache[i]
+    // nodes 
+    int nNodesAlloc;           // 2 ^ (bitsNode + 1)
+    int nNodesLimit;           // 2 ^  bitsNode
+    int nNodesCur;             // the current number of nodes (including const1 and vars)
+    // signature
+    CloudSign nSignCur;
+
+    // statistics
+    int nMemUsed;              // memory usage in bytes
+    // cache stats
+    int nUniqueHits;           // hits in the unique table
+    int nUniqueMisses;         // misses in the unique table
+    int nCacheHits;            // hits in the caches
+    int nCacheMisses;          // misses in the caches
+    // the number of steps through the hash table
+    int nUniqueSteps;
+
+    // tables
+    CloudNode * tUnique;       // the unique table to store BDD nodes
+
+    // special nodes
+    CloudNode * pNodeStart;    // the pointer to the first node
+    CloudNode * pNodeEnd;      // the pointer to the first node out of the table
+
+    // constants and variables
+    CloudNode *  one;          // the one function
+    CloudNode *  zero;         // the zero function
+    CloudNode ** vars;         // the elementary variables
+
+    // temporary storage for nodes
+    CloudNode ** ppNodes;
+
+    // caches
+    CloudCacheEntry2 * tCaches[20];    // caches
+};
+
+struct cloudNode   // representation of the node in the unique table
+{
+    CloudSign   s;         // signature
+    CloudVar    v;         // variable
+    CloudNode * e;         // negative cofactor
+    CloudNode * t;         // positive cofactor
+};
+struct cloudCacheEntry1  // one-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;         // argument 1
+    CloudNode * r;         // result
+};
+struct cloudCacheEntry2  // the two-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;
+    CloudNode * b;
+    CloudNode * r;
+};
+struct cloudCacheEntry3  // the three-argument cache
+{
+    CloudSign   s;         // signature
+    CloudNode * a;
+    CloudNode * b;
+    CloudNode * c;
+    CloudNode * r;
+};
+
+
+// parameters
+#define CLOUD_NODE_BITS              23
+#define CLOUD_ONE                    ((unsigned)0x00000001)
+#define CLOUD_NOT_ONE                ((unsigned)0xfffffffe)
+#define CLOUD_VOID                   ((unsigned)0x00000000)
+
+#define CLOUD_CONST_INDEX            ((unsigned)0x0fffffff)
+#define CLOUD_MARK_ON                ((unsigned)0x10000000)
+#define CLOUD_MARK_OFF               ((unsigned)0xefffffff)
+
+// hash functions a la Buddy
+#define cloudHashBuddy2(x,y,s)       ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))
+#define cloudHashBuddy3(x,y,z,s)     (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))
+// hash functions a la Cudd
+#define DD_P1                           12582917
+#define DD_P2                         4256249
+#define DD_P3                         741457
+#define DD_P4                         1618033999
+#define cloudHashCudd2(f,g,s)        ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
+#define cloudHashCudd3(f,g,h,s)      (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s))
+
+// node complementation (using node)
+#define Cloud_Regular(p)             ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble)
+#define Cloud_Not(p)                 ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE))     // complement the node
+#define Cloud_NotCond(p,c)           (((int)(c))? Cloud_Not(p):(p))                  // complement the node conditionally
+#define Cloud_IsComplement(p)        ((int)(((unsigned)(p)) & CLOUD_ONE))            // check if complemented
+// checking constants (using node)
+#define Cloud_IsConstant(p)          (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
+#define cloudIsConstant(p)           (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
+
+// retrieving values from the node (using node structure)
+#define Cloud_V(p)                   ((Cloud_Regular(p))->v)
+#define Cloud_E(p)                   ((Cloud_Regular(p))->e)
+#define Cloud_T(p)                   ((Cloud_Regular(p))->t)
+// retrieving values from the regular node (using node structure)
+#define cloudV(p)                    ((p)->v)
+#define cloudE(p)                    ((p)->e)
+#define cloudT(p)                    ((p)->t)
+// marking/unmarking (using node structure)
+#define cloudNodeMark(p)             ((p)->v       |= CLOUD_MARK_ON)
+#define cloudNodeUnmark(p)           ((p)->v       &= CLOUD_MARK_OFF)
+#define cloudNodeIsMarked(p)         ((int)((p)->v &  CLOUD_MARK_ON))
+
+// cache lookups and inserts (using node)
+#define cloudCacheLookup1(p,sign,f)     (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID))
+#define cloudCacheLookup2(p,sign,f,g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID))
+#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID))
+// cache inserts
+#define cloudCacheInsert1(p,sign,f,r)     (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
+#define cloudCacheInsert2(p,sign,f,g,r)   (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))
+#define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))
+
+//#define CLOUD_ASSERT(p)              (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd))
+#define CLOUD_ASSERT(p)            assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)
+
+// utility macros
+#ifndef ALLOC
+#define ALLOC(type, num)           ((type *) malloc(sizeof(type) * (num)))
+#endif
+
+#ifndef CALLOC
+#define CALLOC(type, num)           ((type *) calloc((num), sizeof(type)))
+#endif
+
+#ifndef FREE
+#define FREE(obj)                   ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#endif
+
+#ifndef PRT
+#define PRT(a,t)                   fprintf( stdout, "%s = ", (a)); printf( "%.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       FUNCTION DECLARATIONS                      ///
+////////////////////////////////////////////////////////////////////////
+// starting/stopping 
+extern CloudManager * Cloud_Init( int nVars, int nBits );
+extern void           Cloud_Quit( CloudManager * dd );
+extern void           Cloud_Restart( CloudManager * dd );
+extern void           Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size );
+extern CloudNode *    Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
+// support and node count
+extern CloudNode *    Cloud_Support( CloudManager * dd, CloudNode * n );
+extern int            Cloud_SupportSize( CloudManager * dd, CloudNode * n );
+extern int            Cloud_DagSize( CloudManager * dd, CloudNode * n );
+extern int            Cloud_DagCollect( CloudManager * dd, CloudNode * n );
+extern int            Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn );
+// cubes
+extern CloudNode *    Cloud_GetOneCube( CloudManager * dd, CloudNode * n );
+extern void           Cloud_bddPrint( CloudManager * dd, CloudNode * Func );
+extern void           Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube );
+// operations
+extern CloudNode *    Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g );
+extern CloudNode *    Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g );
+// stats 
+extern void           Cloud_PrintInfo( CloudManager * dd );
+extern void           Cloud_PrintHashTable( CloudManager * dd );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                            END OF FILE                           ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2ad9a6f0..06a93cf0 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -36,6 +36,7 @@ extern "C" {
 #include <time.h>
 #include "vec.h"
 #include "extra.h"
+#include "cloud.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -133,6 +134,10 @@ struct Kit_DsdMan_t_
     int            nWords;          // the number of words in TTs
     Vec_Ptr_t *    vTtElems;        // elementary truth tables
     Vec_Ptr_t *    vTtNodes;        // the node truth tables
+    // BDD representation
+    CloudManager * dd;              // BDD package
+    Vec_Ptr_t *    vTtBdds;         // the node truth tables
+    Vec_Int_t *    vNodes;          // temporary array for BDD nodes
 };
 
 static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
@@ -431,6 +436,16 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
 }
+static inline void Kit_TruthMuxPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars, int fComp0 )
+{
+    int w;
+    if ( fComp0 )
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
+    else
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
+}
 static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
 {
     unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
@@ -473,11 +488,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
 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 );
+/*=== kitCloud.c ==========================================================*/
+extern CloudNode *     Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars );
+extern unsigned *      Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv );
+extern int             Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes );
+extern int             Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes );
+extern unsigned *      Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes );
+extern void            Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps );
 /*=== kitDsd.c ==========================================================*/
 extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars, int nNodes );
 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, unsigned uSupp );
+extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
 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_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
@@ -485,10 +507,12 @@ 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_DsdDecomposeExpand( 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 unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
@@ -548,6 +572,7 @@ extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, i
 extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
 extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void            Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 );
 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 );
diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c
new file mode 100644
index 00000000..7b160fea
--- /dev/null
+++ b/src/aig/kit/kitCloud.c
@@ -0,0 +1,368 @@
+/**CFile****************************************************************
+
+  FileName    [kitCloud.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation kit.]
+
+  Synopsis    [Procedures using BDD package CLOUD.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 6, 2006.]
+
+  Revision    [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// internal representation of the function to be decomposed
+typedef struct Kit_Mux_t_ Kit_Mux_t;
+struct Kit_Mux_t_
+{
+    unsigned      v  :  5;          // variable 
+    unsigned      t  : 12;          // then edge
+    unsigned      e  : 12;          // else edge
+    unsigned      c  :  1;          // complemented attr of else edge
+    unsigned      i  :  1;          // complemented attr of top node
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derive BDD from the truth table for 5 variable functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
+{
+    static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    CloudNode * pCof0, * pCof1;
+    unsigned uCof0, uCof1;
+    assert( nVars <= 5 );
+    if ( uTruth == 0 )
+        return dd->zero;
+    if ( uTruth == ~0 )
+        return dd->one;
+    if ( nVars == 1 )
+    {
+        if ( uTruth == uVars[0] )
+            return dd->vars[nVarsAll-1];
+        if ( uTruth == ~uVars[0] )
+            return Cloud_Not(dd->vars[nVarsAll-1]);
+        assert( 0 );
+    }
+//    Count++;
+    assert( nVars > 1 );
+    uCof0 = uTruth & ~uVars[nVars-1];
+    uCof1 = uTruth &  uVars[nVars-1];
+    uCof0 |= uCof0 << (1<<(nVars-1));
+    uCof1 |= uCof1 >> (1<<(nVars-1));
+    if ( uCof0 == uCof1 )
+        return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+    if ( uCof0 == ~uCof1 )
+    {
+        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+        pCof1 = Cloud_Not( pCof0 );
+    }
+    else
+    {
+        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+        pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
+    }
+    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
+{
+    CloudNode * pCof0, * pCof1;
+    unsigned * pTruth0, * pTruth1;
+    if ( nVars <= 5 )
+        return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
+    if ( Kit_TruthIsConst0(pTruth, nVars) )
+        return dd->zero;
+    if ( Kit_TruthIsConst1(pTruth, nVars) )
+        return dd->one;
+//    Count++;
+    pTruth0 = pTruth;
+    pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
+    if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
+        return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+    if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
+    {
+        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+        pCof1 = Cloud_Not( pCof0 );
+    }
+    else
+    {
+        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+        pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
+    }
+    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
+{
+    CloudNode * pRes;
+    pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
+//    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
+    return pRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Transforms the array of BDDs into the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
+{
+    Kit_Mux_t Mux;
+    int nNodes, i;
+    // collect BDD nodes
+    nNodes = Cloud_DagCollect( dd, pFunc );
+    if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
+        return 0;
+    assert( nNodes == Cloud_DagSize( dd, pFunc ) );
+    assert( nNodes < dd->nNodesLimit );
+    Vec_IntClear( vNodes );
+    Vec_IntPush( vNodes, 0 ); // const1 node
+    dd->ppNodes[0]->s = 0;
+    for ( i = 1; i < nNodes; i++ )
+    {
+        dd->ppNodes[i]->s = i;
+        Mux.v = dd->ppNodes[i]->v;
+        Mux.t = dd->ppNodes[i]->t->s;
+        Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
+        Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
+        Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
+        // put the MUX into the array
+        Vec_IntPush( vNodes, *((int *)&Mux) );
+    }
+    assert( Vec_IntSize(vNodes) == nNodes );
+    // reset signatures
+    for ( i = 0; i < nNodes; i++ )
+        dd->ppNodes[i]->s = dd->nSignCur;
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Transforms the array of BDDs into the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
+{
+    CloudNode * pFunc;
+    Cloud_Restart( dd );
+    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+    Vec_IntClear( vNodes );
+    return Kit_CreateCloud( dd, pFunc, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes composition of truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
+{
+    unsigned * pThis, * pFan0, * pFan1;
+    Kit_Mux_t Mux;
+    int i, Entry;
+    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+    pThis = Vec_PtrEntry( vStore, 0 );
+    Kit_TruthFill( pThis, nVars );
+    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
+        pFan0 = Vec_PtrEntry( vStore, Mux.e );
+        pFan1 = Vec_PtrEntry( vStore, Mux.t );
+        pThis = Vec_PtrEntry( vStore, i );
+        Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
+    } 
+    // complement the result
+    if ( Mux.i )
+        Kit_TruthNot( pThis, pThis, nVars );
+    return pThis;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes composition of truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, 
+    unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
+{
+    CloudNode * pFunc;
+    unsigned * pThis, * pFan0, * pFan1;
+    Kit_Mux_t Mux;
+    int i, Entry, RetValue;
+    // derive BDD from truth table
+    Cloud_Restart( dd );
+    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+    // convert it into nodes
+    RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
+    if ( RetValue == 0 )
+        printf( "Kit_TruthCompose(): Internal failure!!!\n" );
+    // verify the result
+//    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
+//    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
+//        printf( "Failed!\n" );
+    // compute truth table from the BDD
+    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+    pThis = Vec_PtrEntry( vStore, 0 );
+    Kit_TruthFill( pThis, nVarsAll );
+    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        pFan0 = Vec_PtrEntry( vStore, Mux.e );
+        pFan1 = Vec_PtrEntry( vStore, Mux.t );
+        pThis = Vec_PtrEntry( vStore, i );
+        Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
+    }
+    // complement the result
+    if ( Mux.i )
+        Kit_TruthNot( pThis, pThis, nVarsAll );
+    return pThis;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Compute BDD for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
+{
+    Kit_Mux_t Mux;
+    unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
+    int i, v, Var, Entry, nSupps;
+    nSupps = 2 * nVars;
+
+    // extend storage
+    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
+        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
+    puSuppAll = Vec_IntArray( vMemory );
+    // clear storage for the const node
+    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
+    // compute supports from nodes
+    Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+        Var = nVars - 1 - Mux.v;
+        pFan0 = puSuppAll + nSupps * Mux.e;
+        pFan1 = puSuppAll + nSupps * Mux.t;
+        pThis = puSuppAll + nSupps * i;
+        for ( v = 0; v < nSupps; v++ )
+            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
+        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
+        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
+        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
+        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
+    }
+    // copy the result
+    memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
+    // compute the inverse
+
+    // extend storage
+    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
+        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
+    puSuppAll = Vec_IntArray( vMemory );
+    // clear storage for the const node
+    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
+    // compute supports from nodes
+    Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
+    {
+        Mux = *((Kit_Mux_t *)&Entry);
+//        Var = nVars - 1 - Mux.v;
+        Var = Mux.v;
+        pFan0 = puSuppAll + nSupps * Mux.e;
+        pFan1 = puSuppAll + nSupps * Mux.t;
+        pThis = puSuppAll + nSupps * i;
+        for ( v = 0; v < nSupps; v++ )
+            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
+        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
+        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
+        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
+        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
+    }
+
+    // merge supports
+    for ( Var = 0; Var < nSupps; Var++ )
+        puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 9c61bb6f..ada4ef09 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -44,10 +44,13 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
     Kit_DsdMan_t * p;
     p = ALLOC( Kit_DsdMan_t, 1 );
     memset( p, 0, sizeof(Kit_DsdMan_t) );
-    p->nVars = nVars;
-    p->nWords = Kit_TruthWordNum( p->nVars );
+    p->nVars    = nVars;
+    p->nWords   = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
     p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
+    p->dd       = Cloud_Init( 16, 13 );
+    p->vTtBdds  = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
+    p->vNodes   = Vec_IntAlloc( 512 );
     return p;
 }
 
@@ -64,6 +67,9 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
 ***********************************************************************/
 void Kit_DsdManFree( Kit_DsdMan_t * p )
 {
+    Cloud_Quit( p->dd );
+    Vec_IntFree( p->vNodes );
+    Vec_PtrFree( p->vTtBdds );
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
     free( p );
@@ -315,11 +321,140 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
+unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
 {
     Kit_DsdObj_t * pObj;
-    unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
-    unsigned i, m, iLit, nMints, fCompl, nPartial = 0;
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
+
+    // get the node with this ID
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
+
+    // special case: literal of an internal node
+    if ( pObj == NULL )
+    {
+        assert( Id < pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // constant node
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        assert( pObj->nFans == 0 );
+        Kit_TruthFill( pTruthRes, pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // elementary variable node
+    if ( pObj->Type == KIT_DSD_VAR )
+    {
+        assert( pObj->nFans == 1 );
+        iLit = pObj->pFans[0];
+        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+        if ( Kit_DsdLitIsCompl(iLit) )
+            Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
+        else
+            Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
+        return pTruthRes;
+    }
+
+    // collect the truth tables of the fanins
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+    // create the truth table
+
+    // simple gates
+    if ( pObj->Type == KIT_DSD_AND )
+    {
+        Kit_TruthFill( pTruthRes, pNtk->nVars );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
+        return pTruthRes;
+    }
+    if ( pObj->Type == KIT_DSD_XOR )
+    {
+        Kit_TruthClear( pTruthRes, pNtk->nVars );
+        fCompl = 0;
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        {
+            Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
+            fCompl ^= Kit_DsdLitIsCompl(iLit);
+        }
+        if ( fCompl )
+            Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+        return pTruthRes;
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+/*
+    // get the truth table of the prime node
+    pTruthPrime = Kit_DsdObjTruth( pObj );
+    // get storage for the temporary minterm
+    pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
+
+    // go through the minterms
+    nMints = (1 << pObj->nFans);
+    Kit_TruthClear( pTruthRes, pNtk->nVars );
+    for ( m = 0; m < nMints; m++ )
+    {
+        if ( !Kit_TruthHasBit(pTruthPrime, m) )
+            continue;
+        Kit_TruthFill( pTruthMint, pNtk->nVars );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
+        Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
+    }
+*/
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
+    return pTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
+{
+    unsigned * pTruthRes;
+    int i;
+    // assign elementary truth ables
+    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) );
+    // complement the truth table if needed
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+    return pTruthRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl, nPartial = 0;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
 
     // get the node with this ID
     pObj = Kit_DsdNtkObj( pNtk, Id );
@@ -347,7 +482,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         assert( pObj->nFans == 1 );
         iLit = pObj->pFans[0];
         assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
-        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+        pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
         if ( Kit_DsdLitIsCompl(iLit) )
             Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
         else
@@ -360,7 +495,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     {
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
             if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
-                pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+                pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
             else
             {
                 pTruthFans[i] = NULL;
@@ -370,7 +505,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
     else
     {
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
-            pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+            pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
     }
     // create the truth table
 
@@ -410,7 +545,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
         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
@@ -428,6 +563,9 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
             Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
+*/
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
 }
 
@@ -442,7 +580,7 @@ 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 uSupp )
+unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
 {
     unsigned * pTruthRes;
     int i;
@@ -454,7 +592,7 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
     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), uSupp );
+    pTruthRes = Kit_DsdTruthComputeNodeOne_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 );
@@ -475,9 +613,10 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
 unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec )
 {
     Kit_DsdObj_t * pObj;
-    unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
-    unsigned i, m, iLit, nMints, fCompl, uSuppCur, uSuppFan, nPartial;
     int pfBoundSet[16];
+    unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp;
+    unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur;
+//    unsigned m, nMints, * pTruthPrime, * pTruthMint; 
     assert( uSupp > 0 );
 
     // get the node with this ID
@@ -507,7 +646,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
 
     // if there is no intersection, or full intersection, use simple procedure
     if ( nPartial == 0 || nPartial == pObj->nFans )
-        return Kit_DsdTruthComputeNode_rec( p, pNtk, Id, 0 );
+        return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 );
 
     // if support of the component includes some other variables
     // we need to continue constructing it as usual by the two-function procedure
@@ -520,7 +659,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
             if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) )
                 pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec );
             else
-                pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
+                pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
         }
 
         // create composition/decomposition functions
@@ -556,7 +695,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         // solve the fanins and collect info, which components belong to the bound set
         Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         {
-            pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
+            pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
             pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0);
         }
 
@@ -603,7 +742,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
         // set the corresponding component to be the new variable
         Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar );
     }
-
+/*
     // get the truth table of the prime node
     pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
@@ -621,6 +760,11 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
             Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
+*/
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        assert( !Kit_DsdLitIsCompl(iLit) );
+    pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes );
+    Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars );
     return pTruthRes;
 }
 
@@ -647,12 +791,12 @@ unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsign
     if ( (uSupp & uSuppAll) == 0 )
     {
         Kit_TruthClear( pTruthDec, pNtk->nVars );
-        return Kit_DsdTruthCompute( p, pNtk, 0 );
+        return Kit_DsdTruthCompute( p, pNtk );
     }
     // consider special case - support is fully contained
     if ( (uSupp & uSuppAll) == uSuppAll )
     {
-        pTruthRes = Kit_DsdTruthCompute( p, pNtk, 0 );
+        pTruthRes = Kit_DsdTruthCompute( p, pNtk );
         Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars );
         Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
         return pTruthRes;
@@ -684,7 +828,7 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
     Kit_DsdMan_t * p;
     unsigned * pTruth;
     p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruth = Kit_DsdTruthCompute( p, pNtk );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
     Kit_DsdManFree( p );
 }
@@ -720,7 +864,7 @@ void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSu
 ***********************************************************************/
 void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
 {
-    unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
+    unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
 /*
     // verification
@@ -836,6 +980,32 @@ int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
     return nSizeMax;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finds the union of supports of the non-DSD blocks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned i, uSupport = 0;
+//    FREE( pNtk->pSupps );
+    Kit_DsdGetSupports( pNtk );
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        uSupport |= Kit_DsdLitSupport( pNtk, Kit_DsdVar2Lit(pObj->Id,0) );
+    }
+    return uSupport;
+}
+
 
 /**Function*************************************************************
 
@@ -1759,6 +1929,26 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 
   Synopsis    [Performs decomposition of the truth table.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pNtk, * pTemp;
+    pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
+    pNtk = Kit_DsdExpand( pTemp = pNtk );      
+    Kit_DsdNtkFree( pTemp );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
   Description [Uses MUXes to break-down large prime nodes.]
                
   SideEffects []
@@ -1867,7 +2057,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
@@ -1892,7 +2082,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
     Kit_DsdMan_t * p;
     unsigned * pTruthC;
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
     Kit_DsdManFree( p );
@@ -1934,7 +2124,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 
     // recompute the truth table
     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
-    pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
 //    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
 //    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
     if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
@@ -2004,7 +2194,7 @@ void Kit_DsdPrecompute4Vars()
 */
 
         p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
-        pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+        pTruthC = Kit_DsdTruthCompute( p, pNtk );
         if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
             printf( "Verification failed.\n" );
         Kit_DsdManFree( p );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index d196b455..65389ef9 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -901,6 +901,68 @@ void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int n
 
 /**Function*************************************************************
 
+  Synopsis    [Multiplexes two functions with the given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    if ( fCompl0 == 0 )
+    {
+        Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
+        return;
+    }
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pOut[i]      = ~pCof0[i];
+                pOut[Step+i] = pCof1[Step+i];
+            }
+            pOut += 2*Step;
+            pCof0 += 2*Step;
+            pCof1 += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks symmetry of two variables.]
 
   Description []
@@ -1623,7 +1685,7 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
 {
     static char pFileName[100];
     FILE * pFile;
-    sprintf( pFileName, "s%03d", nFile );
+    sprintf( pFileName, "tt\\s%04d", nFile );
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "rt " );
     Extra_PrintHexadecimal( pFile, pTruth, nVars );
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index a01690d0..25c8e767 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/aig/kit/kitBdd.c \
+    src/aig/kit/kitCloud.c src/aig/kit/cloud.c \
     src/aig/kit/kitDsd.c \
     src/aig/kit/kitFactor.c \
     src/aig/kit/kitGraph.c \
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index d30198c1..604c5ffa 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -45,8 +45,8 @@ static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference );
 int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 {
     int nConeSize1, nConeSize2;
-    assert( Abc_NtkIsStrash(pNode->pNtk) );
-    assert( !Abc_ObjIsComplement( pNode ) );
+//    assert( Abc_NtkIsStrash(pNode->pNtk) );
+//    assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
     if ( Abc_ObjFaninNum(pNode) == 0 )
         return 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 22a8ad54..a8888d81 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2979,22 +2979,20 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-//    printf("This command will be available soon\n");
-//    return 0;
-
     // set defaults
     memset( pPars, 0, sizeof(Lpk_Par_t) );
     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 =  1; // (L) the maximum number of increased levels
+    pPars->nGrowthLevel =  0; // (L) the maximum number of increased levels
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
     pPars->fFirst       =  0;
+    pPars->fOldAlgo     =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3051,6 +3049,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fFirst ^= 1;
             break;
+        case 'o':
+            pPars->fOldAlgo ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -3074,6 +3075,11 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command can only be applied to a logic network.\n" );
         return 1;
     }
+    if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 )
+    {
+        fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared );
+        return 1;
+    }
 
     // modify the current network
     if ( !Lpk_Resynthesize( pNtk, pPars ) )
@@ -3084,17 +3090,18 @@ 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>] [-szfvwh]\n" );
+    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\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 );
-    fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num) [default = %d]\n", pPars->nVarsShared );
+    fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
     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-o       : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "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-w       : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
     return 1;
 } 
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index ecf29f32..47367bc6 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -412,7 +412,7 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
   SeeAlso     []
 
 ******************************************************************************/
-static inline Vec_StrBase10Log( unsigned Num )
+static inline int Vec_StrBase10Log( unsigned Num )
 {
     int Res;
     assert( Num >= 0 );
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;