Improvements to the NPN semi-canonical form computation package.

9 files changed, 609 insertions, 133 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3b6c2c00..01b24e3e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4866,17 +4866,18 @@ int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: testnpn [-A <num>] [-vh] <file_name>\n" );
-    Abc_Print( -2, "\t           testbench for computing semi-canonical forms of Boolean functions\n" );
+    Abc_Print( -2, "usage: testnpn [-A <num>] [-vh] <file>\n" );
+    Abc_Print( -2, "\t           testbench for computing (semi-)canonical forms\n" );
+    Abc_Print( -2, "\t           of completely-specified Boolean functions up to 16 varibles\n" );
     Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
-    Abc_Print( -2, "\t               0: none (reading and writing the file)\n" );
-    Abc_Print( -2, "\t               1: exact canonical form (works only for 6 variables)\n" );
+    Abc_Print( -2, "\t               0: uniqifying truth tables\n" );
+    Abc_Print( -2, "\t               1: exact NPN canonical form by brute-force enumeration\n" );
     Abc_Print( -2, "\t               2: semi-canonical form by counting 1s in cofactors\n" );
-    Abc_Print( -2, "\t               3: semi-canonical form by minimizing truth table value\n" );
-    Abc_Print( -2, "\t               4: hybrid semi-canonical form (works only for 6 variables)\n" );
-    Abc_Print( -2, "\t               5: Jake's hybrid semi-canonical form (works up to 16 variables)\n" );
+    Abc_Print( -2, "\t               3: Jake's hybrid semi-canonical form (fast)\n" );
+    Abc_Print( -2, "\t               4: Jake's hybrid semi-canonical form (high-effort)\n" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
+    Abc_Print( -2, "\t<file>   : the text file with truth tables in hexadecimal, listed one per line\n");
     return 1;
 } 
 
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index e8c9168d..c1cb4ae0 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -66,9 +66,66 @@ extern void            Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p );
   SeeAlso     []
 
 ***********************************************************************/
+// returns hash key of the truth table
+static inline int Abc_TruthHashKey( word * pFunc, int nWords, int nTableSize )
+{
+    static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
+    int w;
+    word Key = 0;
+    for ( w = 0; w < nWords; w++ )
+        Key += pFunc[w] * s_BigPrimes[w % 7];
+    return (int)(Key % nTableSize);
+}
+// returns 1 if the entry with this truth table exits
+static inline int Abc_TruthHashLookup( word ** pFuncs, int iThis, int nWords, int * pTable, int * pNexts, int Key )
+{
+    int iThat;
+    for ( iThat = pTable[Key]; iThat != -1; iThat = pNexts[iThat] )
+        if ( !memcmp( pFuncs[iThat], pFuncs[iThis], sizeof(word) * nWords ) )
+            return 1;
+    return 0;
+}
+// hashes truth tables and collects unique ones
+int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
+{
+    // allocate hash table
+    int nTableSize = Abc_PrimeCudd(p->nFuncs);
+    int * pTable = ABC_FALLOC( int, nTableSize );
+    int * pNexts = ABC_FALLOC( int, nTableSize );
+    // hash functions
+    int i, k, Key;
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        Key = Abc_TruthHashKey( p->pFuncs[i], p->nWords, nTableSize );
+        if ( Abc_TruthHashLookup( p->pFuncs, i, p->nWords, pTable, pNexts, Key ) ) // found equal
+            p->pFuncs[i] = NULL;
+        else // there is no equal (the first time this one occurs so far)
+            pNexts[i] = pTable[Key], pTable[Key] = i;
+    }
+    ABC_FREE( pTable );
+    ABC_FREE( pNexts );
+    // count the number of unqiue functions
+    assert( p->pFuncs[0] != NULL );
+    for ( i = k = 1; i < p->nFuncs; i++ )
+        if ( p->pFuncs[i] != NULL )
+            p->pFuncs[k++] = p->pFuncs[i];
+    return (p->nFuncs = k);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of unique truth tables.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
 int nWords = 0; // unfortunate global variable
 int Abc_TruthCompare( word ** p1, word ** p2 ) { return memcmp(*p1, *p2, sizeof(word) * nWords); }
-int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
+int Abc_TruthNpnCountUniqueSort( Abc_TtStore_t * p )
 {
     int i, k;
     // sort them by value
@@ -116,28 +173,27 @@ void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
 void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
 {
     unsigned pAux[2048];
-    char pCanonPerm[32];
+    word pAuxWord[1024], pAuxWord1[1024];
+    char pCanonPerm[16];
     unsigned uCanonPhase=0;
     clock_t clk = clock();
-    int i;
+    int i, maxCtr=0;
 
     char * pAlgoName = NULL;
     if ( NpnType == 0 )
-        pAlgoName = "uniqifying       ";
+        pAlgoName = "uniqifying         ";
     else if ( NpnType == 1 )
-        pAlgoName = "exact NPN        ";
+        pAlgoName = "exact NPN          ";
     else if ( NpnType == 2 )
-        pAlgoName = "counting 1s      ";
+        pAlgoName = "counting 1s        ";
     else if ( NpnType == 3 )
-        pAlgoName = "minimizing TT    ";
+        pAlgoName = "Jake's hybrid fast ";
     else if ( NpnType == 4 )
-        pAlgoName = "hybrid NPN       ";
-    else if ( NpnType == 5 )
-        pAlgoName = "Jake's hybrid NPN";
+        pAlgoName = "Jake's hybrid good ";
 
     assert( p->nVars <= 16 );
     if ( pAlgoName )
-        printf( "Applying %-10s to %8d func%s of %2d vars...  ",  
+        printf( "Applying %-20s to %8d func%s of %2d vars...  ",  
             pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
     if ( fVerbose )
         printf( "\n" );
@@ -154,23 +210,18 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
     }
     else if ( NpnType == 1 )
     {
-        int * pComp = Extra_GreyCodeSchedule( p->nVars );
-        int * pPerm = Extra_PermSchedule( p->nVars );
-        if ( p->nVars == 6 )
+        permInfo* pi; 
+        Abc_TruthNpnCountUnique(p);
+        pi = setPermInfoPtr(p->nVars);
+        for ( i = 0; i < p->nFuncs; i++ )
         {
-            for ( i = 0; i < p->nFuncs; i++ )
-            {
-                if ( fVerbose )
-                    printf( "%7d : ", i );
-                *((word *)p->pFuncs[i]) = Extra_Truth6MinimumExact( *((word *)p->pFuncs[i]), pComp, pPerm );
-                if ( fVerbose )
-                    Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
-            }
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            simpleMinimal(p->pFuncs[i], pAuxWord, pAuxWord1, pi, p->nVars);
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
         }
-        else
-            printf( "This feature only works for 6-variable functions.\n" );
-        ABC_FREE( pComp );
-        ABC_FREE( pPerm );
+        freePermInfoPtr(pi);
     }
     else if ( NpnType == 2 )
     {
@@ -191,43 +242,24 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
             if ( fVerbose )
                 printf( "%7d : ", i );
             resetPCanonPermArray(pCanonPerm, p->nVars);
-            uCanonPhase = Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
+            uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
             if ( fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
         }
     }
     else if ( NpnType == 4 )
     {
-        if ( p->nVars == 6 )
-        {
-            for ( i = 0; i < p->nFuncs; i++ )
-            {
-                if ( fVerbose )
-                    printf( "%7d : ", i );
-                resetPCanonPermArray(pCanonPerm, p->nVars);
-                Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
-                *((word *)p->pFuncs[i]) = Extra_Truth6MinimumHeuristic( *((word *)p->pFuncs[i]) );
-                if ( fVerbose )
-                    Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
-            }
-        }
-        else
-            printf( "This feature only works for 6-variable functions.\n" );
-    }
-    else if ( NpnType == 5 )
-    {
         for ( i = 0; i < p->nFuncs; i++ )
         {
             if ( fVerbose )
                 printf( "%7d : ", i );
             resetPCanonPermArray(pCanonPerm, p->nVars);
-            uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
+            uCanonPhase = luckyCanonicizer_final_fast1( p->pFuncs[i], p->nVars, pCanonPerm );
             if ( fVerbose )
                 Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
         }
     }
     else assert( 0 );
-
     clk = clock() - clk;
     printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
     Abc_PrintTime( 1, "Time", clk );
@@ -284,7 +316,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose )
 {
     if ( fVerbose )
         printf( "Using truth tables from file \"%s\"...\n", pFileName );
-    if ( NpnType >= 0 && NpnType <= 5 )
+    if ( NpnType >= 0 && NpnType <= 4 )
         Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
     else
         printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/bool/lucky/lucky.h b/src/bool/lucky/lucky.h
index 0a055b40..fac24aeb 100644
--- a/src/bool/lucky/lucky.h
+++ b/src/bool/lucky/lucky.h
@@ -20,9 +20,24 @@
 
 ABC_NAMESPACE_HEADER_START
 
+typedef struct
+{
+    int varN;
+    int* swapArray;
+    int swapCtr;
+    int totalSwaps;
+    int* flipArray;
+    int flipCtr;
+    int totalFlips; 
+}permInfo;
+
 extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
-extern int      luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
-extern void     resetPCanonPermArray(char* x, int nVars); 
+extern unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
+extern unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm );
+extern void resetPCanonPermArray(char* x, int nVars); 
+extern permInfo* setPermInfoPtr(int var);
+extern void freePermInfoPtr(permInfo* x);
+extern void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/bool/lucky/luckyFast16.c b/src/bool/lucky/luckyFast16.c
index ebeeab1b..83a64b11 100644
--- a/src/bool/lucky/luckyFast16.c
+++ b/src/bool/lucky/luckyFast16.c
@@ -15,7 +15,7 @@
 ***********************************************************************/
 
 #include "luckyInt.h"
-
+//#define LUCKY_VERIFY
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,6 +27,48 @@ static word SFmask[5][4] = {
     {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}   
 };
 
+// we need next two functions only for verification of lucky method in debugging mode 
+void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
+{
+    int Temp;
+    swap_ij(pAfter, nVars, iVarInPosition, jVar);
+    
+    Temp = pCanonPerm[iVarInPosition];
+    pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
+    pCanonPerm[jVar] = Temp;
+    
+    if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
+    {
+        *pUCanonPhase ^= (1 << iVarInPosition);
+        *pUCanonPhase ^= (1 << jVar);
+    }
+    if((*pUCanonPhase>>iVarInPosition) & 1)
+        Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
+    
+}
+int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
+{
+    int i,j;
+    char tempChar;
+    for(j=0;j<nVars;j++)
+    {
+        tempChar = 'a'+ j;
+        for(i=j;i<nVars;i++)
+        {
+            if(tempChar != pCanonPerm[i])
+                continue;
+            swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
+            break;
+        }
+    }
+    if((uCanonPhase>>nVars) & 1)
+        Kit_TruthNot_64bit(pAfter, nVars );
+    if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
+        return 0;
+    else
+        return 1;
+}
+
 ////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
 
 // there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
@@ -203,6 +245,13 @@ inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, i
         }
     }
 }
+
+inline void minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int DifStart1;
+    if(minTemp1_fast(pInOut, iVar, nWords, &DifStart1) == 2)
+        arrangeQuoters_superFast_lessThen5(pInOut, DifStart1/100, 0, 2, 1, 3, iVar, nWords, pCanonPerm, pCanonPhase); 
+}
 ////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
 
 // It rearranges InOut (swaps and flips through rearrangement of quoters)
@@ -362,6 +411,14 @@ inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords,
     }
 }
 
+inline void minimalSwapAndFlipIVar_superFast_iVar5_noEBFC(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int DifStart1;
+    unsigned temp[2048];
+    if(minTemp1_fast_iVar5(pInOut, nWords, &DifStart1) == 2)
+        arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart1, 0, 2, 1, 3, pCanonPerm, pCanonPhase); 
+}
+
 ////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
 
 // It rearranges InOut (swaps and flips through rearrangement of quoters)
@@ -536,6 +593,14 @@ inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, i
     }
 }
 
+inline void minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int DifStart1;
+    word temp[1024];
+    if(minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1) == 2)
+        arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart1, 0, 2, 1, 3, iVar, pCanonPerm, pCanonPhase); 
+}
+
 /////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
 inline void minimalInitialFlip_fast_16Vars(word* pInOut, int  nVars, unsigned* pCanonPhase)
 {
@@ -587,38 +652,161 @@ inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWo
         return 1;
 }
 
-inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+inline int minimalSwapAndFlipIVar_superFast_all_noEBFC(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int i;
+    word pDuplicate[1024];  
+    int bitInfoTemp = pStore[0];
+    memcpy(pDuplicate,pInOut,nWords*sizeof(word));
+    for(i=0;i<5;i++)
+    {
+        if(bitInfoTemp == pStore[i+1])
+            minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+        else
+        {
+            bitInfoTemp = pStore[i+1];
+            continue;
+        }
+    }
+    if(bitInfoTemp == pStore[i+1])
+        minimalSwapAndFlipIVar_superFast_iVar5_noEBFC((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
+    else    
+        bitInfoTemp = pStore[i+1];
+    
+    for(i=6;i<nVars-1;i++)
+    {
+        if(bitInfoTemp == pStore[i+1])
+            minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+        else
+        {
+            bitInfoTemp = pStore[i+1];
+            continue;
+        }
+    }
+    if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
+        return 0;
+    else
+        return 1;
+}
+
+
+// old version with out noEBFC
+// inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+// {
+//     while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
+//         continue;
+// }
+
+inline void luckyCanonicizerS_F_first_16Vars1(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
 {
-    minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
-    while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
-        continue;
+    if(((* pCanonPhase) >> (nVars+1)) & 1)
+        while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
+            continue;
+    else
+        while( minimalSwapAndFlipIVar_superFast_all_noEBFC(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
+            continue;
 }
 
-inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+inline void luckyCanonicizerS_F_first_16Vars11(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
 {
-//    word pDuplicate[1024]={0};
-//    word pDuplicateLocal[1024]={0};
-//    memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
+    word duplicate[1024];
+    char pCanonPerm1[16];
+    unsigned uCanonPhase1;
+
+    if((* pCanonPhase) >> (nVars+2) )
+    {         
+        memcpy(duplicate, pInOut, sizeof(word)*nWords);
+        Kit_TruthNot_64bit(duplicate, nVars);
+        uCanonPhase1 = *pCanonPhase;
+        uCanonPhase1 ^= (1 << nVars);
+        memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
+        luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);        
+        luckyCanonicizerS_F_first_16Vars1(duplicate, nVars, nWords, pStore, pCanonPerm1, &uCanonPhase1);
+        if(memCompare(pInOut, duplicate,nVars) == 1)
+        {
+            *pCanonPhase = uCanonPhase1;
+            memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
+            memcpy(pInOut, duplicate, sizeof(word)*nWords);
+        }
+    }
+    else    
+        luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);
+}
 
+inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
     assert( nVars > 6 && nVars <= 16 );
     (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
-    luckyCanonicizerS_F_first_16Vars(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
+    luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); 
+}
+
+void bitReverceOrder(word* x, int  nVars)
+{
+    int i;
+    for(i= nVars-1;i>=0;i--)
+        Kit_TruthChangePhase_64bit( x, nVars, i );
+}
+
 
-//    memcpy(pDuplicate,pInOut,nWords*sizeof(word));
-//    assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
+inline void luckyCanonicizer_final_fast_16Vars1(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{   
+    assert( nVars > 6 && nVars <= 16 );
+    (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
+    luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); 
+    bitReverceOrder(pInOut, nVars);
+    (*pCanonPhase) ^= (1<<nVars) -1;
+    luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); 
 }
 
+
 // top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
-int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
+unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
 {
+    int nWords;
     int pStore[16];
     unsigned uCanonPhase = 0;
-    int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
+#ifdef LUCKY_VERIFY
+    word temp[1024] = {0};
+    word duplicate[1024] = {0};
+    Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
+#endif
     if ( nVars <= 6 )
-        pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
+        pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
     else if ( nVars <= 16 )
+    {
+        nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
         luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
+    }
+    else assert( 0 );
+#ifdef LUCKY_VERIFY
+    Kit_TruthCopy_64bit( temp, pInOut, nVars );
+    assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
+#endif
+        return uCanonPhase;
+}
+
+unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm)
+{
+    int nWords;
+    int pStore[16];
+    unsigned uCanonPhase = 0;
+#ifdef LUCKY_VERIFY
+    word temp[1024] = {0};
+    word duplicate[1024] = {0};
+    Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
+#endif
+    if ( nVars <= 6 )
+        pInOut[0] = luckyCanonicizer_final_fast_6Vars1( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
+    else if ( nVars <= 16 )
+    {
+        nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
+        luckyCanonicizer_final_fast_16Vars1( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
+    }
     else assert( 0 );
+#ifdef LUCKY_VERIFY
+    Kit_TruthCopy_64bit( temp, pInOut, nVars );
+    assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
+#endif
     return uCanonPhase;
 }
 
@@ -627,4 +815,3 @@ ABC_NAMESPACE_IMPL_END
 
 
 
-
diff --git a/src/bool/lucky/luckyFast6.c b/src/bool/lucky/luckyFast6.c
index 086a9bc6..bfc555aa 100644
--- a/src/bool/lucky/luckyFast6.c
+++ b/src/bool/lucky/luckyFast6.c
@@ -34,47 +34,7 @@ inline void resetPCanonPermArray(char* x, int nVars)
         x[i] = 'a'+i;
 }
 
-// we need next two functions only for verification of lucky method in debugging mode 
-void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
-{
-    int Temp;
-    swap_ij(pAfter, nVars, iVarInPosition, jVar);
-    
-    Temp = pCanonPerm[iVarInPosition];
-    pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
-    pCanonPerm[jVar] = Temp;
-    
-    if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
-    {
-        *pUCanonPhase ^= (1 << iVarInPosition);
-        *pUCanonPhase ^= (1 << jVar);
-    }
-    if((*pUCanonPhase>>iVarInPosition) & 1)
-        Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
-    
-}
-int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
-{
-    int i,j;
-    char tempChar;
-    for(j=0;j<nVars;j++)
-    {
-        tempChar = 'a'+ j;
-        for(i=j;i<nVars;i++)
-        {
-            if(tempChar != pCanonPerm[i])
-                continue;
-            swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
-            break;
-        }
-    }
-    if((uCanonPhase>>nVars) & 1)
-        Kit_TruthNot_64bit(pAfter, nVars );
-    if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
-        return 0;
-    else
-        return 1;
-}
+
 
 inline word Abc_allFlip(word x, unsigned* pCanonPhase)
 {
@@ -194,13 +154,29 @@ inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, uns
         return tMin;
     }
 }
+
+inline word Extra_Truth6MinimumRoundOne_noEBFC( word t, int iVar,  char* pCanonPerm, unsigned* pCanonPhase)
+{
+    word tMin;     
+    assert( iVar >= 0 && iVar < 5 );  
+    
+    tMin = Extra_Truth6SwapAdjacent( t, iVar );   // b a
+    if(t<tMin)
+        return t;
+    else
+    {
+        (* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, 4);
+        return tMin;
+    }
+}
+
+
 // this function finds minimal for all TIED(and tied only) iVars 
 //it finds tied vars based on rearranged  Store info - group of tied vars has the same bit count in Store
 inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
 {
     int i, bitInfoTemp;
-    word tMin0, tMin;
-    tMin=Abc_allFlip(t, pCanonPhase);
+    word tMin0, tMin=t;
     do
     {
         bitInfoTemp = pStore[0];
@@ -211,23 +187,99 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
                 tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );         
             else
                 bitInfoTemp = pStore[i+1];
+        }
+    }while ( tMin0 != tMin );
+    return tMin;
+}
+
+inline word Extra_Truth6MinimumRoundMany_noEBFC( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+    int i, bitInfoTemp;
+    word tMin0, tMin=t;
+    do
+    {
+        bitInfoTemp = pStore[0];
+        tMin0 = tMin;
+        for ( i = 0; i < 5; i++ )
+        {
+            if(bitInfoTemp == pStore[i+1])          
+                tMin = Extra_Truth6MinimumRoundOne_noEBFC( tMin, i, pCanonPerm, pCanonPhase );         
+            else
+                bitInfoTemp = pStore[i+1];
         } 
-        
     }while ( tMin0 != tMin );
     return tMin;
 }
+inline word Extra_Truth6MinimumRoundMany1( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+    word tMin0, tMin=t;
+    char pCanonPerm1[16];
+    unsigned uCanonPhase1;
+    switch ((* pCanonPhase) >> 7)
+    {
+    case 0 :
+        {
 
+            return Extra_Truth6MinimumRoundMany_noEBFC( t, pStore, pCanonPerm, pCanonPhase);
+        }
+    case 1 :
+        {            
+            return Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
+        }
+    case 2 :
+        { 
+            uCanonPhase1 = *pCanonPhase;
+            uCanonPhase1 ^= (1 << 6);
+            memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
+            tMin0 = Extra_Truth6MinimumRoundMany_noEBFC( t, pStore, pCanonPerm, pCanonPhase);
+            tMin =  Extra_Truth6MinimumRoundMany_noEBFC( ~t, pStore, pCanonPerm1, &uCanonPhase1);
+            if(tMin0 <=tMin)
+                return tMin0;
+            else
+            {
+                *pCanonPhase = uCanonPhase1;
+                memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
+                return tMin;
+            }
+        }
+    case 3 :
+        {
+            uCanonPhase1 = *pCanonPhase;
+            uCanonPhase1 ^= (1 << 6);
+            memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
+            tMin0 = Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
+            tMin =  Extra_Truth6MinimumRoundMany( ~t, pStore, pCanonPerm1, &uCanonPhase1);
+            if(tMin0 <=tMin)
+                return tMin0;
+            else
+            {
+                *pCanonPhase = uCanonPhase1;
+                memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
+                return tMin;
+            }
+        }
+    }
+    return Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
+}
 
-inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase)
 {
-//  word temp, duplicat = InOut;
     (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
-//  InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
-//      temp = InOut;
-//      assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
-//      return(InOut); 
-    return Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPerm, pCanonPhase );
-    
+    return Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase); 
 }
+inline word luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+    (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
+    InOut = Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase);
+    Kit_TruthChangePhase_64bit( &InOut, 6, 5 );
+    Kit_TruthChangePhase_64bit( &InOut, 6, 4 );
+    Kit_TruthChangePhase_64bit( &InOut, 6, 3 );
+    Kit_TruthChangePhase_64bit( &InOut, 6, 2 );
+    Kit_TruthChangePhase_64bit( &InOut, 6, 1 );        
+    Kit_TruthChangePhase_64bit( &InOut, 6, 0 );
+    (*pCanonPhase) ^= 0x3F;
+    return Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase); 
+}
+
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 2e476f86..4801b961 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -41,6 +41,7 @@ typedef unsigned __int64  word;
 #define true 1
 #define inline __inline  // compatible with MS VS 6.0
 #define ABC_ALLOC(type, num)    ((type *) malloc(sizeof(type) * (num)))
+// #define LUCKY_VERIFY
 #endif
 
 
@@ -118,9 +119,9 @@ extern  permInfo* setPermInfoPtr(int var);
 extern  void freePermInfoPtr(permInfo* x);
 extern  inline void  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
 extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
-extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore );
-extern  inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase );
-extern  inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
+extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore);
+extern  inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
+extern  inline word luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
 extern  inline void resetPCanonPermArray_6Vars(char* x);
 extern  void swap_ij( word* f,int totalVars, int varI, int varJ);
 extern  inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
diff --git a/src/bool/lucky/luckySimple.c b/src/bool/lucky/luckySimple.c
new file mode 100644
index 00000000..52e5e13d
--- /dev/null
+++ b/src/bool/lucky/luckySimple.c
@@ -0,0 +1,183 @@
+/**CFile****************************************************************
+
+  FileName    [luckySimple.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Truth table minimization procedures.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+static swapInfo* setSwapInfoPtr(int varsN)
+{
+    int i;
+    swapInfo* x = (swapInfo*) malloc(sizeof(swapInfo));
+    x->posArray = (varInfo*) malloc (sizeof(varInfo)*(varsN+2));
+    x->realArray = (int*) malloc (sizeof(int)*(varsN+2));
+    x->varN = varsN;
+    x->realArray[0]=varsN+100;
+    for(i=1;i<=varsN;i++)
+    {
+        x->posArray[i].position=i;
+        x->posArray[i].direction=-1;
+        x->realArray[i]=i;
+    }    
+    x->realArray[varsN+1]=varsN+10;
+    return x;
+}
+
+
+static void freeSwapInfoPtr(swapInfo* x)
+{
+    free(x->posArray);
+    free(x->realArray);
+    free(x);
+}
+
+int nextSwap(swapInfo* x)
+{
+    int i,j,temp;
+    for(i=x->varN;i>1;i--)
+    {
+        if( i > x->realArray[x->posArray[i].position + x->posArray[i].direction] )
+        {
+            x->posArray[i].position = x->posArray[i].position + x->posArray[i].direction;
+            temp = x->realArray[x->posArray[i].position];
+            x->realArray[x->posArray[i].position] = i; 
+            x->realArray[x->posArray[i].position - x->posArray[i].direction] = temp;
+            x->posArray[temp].position = x->posArray[i].position - x->posArray[i].direction; 
+            for(j=x->varN;j>i;j--)
+            {
+                x->posArray[j].direction =     x->posArray[j].direction * -1;
+            }
+            x->positionToSwap1 = x->posArray[temp].position - 1;
+            x->positionToSwap2 = x->posArray[i].position - 1;            
+            return 1;
+        }
+        
+    }
+    return 0;    
+}
+
+void fillInSwapArray(permInfo* pi)
+{
+    int counter=pi->totalSwaps-1;
+    swapInfo* x= setSwapInfoPtr(pi->varN);
+    while(nextSwap(x)==1)
+    {
+        if(x->positionToSwap1<x->positionToSwap2)
+            pi->swapArray[counter--]=x->positionToSwap1;
+        else
+            pi->swapArray[counter--]=x->positionToSwap2;
+    }
+    
+    freeSwapInfoPtr(x);    
+}
+int oneBitPosition(int x, int size)
+{
+    int i;
+    for(i=0;i<size;i++)
+        if((x>>i)&1 == 1)
+            return i;
+    return -1;
+}
+void fillInFlipArray(permInfo* pi)
+{
+    int i, temp=0, grayNumber;
+    for(i=1;i<=pi->totalFlips;i++)
+    {
+        grayNumber = i^(i>>1);
+        pi->flipArray[pi->totalFlips-i]=oneBitPosition(temp^grayNumber, pi->varN);
+        temp = grayNumber;        
+    }
+    
+    
+}
+inline int factorial(int n)
+{
+    return (n == 1 || n == 0) ? 1 : factorial(n - 1) * n;
+}
+permInfo* setPermInfoPtr(int var)
+{
+    permInfo* x;
+    x = (permInfo*) malloc(sizeof(permInfo));
+    x->flipCtr=0;
+    x->varN = var; 
+    x->totalFlips=(1<<var)-1;
+    x->swapCtr=0;
+    x->totalSwaps=factorial(var)-1;
+    x->flipArray = (int*) malloc(sizeof(int)*x->totalFlips);
+    x->swapArray = (int*) malloc(sizeof(int)*x->totalSwaps);
+    fillInSwapArray(x);
+    fillInFlipArray(x);
+    return x;
+}
+
+void freePermInfoPtr(permInfo* x)
+{
+    free(x->flipArray);
+    free(x->swapArray);
+    free(x);
+}
+inline void minWord(word* a, word* b, word* minimal, int nVars)
+{
+    if(memCompare(a, b, nVars) == -1)
+        Kit_TruthCopy_64bit( minimal, a, nVars );
+    else
+        Kit_TruthCopy_64bit( minimal, b, nVars );
+}
+inline void minWord3(word* a, word* b, word* minimal, int nVars)
+{ 
+    if (memCompare(a, b, nVars) <= 0)
+    {
+        if (memCompare(a, minimal, nVars) < 0) 
+            Kit_TruthCopy_64bit( minimal, a, nVars ); 
+        else 
+            return ;
+    }    
+    if (memCompare(b, minimal, nVars) <= 0)
+        Kit_TruthCopy_64bit( minimal, b, nVars );
+}
+void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
+{
+    int i,j=0;
+    Kit_TruthCopy_64bit( pAux, x, nVars );
+    Kit_TruthNot_64bit( x, nVars );
+    
+    minWord(x, pAux, minimal, nVars);
+    
+    for(i=pi->totalSwaps-1;i>=0;i--)
+    {
+        Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
+        Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
+        minWord3(x, pAux, minimal, nVars);
+    }
+    for(j=pi->totalFlips-1;j>=0;j--)
+    {
+        Kit_TruthSwapAdjacentVars_64bit(x, nVars, 0);
+        Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, 0);
+        Kit_TruthChangePhase_64bit(x, nVars, pi->flipArray[j]);
+        Kit_TruthChangePhase_64bit(pAux, nVars, pi->flipArray[j]);
+        minWord3(x, pAux, minimal, nVars);
+        for(i=pi->totalSwaps-1;i>=0;i--)
+        {
+            Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
+            Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
+            minWord3(x, pAux, minimal, nVars);
+        }
+    } 
+    Kit_TruthCopy_64bit( x, minimal, nVars );    
+}
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
index 13bb489e..e4065db6 100644
--- a/src/bool/lucky/luckySwap.c
+++ b/src/bool/lucky/luckySwap.c
@@ -241,6 +241,7 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
     } while ( fChange );
     return uCanonPhase;
 }
+
 inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
 {
     int nWords = Kit_TruthWordNum_64bit( nVars );
@@ -250,8 +251,8 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
     assert( nVars <= 16 );
     
     nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-    //  if ( (nOnes == nWords * 32) )
-    //      return 999999;
+    if ( nOnes == nWords * 32 )
+        uCanonPhase |= (1 << (nVars+2));
     
     if ( (nOnes > nWords * 32) )
     {
@@ -266,9 +267,12 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
-        //      if (  pStore[i]  == nOnes-pStore[i])
-        //          return 999999;
-        if ( pStore[i] >= nOnes-pStore[i])
+        if (  2*pStore[i]  == nOnes)
+        {
+            uCanonPhase |= (1 << (nVars+1));
+            continue;
+        }
+        if ( pStore[i] > nOnes-pStore[i])
             continue;
         uCanonPhase |= (1 << i);
         pStore[i] = nOnes-pStore[i]; 
diff --git a/src/bool/lucky/module.make b/src/bool/lucky/module.make
index dad5ee61..a65f61df 100644
--- a/src/bool/lucky/module.make
+++ b/src/bool/lucky/module.make
@@ -2,5 +2,6 @@ SRC +=  src/bool/lucky/lucky.c \
     src/bool/lucky/luckyFast16.c \
     src/bool/lucky/luckyFast6.c \
     src/bool/lucky/luckyRead.c \
+    src/bool/lucky/luckySimple.c \
     src/bool/lucky/luckySwapIJ.c \
     src/bool/lucky/luckySwap.c