Exploration of Sasao's decomposition and minor improvements.

6 files changed, 876 insertions, 36 deletions

diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 1c88635a..81990bac 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -52,7 +52,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
+DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars )
 {
     DdNode * bSum, * bCube, * bTemp, * bVar;
     char * pCube;
@@ -65,7 +65,7 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
     {
         for ( v = 0; v < nVars; v++ )
         {
-            bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
+            bSum  = Cudd_bddXor( dd, bTemp = bSum, pbVars? pbVars[v] : Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
             Cudd_RecursiveDeref( dd, bTemp );
         }
     }
@@ -78,9 +78,9 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
             Abc_CubeForEachVar( pCube, Value, v )
             {
                 if ( Value == '0' )
-                    bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+                    bVar = Cudd_Not( pbVars? pbVars[v] : Cudd_bddIthVar( dd, v ) );
                 else if ( Value == '1' )
-                    bVar = Cudd_bddIthVar( dd, v );
+                    bVar = pbVars? pbVars[v] : Cudd_bddIthVar( dd, v );
                 else
                     continue;
                 bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
@@ -128,7 +128,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );
+        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );
         if ( pNode->pData == NULL )
         {
             printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
@@ -282,7 +282,7 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
     // verify
     if ( fVerify )
     {
-        bFuncNew = Abc_ConvertSopToBdd( dd, pSop );  Cudd_Ref( bFuncNew );
+        bFuncNew = Abc_ConvertSopToBdd( dd, pSop, NULL );  Cudd_Ref( bFuncNew );
         if ( bFuncOn == bFuncOnDc )
         {
             if ( bFuncNew != bFuncOn )
@@ -483,7 +483,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( Abc_SopIsComplement((char *)pNode->pData) )
         {
-            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );  Cudd_Ref( bFunc );
+            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );  Cudd_Ref( bFunc );
             pNode->pData = Abc_ConvertBddToSop( (Mem_Flex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
             Cudd_RecursiveDeref( dd, bFunc );
             assert( !Abc_SopIsComplement((char *)pNode->pData) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e158a286..9d30fee8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8665,9 +8665,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 /*
-//    Bbl_ManSimpleDemo();
-//    pNtkRes = Abc_NtkCRetime( pNtk );
-    pNtkRes = NULL;
+{
+    extern Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose );
+    pNtkRes = Abc_NtkBddDec( pNtk, fVerbose );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8675,11 +8675,19 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+}
 */
 
+//    Abc_NtkCheckAbsorb( pNtk, 4 );
+
+    if ( fBmc )
+        Abc_NktMffcServerTest( pNtk );
+    else
+        Abc_ResPartitionTest( pNtk );
+
 //    Abc_NtkHelloWorld( pNtk );
 //    Abc_NktMffcTest( pNtk );
-    Abc_NktMffcServerTest( pNtk );
+//    Abc_NktMffcServerTest( pNtk );
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-h] <file_name>\n" );
diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c
index 7f952f14..177c806e 100644
--- a/src/base/abci/abcCascade.c
+++ b/src/base/abci/abcCascade.c
@@ -30,6 +30,7 @@ ABC_NAMESPACE_IMPL_START
 #define BDD_FUNC_MAX 256
 
 //extern void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc );
+extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -37,6 +38,641 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Derive BDD of the characteristic function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_ResBuildBdd( Abc_Ntk_t * pNtk, DdManager * dd )
+{
+    Vec_Ptr_t * vNodes, * vBdds, * vLocals;
+    Abc_Obj_t * pObj, * pFanin;
+    DdNode * bFunc, * bPart, * bTemp, * bVar;
+    int i, k;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    assert( Abc_NtkCoNum(pNtk) <= 3 );
+    vBdds = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), Cudd_bddIthVar(dd, i) );
+    // create internal node BDDs
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    vLocals = Vec_PtrAlloc( 6 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+        {
+            bFunc = Cudd_NotCond( Cudd_ReadOne(dd), Abc_SopIsConst0((char *)pObj->pData) );  Cudd_Ref( bFunc );
+            Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
+            continue;
+        }
+        Vec_PtrClear( vLocals );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_PtrPush( vLocals, Vec_PtrEntry(vBdds, Abc_ObjId(pFanin)) );
+        bFunc = Abc_ConvertSopToBdd( dd, (char *)pObj->pData, (DdNode **)Vec_PtrArray(vLocals) );  Cudd_Ref( bFunc );
+        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
+    }
+    Vec_PtrFree( vLocals );
+    // create char function
+    bFunc = Cudd_ReadOne( dd );  Cudd_Ref( bFunc );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, i + Abc_NtkCiNum(pNtk) );
+        bTemp = (DdNode *)Vec_PtrEntry( vBdds, Abc_ObjFaninId0(pObj) );
+        bPart = Cudd_bddXnor( dd, bTemp, bVar );          Cudd_Ref( bPart );
+        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, bPart );  Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bPart );
+    }
+    // dereference
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vBdds, Abc_ObjId(pObj)) );
+    Vec_PtrFree( vBdds );
+    Vec_PtrFree( vNodes );
+    // reorder
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Initializes variable partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResStartPart( int nInputs, unsigned uParts[], int nParts )
+{
+    int i, Group, Left, Shift = 0, Count = 0;
+    Group = nInputs / nParts;
+    Left  = nInputs % nParts;
+    for ( i = 0; i < Left; i++ )
+    {
+        uParts[i] = (~((~0) << (Group+1))) << Shift;
+        Shift += Group+1;
+    }
+    for (      ; i < nParts; i++ )
+    {
+        uParts[i] = (~((~0) << Group)) << Shift;
+        Shift += Group;
+    }
+    for ( i = 0; i < nParts; i++ )
+        Count += Extra_WordCountOnes( uParts[i] );
+    assert( Count == nInputs );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Initializes variable partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResStartPart2( int nInputs, unsigned uParts[], int nParts )
+{
+    int i, Count = 0;
+    for ( i = 0; i < nParts; i++ )
+        uParts[i] = 0;
+    for ( i = 0; i < nInputs; i++ )
+        uParts[i % nParts] |= (1 << i);
+    for ( i = 0; i < nParts; i++ )
+        Count += Extra_WordCountOnes( uParts[i] );
+    assert( Count == nInputs );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Returns one if unique pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResCheckUnique( char Pats[], int nPats, int pat )
+{
+    int i;
+    for ( i = 0; i < nPats; i++ )
+        if ( Pats[i] == pat )
+            return 0;
+    return 1;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Check if pattern is decomposable with non-strict.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResCheckNonStrict( char Pattern[], int nVars, int nBits )
+{
+    static char Pat0[256], Pat1[256];
+    int v, m, nPats0, nPats1, nNumber = (1 << (nBits - 1));
+    int Result = 0;
+    for ( v = 0; v < nVars; v++ )
+    {
+        nPats0 = nPats1 = 0;
+        for ( m = 0; m < (1<<nVars); m++ )
+        {
+            if ( (m & (1 << v)) == 0 )
+            {
+                if ( Abc_ResCheckUnique( Pat0, nPats0, Pattern[m] ) )
+                {
+                    Pat0[ nPats0++ ] = Pattern[m];
+                    if ( nPats0 > nNumber )
+                        break;
+                }
+            }
+            else
+            {
+                if ( Abc_ResCheckUnique( Pat1, nPats1, Pattern[m] ) )
+                {
+                    Pat1[ nPats1++ ] = Pattern[m];
+                    if ( nPats1 > nNumber )
+                        break;
+                }
+            }
+        }
+        if ( m == (1<<nVars) )
+            Result++;
+    }
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResCofCount( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pCheck )
+{
+    static char Pattern[256];
+    DdNode * pbVars[32];
+    Vec_Ptr_t * vCofs;
+    DdNode * bCof, * bCube, * bTemp;
+    int i, k, Result, nVars = 0;
+    // collect variables
+    for ( i = 0; i < 32; i++ )
+        if ( uMask & (1 << i) )
+            pbVars[nVars++] = dd->vars[i];
+    assert( nVars <= 8 );
+    // compute cofactors
+    vCofs = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < (1 << nVars); i++ )
+    {
+        bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );  Cudd_Ref( bCube );
+        bCof  = Cudd_Cofactor( dd, bFunc, bCube );               Cudd_Ref( bCof );
+        Cudd_RecursiveDeref( dd, bCube );
+        Vec_PtrForEachEntry( DdNode *, vCofs, bTemp, k )
+            if ( bTemp == bCof )
+                break;
+        if ( k < Vec_PtrSize(vCofs) )
+            Cudd_RecursiveDeref( dd, bCof );
+        else
+            Vec_PtrPush( vCofs, bCof );
+        Pattern[i] = k;
+    }
+    Result = Vec_PtrSize( vCofs );
+    Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
+        Cudd_RecursiveDeref( dd, bCof );
+    Vec_PtrFree( vCofs );
+    if ( pCheck )
+    {
+        *pCheck = Abc_ResCheckNonStrict( Pattern, nVars, Extra_Base2Log(Result) );
+/*
+        if ( *pCheck == 1 && nVars == 4 && Result == 8 )
+        {
+            for ( i = 0; i < (1 << nVars); i++ )
+                printf( "%d ", Pattern[i] );
+            i = 0;
+        }
+*/
+    }
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cost of the partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResCost( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pnCofs, int * pCheck )
+{
+    int nCofs = Abc_ResCofCount( dd, bFunc, uMask, pCheck );
+    int n2Log = Extra_Base2Log( nCofs );
+    if ( pnCofs ) *pnCofs = nCofs;
+    return 10000 * n2Log + (nCofs - (1 << (n2Log-1))) * (nCofs - (1 << (n2Log-1)));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Migrates variables between the two groups.]
+
+  Description [Returns 1 if there is change.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResMigrate( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int iPart1, int iPart2 )
+{
+    unsigned uParts2[2] = { uParts[iPart1], uParts[iPart2] };
+    int i, k, CostCur, CostBest, fChange = 0;
+    assert( (uParts[iPart1] & uParts[iPart2]) == 0 );
+    CostBest = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL ) 
+             + Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
+    for ( i = 0; i < nInputs; i++ )
+    if ( uParts[iPart1] & (1 << i) )
+    {
+        for ( k = 0; k < nInputs; k++ )
+        if ( uParts[iPart2] & (1 << k) )
+        {
+            if ( i == k )
+                continue;
+            uParts[iPart1] ^= (1 << i) | (1 << k);
+            uParts[iPart2] ^= (1 << i) | (1 << k);
+            CostCur = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL ) + Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
+            if ( CostCur < CostBest )
+            {
+                CostCur    = CostBest;
+                uParts2[0] = uParts[iPart1];
+                uParts2[1] = uParts[iPart2];
+                fChange = 1;
+            }
+            uParts[iPart1] ^= (1 << i) | (1 << k);
+            uParts[iPart2] ^= (1 << i) | (1 << k);
+        }
+    }
+    uParts[iPart1] = uParts2[0];
+    uParts[iPart2] = uParts2[1];
+    return fChange;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Migrates variables between the two groups.]
+
+  Description [Returns 1 if there is change.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResPrint( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int nParts )
+{
+    int i, k, nCofs, Cost, CostAll = 0, fCheck;
+    for ( i = 0; i < nParts; i++ )
+    {
+        Cost = Abc_ResCost( dd, bFunc, uParts[i], &nCofs, &fCheck );
+        CostAll += Cost;
+        for ( k = 0; k < nInputs; k++ )
+            printf( "%c", (uParts[i] & (1 << k))? 'a' + k : '-' );
+        printf( " %2d %d-%d %6d   ", nCofs, Extra_Base2Log(nCofs), fCheck, Cost );
+    }
+    printf( "%4d\n", CostAll );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [PrintCompute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResPrintAllCofs( DdManager * dd, DdNode * bFunc, int nInputs, int nCofMax )
+{
+    int i, k, nBits, nCofs, Cost, fCheck;
+    for ( i = 0; i < (1<<nInputs); i++ )
+    {
+        nBits = Extra_WordCountOnes( i );
+        if ( nBits < 3 || nBits > 6 )
+            continue;
+        Cost = Abc_ResCost( dd, bFunc, i, &nCofs, &fCheck );
+        if ( nCofs > nCofMax )
+            continue;
+        for ( k = 0; k < nInputs; k++ )
+            printf( "%c", (i & (1 << k))? 'a' + k : '-' );
+        printf( "  n=%2d  c=%2d  l=%d-%d   %6d\n", 
+            Extra_WordCountOnes(i), nCofs, Extra_Base2Log(nCofs), fCheck, Cost );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResSwapRandom( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int nParts, int nTimes )
+{
+    int i, k, n, iPart1, iPart2;
+    for ( n = 0; n < nTimes; )
+    {
+        // get the vars
+        i = k = 0;
+        while ( i == k )
+        {
+            i = rand() % nInputs;
+            k = rand() % nInputs;
+        }
+        // find the groups
+        for ( iPart1 = 0; iPart1 < nParts; iPart1++ )
+            if ( uParts[iPart1] & (1 << i) )
+                break;
+        for ( iPart2 = 0; iPart2 < nParts; iPart2++ )
+            if ( uParts[iPart2] & (1 << k) )
+                break;
+        if ( iPart1 == iPart2 )
+            continue;
+        // swap the vars
+        uParts[iPart1] ^= (1 << i) | (1 << k);
+        uParts[iPart2] ^= (1 << i) | (1 << k);
+        n++;
+//printf( "   " );
+//Abc_ResPrint( dd, bFunc, nInputs, uParts, nParts );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResPartition( DdManager * dd, DdNode * bFunc, int nInputs )
+{
+    int nIters = 5;
+    unsigned uParts[10];
+    int i, fChange = 1;
+    int nSuppSize = Cudd_SupportSize( dd, bFunc );
+    printf( "Ins =%3d. Outs =%2d. Nodes =%3d. Supp =%2d.\n", 
+        nInputs, dd->size-nInputs, Cudd_DagSize(bFunc), nSuppSize );
+//Abc_ResPrintAllCofs( dd, bFunc, nInputs, 4 );
+
+    if ( nSuppSize <= 6 )
+    {
+        printf( "Support is less or equal than 6\n" );
+        return;
+    }
+    if ( nInputs <= 12 )
+    {
+        Abc_ResStartPart( nInputs, uParts, 2 );
+        Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
+        for ( i = 0; i < nIters; i++ )
+        {
+            if ( i ) 
+            {
+                printf( "Randomizing... \n" );
+                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 2, 20 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
+            }
+            fChange = 1;
+            while ( fChange )
+            {
+                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
+            }
+        }
+    }
+    else if ( nInputs > 12 && nInputs <= 18 )
+    {
+        Abc_ResStartPart( nInputs, uParts, 3 );
+        Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
+        for ( i = 0; i < nIters; i++ )
+        {
+            if ( i ) 
+            {
+                printf( "Randomizing... \n" );
+                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 3, 20 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
+            }
+            fChange = 1;
+            while ( fChange )
+            {
+                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
+            }
+        }
+    }
+    else if ( nInputs > 18 && nInputs <= 24 )
+    {
+        Abc_ResStartPart( nInputs, uParts, 4 );
+        Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+        for ( i = 0; i < nIters; i++ )
+        {
+            if ( i )
+            {
+                printf( "Randomizing... \n" );
+                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 4, 20 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+            }
+            fChange = 1;
+            while ( fChange )
+            {
+                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 3 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 3 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 2, 3 );
+                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
+            }
+        }
+    }
+//    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResPartitionTest( Abc_Ntk_t * pNtk )
+{
+    DdManager * dd;
+    DdNode * bFunc;
+    dd = Cudd_Init( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    bFunc = Abc_ResBuildBdd( pNtk, dd );   Cudd_Ref( bFunc );
+    Abc_ResPartition( dd, bFunc, Abc_NtkCiNum(pNtk) );
+    Cudd_RecursiveDeref( dd, bFunc );
+    Extra_StopManager( dd );
+}
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkBddCofCount( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nVars )
+{
+    Vec_Ptr_t * vCofs;
+    DdNode * bCof, * bCube;
+    int i, Result;
+    vCofs = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < (1 << nVars); i++ )
+    {
+        bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );  Cudd_Ref( bCube );
+        bCof  = Cudd_Cofactor( dd, bFunc, bCube );               Cudd_Ref( bCof );
+        Cudd_RecursiveDeref( dd, bCube );
+        if ( Vec_PtrPushUnique( vCofs, bCof ) )
+            Cudd_RecursiveDeref( dd, bCof );
+    }
+    Result = Vec_PtrSize( vCofs );
+    Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
+        Cudd_RecursiveDeref( dd, bCof );
+    Vec_PtrFree( vCofs );
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkExploreCofs2( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nIns, int nLutSize )
+{
+    int i;
+    printf( "Inputs = %2d.  Nodes = %2d.  LutSize = %2d.\n", nIns, Cudd_DagSize(bFunc), nLutSize );
+    for ( i = 0; i <= nIns - nLutSize; i++ )
+        printf( "[%2d %2d] : %3d\n", i, i+nLutSize-1, Abc_NtkBddCofCount(dd, bFunc, dd->vars+i, nLutSize) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the number of distinct cofactors in the BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkExploreCofs( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nIns, int nLutSize )
+{
+    DdManager * ddNew;
+    DdNode * bFuncNew;
+    DdNode * pbVarsNew[32];
+    int i, k, c, nCofs, nBits;
+
+    ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_ShuffleHeap( ddNew, dd->invperm );
+    bFuncNew = Cudd_bddTransfer( dd, ddNew, bFunc );  Cudd_Ref( bFuncNew );
+
+    for ( i = 0; i < (1 << nIns); i++ )
+    {
+        nBits = Extra_WordCountOnes(i);
+        if ( nBits != nLutSize && nBits != nLutSize -1 && nBits != nLutSize -2  )
+            continue;
+        for ( c = k = 0; k < nIns; k++ )
+        {
+            if ( (i & (1 << k)) == 0 )
+                continue;
+//            pbVarsNew[c++] = pbVars[k];
+            pbVarsNew[c++] = ddNew->vars[k];
+        }
+        nCofs = Abc_NtkBddCofCount(ddNew, bFuncNew, pbVarsNew, c);
+        if ( nCofs > 8 )
+            continue;
+
+        for ( c = k = 0; k < nIns; k++ )
+        {
+            if ( (i & (1 << k)) == 0 )
+            {
+                printf( "-" );
+                continue;
+            }
+            printf( "%c", k + 'a' );
+        }
+        printf( " : %2d\n", nCofs );
+    }
+
+    Cudd_RecursiveDeref( ddNew, bFuncNew );
+    Extra_StopManager( ddNew );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Find the constant node corresponding to the encoded output value.]
 
   Description []
@@ -136,6 +772,64 @@ DdNode * Abc_NtkBddToAdd( DdManager * dd, DdNode * bFunc, int nOuts )
 
 /**Function*************************************************************
 
+  Synopsis    [Recursively construct ADD for BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkAddToBdd_rec( DdManager * dd, DdNode * aFunc, int nIns, int nOuts, stmm_table * tTable )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    DdNode ** ppSlot;
+    assert( !Cudd_IsComplement(aFunc) );
+    if ( stmm_find_or_add( tTable, (char *)aFunc, (char ***)&ppSlot ) )
+        return *ppSlot;
+    if ( Cudd_IsConstant(aFunc) )
+    {
+        assert( Cudd_ReadSize(dd) >= nIns + nOuts );
+        bFunc  = Extra_bddBitsToCube( dd, (int)Cudd_V(aFunc), nOuts, dd->vars + nIns, 1 );  Cudd_Ref( bFunc );
+    }
+    else
+    {
+        assert( aFunc->index < nIns );
+        bFunc0 = Abc_NtkAddToBdd_rec( dd, cuddE(aFunc), nIns, nOuts, tTable );
+        bFunc1 = Abc_NtkAddToBdd_rec( dd, cuddT(aFunc), nIns, nOuts, tTable );                                                
+        bFunc  = Cudd_bddIte( dd, Cudd_bddIthVar(dd, aFunc->index), bFunc1, bFunc0 );  Cudd_Ref( bFunc );
+    }
+    return (*ppSlot = bFunc);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [R]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkAddToBdd( DdManager * dd, DdNode * aFunc, int nIns, int nOuts )
+{
+    DdNode * bFunc, * bTemp, * aTemp;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    tTable = stmm_init_table( st_ptrcmp, st_ptrhash );
+    bFunc = Abc_NtkAddToBdd_rec( dd, aFunc, nIns, nOuts, tTable );  
+    stmm_foreach_item( tTable, gen, (char **)&aTemp, (char **)&bTemp )
+        Cudd_RecursiveDeref( dd, bTemp );
+    stmm_free_table( tTable );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the characteristic function.]
 
   Description []
@@ -177,24 +871,37 @@ DdNode * Abc_NtkBddDecCharFunc( DdManager * dd, DdNode ** pFuncs, int nOuts, int
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkBddDecTry( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nOuts, int Mask, int nBits )
+DdNode * Abc_NtkBddDecTry( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nIns, int nOuts, int Mask, int nBits )
 {
-    DdNode * bFunc, * aFunc, * aFuncNew;
-    // drive the characteristic function
+    int fReorder = 0;
+    DdNode * bFunc;//, * aFunc, * aFuncNew;
+    // derive the characteristic function
     bFunc = Abc_NtkBddDecCharFunc( dd, pFuncs, nOuts, Mask, nBits );    Cudd_Ref( bFunc );
-//Abc_NodeShowBddOne( dd, bFunc );
+/*
     // transfer to ADD
     aFunc = Abc_NtkBddToAdd( dd, bFunc, nOuts );                        Cudd_Ref( aFunc );
     Cudd_RecursiveDeref( dd, bFunc );
 //Abc_NodeShowBddOne( dd, aFunc );
+
     // perform reordering for BDD width
-    aFuncNew = Extra_Reorder( pReo, dd, aFunc, NULL );                  Cudd_Ref( aFuncNew );
-printf( "Before = %d.  After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNew) );
-//Abc_NodeShowBddOne( dd, aFuncNew );
+    if ( fReorder )
+    {
+        aFuncNew = Extra_Reorder( pReo, dd, aFunc, NULL );              Cudd_Ref( aFuncNew );
+        printf( "Before = %d.  After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNew) );
+        Cudd_RecursiveDeref( dd, aFunc );
+    }
+    else
+        aFuncNew = aFunc;
+
+    // get back to BDD
+    bFunc = Abc_NtkAddToBdd( dd, aFuncNew, nIns, nOuts );  Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( dd, aFuncNew );
-    Cudd_RecursiveDeref( dd, aFunc );
+//Abc_NodeShowBddOne( dd, bFunc );
     // print the result
 //    reoProfileWidthPrint( pReo );
+*/
+    Cudd_Deref( bFunc );
+    return bFunc;
 }
 
 /**Function*************************************************************
@@ -208,7 +915,7 @@ printf( "Before = %d.  After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNe
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkBddDecInt( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nOuts )
+DdNode * Abc_NtkBddDecInt( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nIns, int nOuts )
 {
 /*
     int i, k;
@@ -223,8 +930,53 @@ void Abc_NtkBddDecInt( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nOu
             }
     }
 */
-    Abc_NtkBddDecTry( pReo, dd, pFuncs, nOuts, ~(1<<(32-nOuts)), nOuts );
+    return Abc_NtkBddDecTry( pReo, dd, pFuncs, nIns, nOuts, ~(1<<(32-nOuts)), nOuts );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate Sasao's decomposition.]
+
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateFromCharFunc( Abc_Ntk_t * pNtk, DdManager * dd, DdNode * bFunc )
+{    
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pNode, * pNodeNew, * pNodePo;
+    int i;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    // create inputs for CIs
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
+        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
+        Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
+    }
+    // create inputs for COs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
+        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
+        Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
+    }
+    // transfer BDD
+    pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( pNodeNew->pData );
+    // transfer BDD into to be the local function
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pNodeNew );
+    Abc_ObjAssignName( pNodePo, "out", NULL );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateFromCharFunc(): Network check has failed.\n" );
+    return pNtkNew;
 }
 
 /**Function*************************************************************
@@ -238,14 +990,16 @@ void Abc_NtkBddDecInt( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nOu
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
 {
     int nBddSizeMax   = 1000000;
     int fDropInternal =       0;
     int fReorder      =       1;
+    Abc_Ntk_t * pNtkNew;
     reo_man * pReo;
     DdManager * dd;
     DdNode * pFuncs[BDD_FUNC_MAX];
+    DdNode * bFunc;
     Abc_Obj_t * pNode;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
@@ -254,29 +1008,37 @@ void Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
     if ( dd == NULL )
     {
         Abc_Print( -1, "Construction of global BDDs has failed.\n" );
-        return;
+        return NULL;
     }
+    // collect global BDDs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        pFuncs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
 
-    assert( dd->size == Abc_NtkCiNum(pNtk) );
     // create new variables at the bottom
+    assert( dd->size == Abc_NtkCiNum(pNtk) );
     for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ )
         Cudd_addNewVarAtLevel( dd, dd->size );
-    // create terminals of MTBDD
-//    for ( i = 0; i < (1 << Abc_NtkCoNum(pNtk)); i++ )
-//        Cudd_addConst( dd, i );
-    // collect global BDDs
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        pFuncs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
 
+    // prepare reordering engine
     pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
     Extra_ReorderSetMinimizationType( pReo, REO_MINIMIZE_WIDTH );
-//    Extra_ReorderSetVerification( pReo, 1 );
+    Extra_ReorderSetVerification( pReo, 1 );
     Extra_ReorderSetVerbosity( pReo, 1 );
 
-    Abc_NtkBddDecInt( pReo, dd, pFuncs, Abc_NtkCoNum(pNtk) );
+    // derive characteristic function
+    bFunc = Abc_NtkBddDecInt( pReo, dd, pFuncs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk) );  Cudd_Ref( bFunc );
     Extra_ReorderQuit( pReo );
 
+Abc_NtkExploreCofs( dd, bFunc, dd->vars, Abc_NtkCiNum(pNtk), 6 );
+
+    // create new network
+//    pNtkNew = Abc_NtkCreateFromCharFunc( pNtk, dd, bFunc );
+    pNtkNew = Abc_NtkDup( pNtk );
+
+    // cleanup
+    Cudd_RecursiveDeref( dd, bFunc );
     Abc_NtkFreeGlobalBdds( pNtk, 1 );
+    return pNtkNew;
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index c539b53e..6d62f330 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -40,6 +40,76 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Check if a LUT can absort a fanin.]
+
+  Description [The fanins are (c, d0, d1).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjCheckAbsorb( Abc_Obj_t * pObj, Abc_Obj_t * pPivot, int nLutSize, Vec_Ptr_t * vFanins )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pObj) && Abc_ObjIsNode(pPivot) );
+    // add fanins of the node
+    Vec_PtrClear( vFanins );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        if ( pFanin != pPivot )
+            Vec_PtrPush( vFanins, pFanin );
+    // add fanins of the fanin
+    Abc_ObjForEachFanin( pPivot, pFanin, i )
+    {
+        Vec_PtrPushUnique( vFanins, pFanin );
+        if ( Vec_PtrSize(vFanins) > nLutSize )
+            return 0;
+    }
+    return 1;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Check how many times a LUT can absorb a fanin.]
+
+  Description [The fanins are (c, d0, d1).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
+{
+    Vec_Int_t * vCounts;
+    Vec_Ptr_t * vFanins;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, Counter = 0, Counter2 = 0, clk = clock();
+    vCounts = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    vFanins = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    Abc_ObjForEachFanin( pObj, pFanin, k )
+        if ( Abc_ObjIsNode(pFanin) && Abc_ObjCheckAbsorb( pObj, pFanin, nLutSize, vFanins ) )
+        {
+            Vec_IntAddToEntry( vCounts, Abc_ObjId(pFanin), 1 );
+            Counter++;
+        }
+    Vec_PtrFree( vFanins );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( Vec_IntEntry(vCounts, Abc_ObjId(pObj)) == Abc_ObjFanoutNum(pObj) )
+        {
+//            printf( "%d ", Abc_ObjId(pObj) );
+            Counter2++;
+        }
+    printf( "Absorted = %6d. (%6.2f %%)   Fully = %6d. (%6.2f %%)  ", 
+        Counter,  100.0 * Counter  / Abc_NtkNodeNum(pNtk), 
+        Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Implements 2:1 MUX using one 3-LUT.]
 
   Description [The fanins are (c, d0, d1).]
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index 1d33c89e..1a1a81b2 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -1244,7 +1244,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
             continue;
         Cost = 1.0 * Vec_IntSize(vGlob)/(Vec_IntSize(vLeaves) + Vec_IntSize(vRoots));
         CostAll += Cost;
-        if ( Cost < 0.4 )
+        if ( Cost < 0.5 )
             continue;
 
         printf( "%6d : Root =%3d. Leaf =%3d. Node =%4d. ", 
@@ -1254,7 +1254,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
             printf( "%d ", Entry );
         printf( "\n" );
 
-        sprintf( pFileName, "%s_mffc%04d_%02d.blif", Abc_NtkName(pNtk), i, Vec_IntSize(vGlob) );
+        sprintf( pFileName, "%sc%04di%02dn%02d.blif", Abc_NtkName(pNtk), i, Vec_IntSize(vLeaves), Vec_IntSize(vGlob) );
         Abc_NktMffcPrintInt( pFileName, pNtk, vRoots, vGlob, vLeaves );
     }
     Vec_IntFree( vLeaves );
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index 06ccf9ca..8c414915 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -366,12 +366,12 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
+    extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars );
     extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
     DdManager * dd = (DdManager *)Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
-    bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
+    bFunc1 = Abc_ConvertSopToBdd( dd, pSop, NULL );    Cudd_Ref( bFunc1 );
     bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );   Cudd_Ref( bFunc2 );
 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
 //Extra_bddPrint( dd, bFunc2 ); printf("\n");