diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fd1c2c8b2..669632be2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10768,7 +10768,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmpvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10896,6 +10896,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMinNodes ^= 1;
             break;
+        case 'p':
+            pPars->fUsePerm ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -10945,15 +10948,31 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize );
         return 1;
     }
-    if ( pPars->nVars > 12 )
+    if ( pPars->fKissat )
     {
-        Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
-        return 1;
+        if ( pPars->nVars > 14 )
+        {
+            Abc_Print( -1, "Function should not have more than 14 inputs.\n" );
+            return 1;
+        }
+        if ( pPars->nLutSize > 8 )
+        {
+            Abc_Print( -1, "Node size should not be more than 8 inputs.\n" );
+            return 1;
+        }
     }
-    if ( pPars->nLutSize > 6 )
+    else
     {
-        Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
-        return 1;
+        if ( pPars->nVars > 12 )
+        {
+            Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
+            return 1;
+        }
+        if ( pPars->nLutSize > 6 )
+        {
+            Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
+            return 1;
+        }
     }
     if ( pPars->nRandFuncs ) {
         pPars->fGlucose = 1;
@@ -10972,7 +10991,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <hex>\n" );
+    Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmpvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of I-input function using N K-input gates\n" );
     Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
     Abc_Print( -2, "\t-M <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
@@ -10994,6 +11013,7 @@ usage:
     Abc_Print( -2, "\t-d       : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
     Abc_Print( -2, "\t-s       : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
     Abc_Print( -2, "\t-m       : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
+    Abc_Print( -2, "\t-p       : toggle use specialized permutation when minimizing nodes [default = %s]\n", pPars->fUsePerm ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
     Abc_Print( -2, "\t<hex>    : truth table in hex notation\n" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 374945039..3b591bb4e 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -68,6 +68,7 @@ struct Bmc_EsPar_t_
     int        fLutCascade;
     int        fLutInFixed;
     int        fMinNodes;
+    int        fUsePerm;
     int        RuntimeLim;
     int        nRandFuncs;
     int        nMintNum;
diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c
index 4a96af84e..5f291c20a 100644
--- a/src/sat/bmc/bmcMaj8.c
+++ b/src/sat/bmc/bmcMaj8.c
@@ -47,6 +47,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 #define MAJ_NOBJS  64 // Const0 + Const1 + nVars + nNodes
+#define MAJ_MAX_LUT 8
 
 typedef struct Exa8_Man_t_ Exa8_Man_t;
 struct Exa8_Man_t_ 
@@ -63,7 +64,7 @@ struct Exa8_Man_t_
     Vec_Wrd_t *       vInfo;     // nVars + nNodes + 1
     Vec_Bit_t *       vUsed2;    // bit masks
     Vec_Bit_t *       vUsed3;    // bit masks
-    int               VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
+    int               VarMarks[MAJ_NOBJS][MAJ_MAX_LUT][MAJ_NOBJS]; // variable marks
     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
     Vec_Wec_t *       vOutLits;  // output vars
     Vec_Wec_t *       vInVars;   // input vars
@@ -214,6 +215,7 @@ static int Exa8_ManMarkup( Exa8_Man_t * p )
 {
     int i, k, j;
     assert( p->nObjs <= MAJ_NOBJS );
+    assert( p->nLutSize <= MAJ_MAX_LUT );
     // assign functionality variables
     p->iVar = 1 + p->LutMask * p->nNodes;
     // assign connectivity variables
@@ -347,7 +349,7 @@ static inline int Exa8_ManFindFanin( Exa8_Man_t * p, int i, int k )
 static inline int Exa8_ManEval( Exa8_Man_t * p )
 {
     static int Flag = 0;
-    int i, k, j, iMint; word * pFanins[6];
+    int i, k, j, iMint; word * pFanins[MAJ_MAX_LUT];
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
         int iVarStart = 1 + p->LutMask*(i - p->nVars);
@@ -678,7 +680,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
     abctime clkTotal = Abc_Clock();
     Exa8_Man_t * p; 
     int fCompl = 0;
-    word pTruth[64]; 
+    assert( pPars->nVars <= 14 );
+    assert( pPars->nLutSize <= 8 );
+    int nTruthWords = Abc_TtWordNum( pPars->nVars );
+    word * pTruth = ABC_CALLOC( word, nTruthWords );
+    assert( pTruth );
     if ( pPars->pSymStr ) {
         word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
         pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
@@ -689,8 +695,6 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
     if ( pPars->pTtStr )
         Abc_TtReadHex( pTruth, pPars->pTtStr );
     else assert( 0 );
-    assert( pPars->nVars <= 12 );
-    assert( pPars->nLutSize <= 6 );
     if ( pPars->fUseIncr && !pPars->fSilent )
         printf( "Warning: Ignoring incremental option when using Kissat.\n" );
     pPars->fUseIncr = 0;
@@ -758,6 +762,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
     if ( pPars->pSymStr ) 
         ABC_FREE( pPars->pTtStr );
     Exa8_ManFree( p );
+    ABC_FREE( pTruth );
     return Res;
 }
 
@@ -770,7 +775,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
     for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
         printf( "\nTrying M = %d:\n", n );
         pPars->nNodes = n;
-        if ( fGenPerm ) {
+        if ( !pPars->fUsePerm && fGenPerm ) {
             Vec_Str_t * vStr = Vec_StrAlloc( 100 );
             for ( int v = 0; v < pPars->nLutSize; v++ )
                 Vec_StrPush( vStr, 'a'+v );
@@ -790,7 +795,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
             pPars->pPermStr = Vec_StrReleaseArray(vStr);
             Vec_StrFree( vStr );
         }
-        if ( 0 && fGenPerm ) {
+        else if ( pPars->fUsePerm && fGenPerm ) {
             Vec_Str_t * vStr = Vec_StrAlloc( 100 );
             for ( int v = 0; v < pPars->nLutSize; v++ )
                 Vec_StrPush( vStr, 'a'+v );