diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1d4bde4d7..b23905dd3 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -755,6 +755,7 @@ extern ABC_DLL void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCharNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkCleanNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkStartNameIds( Abc_Ntk_t * p );
 extern ABC_DLL void               Abc_NtkTransferNameIds( Abc_Ntk_t * p, Abc_Ntk_t * pNew );
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index dec5f01e0..b3910236e 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -125,6 +125,12 @@ char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
     sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
     return Buffer;
 }
+char * Abc_ObjNameChar( int Num, int fCap )
+{
+    static char Buffer[2000];
+    sprintf( Buffer, "%c", (fCap ? 'A':'a') + Num );
+    return Buffer;
+}
 
 /**Function*************************************************************
 
@@ -494,6 +500,12 @@ void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_ObjAssignName( pObj, Abc_ObjNameDummy("pi", i, nDigits), NULL );
 }
+void Abc_NtkAddCharPiNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_ObjAssignName( pObj, Abc_ObjNameChar(i, 0), NULL );
+}
 
 /**Function*************************************************************
 
@@ -514,6 +526,12 @@ void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_ObjAssignName( pObj, Abc_ObjNameDummy("po", i, nDigits), NULL );
 }
+void Abc_NtkAddCharPoNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAssignName( pObj, Abc_ObjNameChar(i, 1), NULL );
+}
 
 /**Function*************************************************************
 
@@ -606,6 +624,14 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
     Abc_NtkAddDummyPoNames( pNtk );
     Abc_NtkAddDummyBoxNames( pNtk );
 }
+void Abc_NtkCharNames( Abc_Ntk_t * pNtk )
+{
+    Nm_ManFree( pNtk->pManName );
+    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) + Abc_NtkBoxNum(pNtk) );
+    Abc_NtkAddCharPiNames( pNtk );
+    Abc_NtkAddCharPoNames( pNtk );
+    Abc_NtkAddDummyBoxNames( pNtk );
+}
 void Abc_NtkCleanNames( Abc_Ntk_t * pNtk )
 {  
     Abc_Obj_t * pObj; int i;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index c4dbb36ee..1477c3cc4 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -96,6 +96,52 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan
     pNtk->AndGateDelay = 0.0;
     return pNtk;
 }
+Abc_Ntk_t * Abc_NtkAllocBdd( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan, int nVars )
+{
+    Abc_Ntk_t * pNtk;
+    pNtk = ABC_ALLOC( Abc_Ntk_t, 1 );
+    memset( pNtk, 0, sizeof(Abc_Ntk_t) );
+    pNtk->ntkType     = Type;
+    pNtk->ntkFunc     = Func;
+    // start the object storage
+    pNtk->vObjs       = Vec_PtrAlloc( 100 );
+    pNtk->vPios       = Vec_PtrAlloc( 100 );
+    pNtk->vPis        = Vec_PtrAlloc( 100 );
+    pNtk->vPos        = Vec_PtrAlloc( 100 );
+    pNtk->vCis        = Vec_PtrAlloc( 100 );
+    pNtk->vCos        = Vec_PtrAlloc( 100 );
+    pNtk->vBoxes      = Vec_PtrAlloc( 100 );
+    pNtk->vLtlProperties = Vec_PtrAlloc( 100 );
+    // start the memory managers
+    pNtk->pMmObj      = fUseMemMan? Mem_FixedStart( sizeof(Abc_Obj_t) ) : NULL;
+    pNtk->pMmStep     = fUseMemMan? Mem_StepStart( ABC_NUM_STEPS ) : NULL;
+    // get ready to assign the first Obj ID
+    pNtk->nTravIds    = 1;
+    // start the functionality manager
+    if ( !Abc_NtkIsStrash(pNtk) )
+        Vec_PtrPush( pNtk->vObjs, NULL );
+    if ( Abc_NtkIsStrash(pNtk) )
+        pNtk->pManFunc = Abc_AigAlloc( pNtk );
+    else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
+        pNtk->pManFunc = Mem_FlexStart();
+#ifdef ABC_USE_CUDD
+    else if ( Abc_NtkHasBdd(pNtk) )
+        pNtk->pManFunc = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+#endif
+    else if ( Abc_NtkHasAig(pNtk) )
+        pNtk->pManFunc = Hop_ManStart();
+    else if ( Abc_NtkHasMapping(pNtk) )
+        pNtk->pManFunc = Abc_FrameReadLibGen();
+    else if ( !Abc_NtkHasBlackbox(pNtk) )
+        assert( 0 );
+    // name manager
+    pNtk->pManName = Nm_ManCreate( 200 );
+    // attribute manager
+    pNtk->vAttrs = Vec_PtrStart( VEC_ATTR_TOTAL_NUM );
+    // estimated AndGateDelay
+    pNtk->AndGateDelay = 0.0;
+    return pNtk;
+}
 
 /**Function*************************************************************
 
@@ -118,7 +164,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
     // decide whether to copy the names
     fCopyNames = ( Type != ABC_NTK_NETLIST );
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
+    pNtkNew = Func == ABC_FUNC_BDD ? Abc_NtkAllocBdd( Type, Func, 1, Abc_NtkCiNum(pNtk) ) : Abc_NtkAlloc( Type, Func, 1 );
     pNtkNew->nConstrs   = pNtk->nConstrs;
     pNtkNew->nBarBufs   = pNtk->nBarBufs;
     // duplicate the name and the spec
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 47a4aef6c..8dc00865e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14151,13 +14151,16 @@ usage:
 int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c, fKeepIo = 0;
+    int c, fKeepIo = 0, fAlpha = 0;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "kh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "akh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAlpha ^= 1;
+            break;
         case 'k':
             fKeepIo ^= 1;
             break;
@@ -14173,15 +14176,18 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( fKeepIo )
+    if ( fAlpha )
+        Abc_NtkCharNames( pNtk );
+    else if ( fKeepIo )
         Abc_NtkCleanNames( pNtk );
     else
         Abc_NtkShortNames( pNtk );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: short_names [-kh]\n" );
+    Abc_Print( -2, "usage: short_names [-akh]\n" );
     Abc_Print( -2, "\t         replaces PI/PO/latch names by short char strings\n" );
+    Abc_Print( -2, "\t-a     : toggle using simple character names for PIs/POs [default = %s]\n", fAlpha? "yes": "no" );
     Abc_Print( -2, "\t-k     : toggle keeping PI/PO names unchanged [default = %s]\n", fKeepIo? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 9b5b98881..d47ca8785 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -585,35 +585,42 @@ Abc_Obj_t * Abc_NtkBddFindCofactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkBddTestProfile( DdManager * dd, DdNode * aFunc )
+{
+}
 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 ); if ( iOrder ) Vec_IntRandomizeOrder( vPerm );
+    Vec_Int_t * vPermInv = Vec_IntInvert( vPerm, -1 );
     DdNode * bFuncNew = Extra_TransferPermute( dd, ddNew, bFunc, Vec_IntArray(vPerm) ); Cudd_Ref(bFuncNew);
     if ( iOrder ) Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
     Vec_IntFree( vPerm );
     DdNode * aFuncNew = Cudd_BddToAdd( ddNew, bFuncNew ); Cudd_Ref( aFuncNew );
-    Extra_ProfileWidth( ddNew, aFuncNew, pProfile, -1 );
+    //Extra_ProfileWidth( ddNew, aFuncNew, pProfile, -1 );
     if ( iOrder )
-        printf( "Random order %d:\n", iOrder );
+        printf( "Random order %2d: ", 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( "Natural order:   " );
+    printf( "BDD size = %3d  ", Cudd_DagSize(aFuncNew) );
+    for ( i = 0; i < dd->size; i++ )
+        printf( " %c", 'a' + Vec_IntEntry(vPermInv, ddNew->invperm[i]) );
     printf( "\n" );
     Cudd_RecursiveDeref( ddNew, aFuncNew );
     Cudd_RecursiveDeref( ddNew, bFuncNew );
     Cudd_Quit( ddNew );
+    ABC_FREE( pProfile );
 }
 void Abc_NtkBddDecExplore( Abc_Obj_t * pNode )
 {
     DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
     DdNode * bFunc = (DdNode *)pNode->pData;
+    printf( "DD size = %d\n", dd->size );
     int i; Abc_Random(1);
     if ( Abc_ObjIsNode(pNode) )
-        for ( i = 0; i < 16; i++ )
+        for ( i = 0; i < 32; i++ )
             Abc_NtkBddDecExploreOne( dd, bFunc, i );
 }
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 0676a7d0e..1eff9d581 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -433,7 +433,8 @@ void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInter
 //        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
         Cudd_AutodynDisable( dd );
     }
-//    Cudd_PrintInfo( dd, stdout );
+    if ( fVerbose )
+        Cudd_PrintInfo( dd, stdout );
     return dd;
 }