diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c
index 6703c8ca8..873cea2eb 100644
--- a/src/aig/gia/giaClp.c
+++ b/src/aig/gia/giaClp.c
@@ -382,7 +382,7 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
         Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
-        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
+        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
         Vec_PtrFreeFree( vNamesCi );
         Vec_PtrFreeFree( vNamesCo );
     }
@@ -404,7 +404,7 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p )
     Gia_ManStop( pNew );
 }
 
-void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
+void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
 {
     DdManager * dd;
     Dsd_Manager_t * pManDsd;
@@ -432,7 +432,7 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
         Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
-        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
+        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet );
         Vec_PtrFreeFree( vNamesCi );
         Vec_PtrFreeFree( vNamesCo );
     }
@@ -448,7 +448,7 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
     return NULL;
 }
 
-void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose )
+void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
 {
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a1cf73d57..76ae22eb4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3311,15 +3311,15 @@ usage:
 ***********************************************************************/
 int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Abc_Obj_t * pNode;
-    int c, fCompl = 0, fGlobal = 0, fReorder = 1;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Abc_Obj_t * pNode;
+    int c, fCompl = 0, fGlobal = 0, fReorder = 1, fWidth = 0;
     extern void Abc_NodeShowBdd( Abc_Obj_t * pNode, int fCompl );
     extern void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl, int fReorder );
+    extern void Abc_NtkBddDecExplore( Abc_Obj_t * pNode );
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cgrh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cgrwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3332,6 +3332,9 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReorder ^= 1;
             break;
+        case 'w':
+            fWidth ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -3343,7 +3346,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Print( -1, "Empty network.\n" );
         return 1;
-    }
+    }    
 
     if ( fGlobal )
     {
@@ -3358,7 +3361,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Print( -1, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
         return 1;
-    }
+    }    
     if ( argc > globalUtilOptind + 1 )
     {
         Abc_Print( -1, "Wrong number of auguments.\n" );
@@ -3382,11 +3385,14 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
     }
-    Abc_NodeShowBdd( pNode, fCompl );
+    if ( fWidth )
+        Abc_NtkBddDecExplore( pNode );
+    else
+        Abc_NodeShowBdd( pNode, fCompl );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: show_bdd [-cgrh] <node>\n" );
+    Abc_Print( -2, "usage: show_bdd [-cgrwh] <node>\n" );
     Abc_Print( -2, "       uses DOT and GSVIEW to visualize the global BDDs of primary outputs\n" );
     Abc_Print( -2, "       in terms of primary inputs or the local BDD of a node in terms of its fanins\n" );
 #ifdef WIN32
@@ -3397,6 +3403,7 @@ usage:
     Abc_Print( -2, "\t-c    : toggle visualizing BDD with complemented edges [default = %s].\n", fCompl? "yes": "no" );
     Abc_Print( -2, "\t-g    : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" );
     Abc_Print( -2, "\t-r    : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
+    Abc_Print( -2, "\t-w    : toggles printing width profile of the node's BDD [default = %s]\n", fWidth? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -53855,10 +53862,10 @@ usage:
 int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManPrintDsdMatrix( Gia_Man_t * p, int iIn );
-    extern void Gia_ManCheckDsd( Gia_Man_t * p, int fVerbose );
-    int c, iIn = -1, fDsd = 0, fVerbose = 0;
+    extern void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose );
+    int c, iIn = -1, fDsd = 0, fAll = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Vdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Vdavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -53876,6 +53883,9 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDsd ^= 1;
             break;            
+        case 'a':
+            fAll ^= 1;
+            break;            
         case 'v':
             fVerbose ^= 1;
             break;
@@ -53893,13 +53903,31 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fDsd ) 
     {
         if ( iIn == -1 ) {
-            Gia_ManCheckDsd( pAbc->pGia, 1 );
+            Gia_ManCheckDsd( pAbc->pGia, 0, 1 );
+            if ( fAll ) {
+                for ( iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
+                    for ( c = 0; c < 2; c++ ) {
+                        Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
+                        printf( "%s %2d = %d:\n", c ? "   " : "Var", iIn, c );
+                        Gia_ManCheckDsd( pTemp, 12, 1 );
+                        Gia_ManStop( pTemp );
+                    }                
+            }
             return 0;
         }
         for ( c = 0; c < 2; c++ ) {
             Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
             printf( "Var %2d  Cof %d:\n", iIn, c );
-            Gia_ManCheckDsd(  pTemp, 1 );
+            Gia_ManCheckDsd( pTemp, 0, 1 );
+            if ( fAll ) {
+                for ( int iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
+                    for ( int c = 0; c < 2; c++ ) {
+                        Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn, c );
+                        printf( "%s %2d = %d:\n", c ? "   " : "Var", iIn, c );
+                        Gia_ManCheckDsd( pTemp2, 12, 1 );
+                        Gia_ManStop( pTemp2 );
+                    }
+            }
             Gia_ManStop( pTemp );
         }
         return 0;
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 27d86ae89..6820f1806 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -143,7 +143,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
         ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
         ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
         if ( fVerbose )
-            Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+            Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1, 0 );
         else
             Dsd_TreePrint2( stdout, pManDsd, ppNamesCi, ppNamesCo, -1 );
         ABC_FREE( ppNamesCi );
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 49681ae90..883a56904 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -585,30 +585,36 @@ Abc_Obj_t * Abc_NtkBddFindCofactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkBddDecExploreOne( DdManager * dd, DdNode * bFunc, int nLutSize )
+void Abc_NtkBddDecExploreOne( DdManager * dd, DdNode * bFunc, int iOrder )
 {
     DdManager * ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    int i, * pProfile = ABC_CALLOC( int, dd->size + 100 );
     Cudd_AutodynEnable( ddNew,  CUDD_REORDER_SYMM_SIFT );
-    Vec_Int_t * vPerm = Vec_IntStartNatural( dd->size );
-    Vec_IntRandomizeOrder( vPerm );
+    Vec_Int_t * vPerm = Vec_IntStartNatural( dd->size ); if ( iOrder ) Vec_IntRandomizeOrder( vPerm );
     DdNode * bFuncNew = Extra_TransferPermute( dd, ddNew, bFunc, Vec_IntArray(vPerm) ); Cudd_Ref(bFuncNew);
-    Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
-    Vec_Ptr_t * vCofs = Abc_NtkBddCofactors( ddNew, bFuncNew, nLutSize );
-    Vec_Ptr_t * vUniq = Vec_PtrDup( vCofs );
-    Vec_PtrUniqify( vUniq, (int (*)(const void *, const void *))Vec_PtrSortCompare );
-    printf( "%d  ", Vec_PtrSize(vUniq) );
-    Cudd_RecursiveDeref( dd, bFuncNew );
-    Cudd_Quit( ddNew );
+    if ( iOrder ) Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
     Vec_IntFree( vPerm );
-    Vec_PtrFree( vCofs );
-    Vec_PtrFree( vUniq );
-}
-void Abc_NtkBddDecExplore( DdManager * dd, DdNode * bFunc, int nLutSize )
-{
-    Abc_Random(1);
-    for ( int i = 0; i < 32; i++ )
-        Abc_NtkBddDecExploreOne( dd, bFunc, nLutSize );
+    DdNode * aFuncNew = Cudd_BddToAdd( ddNew, bFuncNew ); Cudd_Ref( aFuncNew );
+    Extra_ProfileWidth( ddNew, aFuncNew, pProfile, -1 );
+    if ( iOrder )
+        printf( "Random order %d:\n", iOrder );
+    else
+        printf( "Natural order:\n" );
+    for ( i = 0; i <= dd->size; i++ )
+        printf( " %d=%d(%d)[%d]", i, pProfile[i], i-Abc_Base2Log(pProfile[i]), ddNew->perm[i] );
     printf( "\n" );
+    Cudd_RecursiveDeref( ddNew, aFuncNew );
+    Cudd_RecursiveDeref( ddNew, bFuncNew );
+    Cudd_Quit( ddNew );
+}
+void Abc_NtkBddDecExplore( Abc_Obj_t * pNode )
+{
+    DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
+    DdNode * bFunc = (DdNode *)pNode->pData;
+    int i; Abc_Random(1);
+    if ( Abc_ObjIsNode(pNode) )
+        for ( i = 0; i < 16; i++ )
+            Abc_NtkBddDecExploreOne( dd, bFunc, i );
 }
 
 /**Function*************************************************************
@@ -645,8 +651,6 @@ Abc_Obj_t * Abc_NtkBddDecompose( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLu
         }
 
     }
-    //if ( dd->size == Abc_ObjFaninNum(pNode) )
-    //Abc_NtkBddDecExplore( dd, (DdNode *)pNode->pData, nLutSize );
     // cofactor w.r.t. the bound set variables
     vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, nLutSize );
     vUniq = Vec_PtrDup( vCofs );
@@ -813,6 +817,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int
 #else
 
 Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int fVerbose ) { return NULL; }
+void Abc_NtkBddDecExplore( Abc_Obj_t * pNode ) {}
 
 #endif
 
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 4c5cd8915..2990c0259 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -115,7 +115,7 @@ extern int             Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot );
 extern int             Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
-extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
+extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet );
 extern void            Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output );
 extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
 /*=== dsdLocal.c =======================================================*/
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 9b9dd2121..42eee2cc5 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -638,7 +638,7 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in
   SeeAlso     []
 
 ***********************************************************************/
-void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output )
+void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet )
 {
     Dsd_Node_t * pNode;
     int SigCounter;
@@ -650,14 +650,14 @@ void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[],
         for ( i = 0; i < pDsdMan->nRoots; i++ )
         {
             pNode = Dsd_Regular( pDsdMan->pRoots[i] );
-            Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames );
+            Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], OffSet, &SigCounter, fShortNames );
         }
     }
     else
     {
         assert( Output >= 0 && Output < pDsdMan->nRoots );
         pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
-        Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames );
+        Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], OffSet, &SigCounter, fShortNames );
     }
 }
 
@@ -686,7 +686,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
     if ( !fComp )
         fprintf( pFile, "%s = ", pOutputName );
     else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
+        fprintf( pFile, "~%s = ", pOutputName );
     pInputNums = ABC_ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
@@ -711,7 +711,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( i )
                 fprintf( pFile, "," );
             if ( fCompNew )
-                fprintf( pFile, " NOT(" );
+                fprintf( pFile, " ~" );
             else
                 fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
@@ -727,8 +727,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, "<%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
+            //if ( fCompNew )
+            //    fprintf( pFile, "" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -751,7 +751,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( i )
                 fprintf( pFile, "," );
             if ( fCompNew )
-                fprintf( pFile, " NOT(" );
+                fprintf( pFile, " ~" );
             else
                 fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
@@ -767,8 +767,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, "<%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
+            //if ( fCompNew )
+            //    fprintf( pFile, "" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -791,7 +791,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( i )
                 fprintf( pFile, "," );
             if ( fCompNew )
-                fprintf( pFile, " NOT(" );
+                fprintf( pFile, " ~" );
             else
                 fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
@@ -807,8 +807,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, "<%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
+            //if ( fCompNew )
+            //    fprintf( pFile, "" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -979,7 +979,7 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
     if ( !fComp )
         fprintf( pFile, "%s = ", pOutputName );
     else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
+        fprintf( pFile, "~%s = ", pOutputName );
     pInputNums = ABC_ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {