diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c84663fd9..543eb5f5c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10720,6 +10720,41 @@ static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes )
     pPerm[Pos] = 0;
     return pPerm;
 }
+static int Abc_TwoExactPermParseObj( char ** ppToken, int nVars, int nNodes, int * pObj )
+{
+    char * pToken = *ppToken;
+    if ( *pToken == '*' )
+    {
+        *pObj = -1;
+        *ppToken = pToken + 1;
+        return 1;
+    }
+    if ( *pToken >= 'a' && *pToken < 'a' + nVars )
+    {
+        *pObj = *pToken - 'a';
+        *ppToken = pToken + 1;
+        return 1;
+    }
+    if ( *pToken >= 'A' && *pToken <= 'Z' )
+    {
+        *pObj = nVars + *pToken - 'A';
+        *ppToken = pToken + 1;
+        return *pObj < nVars + nNodes;
+    }
+    if ( *pToken == 'N' )
+    {
+        char * pNext = pToken + 1;
+        int Num = 0;
+        if ( *pNext < '0' || *pNext > '9' )
+            return 0;
+        while ( *pNext >= '0' && *pNext <= '9' )
+            Num = 10 * Num + *pNext++ - '0';
+        *pObj = nVars + Num;
+        *ppToken = pNext;
+        return *pObj < nVars + nNodes;
+    }
+    return 0;
+}
 static int Abc_TwoExactPermAddDcs( int * pFans, int nVars, int nNodes, int nDcs, int nSkip, int fAll )
 {
     int i, k, nLetters = 0;
@@ -11164,15 +11199,19 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->pPermStr )
     {
-        int i, nEntries = 0;
-        for ( i = 0; pPars->pPermStr[i]; i++ )
+        char * pToken = pPars->pPermStr;
+        int nEntries = 0;
+        while ( *pToken )
         {
-            char Sym = pPars->pPermStr[i];
-            if ( Sym == '_' )
-                continue;
-            if ( Sym != '*' && (Sym < 'a' || Sym >= 'a' + pPars->nVars) )
+            int iObj = -1;
+            if ( *pToken == '_' )
             {
-                Abc_Print( -1, "Permutation symbol \"%c\" is not one of '*', '_' or input variables 'a' through '%c'.\n", Sym, 'a' + pPars->nVars - 1 );
+                pToken++;
+                continue;
+            }
+            if ( !Abc_TwoExactPermParseObj(&pToken, pPars->nVars, pPars->nNodes, &iObj) )
+            {
+                Abc_Print( -1, "Permutation should use '*', '_', input variables 'a' through '%c', or internal nodes 'A' through '%c'.\n", 'a' + pPars->nVars - 1, 'A' + Abc_MinInt(pPars->nNodes, 26) - 1 );
                 return 1;
             }
             nEntries++;
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index eadcd08ad..b5831e7ff 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -704,16 +704,42 @@ static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k )
 {
     char * pPermStr = p->pPars->pPermStr;
     int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1);
-    int nSeen = 0, s;
+    int nSeen = 0;
+    char * pToken;
     if ( p->pPars->pPermFans )
         return p->pPars->pPermFans[iTarget];
     assert( pPermStr != NULL );
-    for ( s = 0; pPermStr[s]; s++ )
+    for ( pToken = pPermStr; *pToken; )
     {
-        if ( pPermStr[s] == '_' )
+        int iObj = -2;
+        if ( *pToken == '_' )
+        {
+            pToken++;
             continue;
+        }
+        if ( *pToken == '*' )
+        {
+            iObj = -1;
+            pToken++;
+        }
+        else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars )
+            iObj = *pToken++ - 'a';
+        else if ( *pToken >= 'A' && *pToken <= 'Z' )
+            iObj = p->nVars + (*pToken++ - 'A');
+        else if ( *pToken == 'N' )
+        {
+            char * pNext = pToken + 1;
+            int Num = 0;
+            assert( *pNext >= '0' && *pNext <= '9' );
+            while ( *pNext >= '0' && *pNext <= '9' )
+                Num = 10 * Num + *pNext++ - '0';
+            iObj = p->nVars + Num;
+            pToken = pNext;
+        }
+        else
+            assert( 0 );
         if ( nSeen++ == iTarget )
-            return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
+            return iObj;
     }
     assert( 0 );
     return -1;
@@ -741,6 +767,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
 static void Exa_ManPrintPerm( Exa_Man_t * p )
 {
     int i, k, iVar;
+    char Name[16];
     printf( "The variable permutation is \"" );
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
@@ -749,7 +776,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p )
         for ( k = 1; k >= 0; k-- )
         {
             iVar = Exa_ManFindFanin( p, i, k );
-            printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
+            printf( "%s", Exa_ManObjName(p, iVar, Name) );
         }
     }
     printf( "\".\n" );
diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
index 87f3a6920..23ccb7217 100644
--- a/src/sat/bmc/bmcMaj2.c
+++ b/src/sat/bmc/bmcMaj2.c
@@ -719,16 +719,42 @@ static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k )
 {
     char * pPermStr = p->pPars->pPermStr;
     int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1);
-    int nSeen = 0, s;
+    int nSeen = 0;
+    char * pToken;
     if ( p->pPars->pPermFans )
         return p->pPars->pPermFans[iTarget];
     assert( pPermStr != NULL );
-    for ( s = 0; pPermStr[s]; s++ )
+    for ( pToken = pPermStr; *pToken; )
     {
-        if ( pPermStr[s] == '_' )
+        int iObj = -2;
+        if ( *pToken == '_' )
+        {
+            pToken++;
             continue;
+        }
+        if ( *pToken == '*' )
+        {
+            iObj = -1;
+            pToken++;
+        }
+        else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars )
+            iObj = *pToken++ - 'a';
+        else if ( *pToken >= 'A' && *pToken <= 'Z' )
+            iObj = p->nVars + (*pToken++ - 'A');
+        else if ( *pToken == 'N' )
+        {
+            char * pNext = pToken + 1;
+            int Num = 0;
+            assert( *pNext >= '0' && *pNext <= '9' );
+            while ( *pNext >= '0' && *pNext <= '9' )
+                Num = 10 * Num + *pNext++ - '0';
+            iObj = p->nVars + Num;
+            pToken = pNext;
+        }
+        else
+            assert( 0 );
         if ( nSeen++ == iTarget )
-            return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
+            return iObj;
     }
     assert( 0 );
     return -1;
@@ -756,6 +782,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
 static void Exa_ManPrintPerm( Exa_Man_t * p )
 {
     int i, k, iVar;
+    char Name[16];
     printf( "The variable permutation is \"" );
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
@@ -764,7 +791,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p )
         for ( k = 1; k >= 0; k-- )
         {
             iVar = Exa_ManFindFanin( p, i, k );
-            printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
+            printf( "%s", Exa_ManObjName(p, iVar, Name) );
         }
     }
     printf( "\".\n" );