Experiments with SPFD-based decomposition + new K-map print-out.

4 files changed, 659 insertions, 16 deletions

diff --git a/src/aig/bdc/bdcSpfd.c b/src/aig/bdc/bdcSpfd.c
index f6946872..1ffc6fc7 100644
--- a/src/aig/bdc/bdcSpfd.c
+++ b/src/aig/bdc/bdcSpfd.c
@@ -69,6 +69,15 @@ static inline int Bdc_CountSpfd( word t, word f )
     return n00 * n11 + n10 * n01;
 }
 
+static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    if ( fCof1 )
+        return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar));
+    else
+        return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar));
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -128,8 +137,11 @@ void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
   SeeAlso     []
 
 ***********************************************************************/
-void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
+void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth )
 {
+    word Diff = Truth ^ pNode->Truth;
+    Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( "   " );
+    Extra_PrintHex( stdout, (unsigned *)&Diff, 6 );         printf( "   " );
     Bdc_SpfdPrint_rec( pNode, Level, vLevels );
     printf( "    %d\n", pNode->Weight );
 }
@@ -149,7 +161,7 @@ void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
 {
     int nSize = nCands * nCands * (nGatesMax + 1) * 5;
     Vec_Ptr_t * vLevels;
-    Vec_Int_t * vCounts, * vWeight;
+    Vec_Int_t * vBegs, * vWeight;
     Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
     int Count0, Count1, * pPerm;
     int i, j, k, c, n, clk;
@@ -176,7 +188,7 @@ void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
 
     // allocate
     vLevels = Vec_PtrAlloc( 100 );
-    vCounts = Vec_IntAlloc( 100 );
+    vBegs = Vec_IntAlloc( 100 );
     vWeight = Vec_IntAlloc( 100 );
 
     // initialize elementary variables
@@ -186,7 +198,7 @@ void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
     for ( i = 0; i < nVars; i++ )
         pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
     Vec_PtrPush( vLevels, pNode );
-    Vec_IntPush( vCounts, nVars );
+    Vec_IntPush( vBegs, nVars );
 
     // the next level
 clk = clock();
@@ -203,7 +215,7 @@ clk = clock();
     }
     assert( c == 5 * nVars * (nVars - 1) / 2 );
     Vec_PtrPush( vLevels, pNode );
-    Vec_IntPush( vCounts, c );
+    Vec_IntPush( vBegs, c );
     for ( i = 0; i < c; i++ )
     {
         pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
@@ -226,12 +238,12 @@ Abc_PrintTime( 1, "Time", clock() - clk );
 clk = clock();
         c = 0;
         pNode1 = Vec_PtrEntry( vLevels, n-1 );
-        Count1 = Vec_IntEntry( vCounts, n-1 );
+        Count1 = Vec_IntEntry( vBegs, n-1 );
         // go through previous levels
         for ( k = 0; k < n-1; k++ )
         {
             pNode0 = Vec_PtrEntry( vLevels, k );
-            Count0 = Vec_IntEntry( vCounts, k );
+            Count0 = Vec_IntEntry( vBegs, k );
             for ( i = 0; i < Count0; i++ )
             for ( j = 0; j < Count1; j++ )
             {
@@ -259,13 +271,14 @@ clk = clock();
         for ( i = 0; i < c; i++ )
         {
             pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
-//Bdc_SpfdPrint( pNode + i, 1, vLevels );
+if ( pNode[i].Weight > 300 )
+Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
             Vec_IntPush( vWeight, pNode[i].Weight );
 
             if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
             {
                 printf( "Function can be implemented using %d gates.\n", n );
-                Bdc_SpfdPrint( pNode + i, n, vLevels );
+                Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
                 goto cleanup;
             }
         }
@@ -286,13 +299,13 @@ clk = clock();
         }
         ABC_FREE( pPerm );
         Vec_PtrPush( vLevels, pNode2 );
-        Vec_IntPush( vCounts, j );
+        Vec_IntPush( vBegs, j );
 
 printf( "Selected %6d gates (out of %6d) on level %2d.   ", j, c, n );
 Abc_PrintTime( 1, "Time", clock() - clk );
 
         for ( i = 0; i < 10; i++ )
-            Bdc_SpfdPrint( pNode2 + i, n, vLevels );
+            Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
     }
 
 cleanup:
@@ -300,7 +313,7 @@ cleanup:
     Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
         ABC_FREE( pNode );
     Vec_PtrFree( vLevels );
-    Vec_IntFree( vCounts );
+    Vec_IntFree( vBegs );
     Vec_IntFree( vWeight );
 }
 
@@ -316,7 +329,7 @@ cleanup:
   SeeAlso     []
 
 ***********************************************************************/
-void Bdc_SpfdDecomposeTest()
+void Bdc_SpfdDecomposeTest_()
 {
     int fTry = 0;
 //    word T[17];
@@ -326,8 +339,9 @@ void Bdc_SpfdDecomposeTest()
 //    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
 //    word Truth    = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
 //    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
-    word Truth = 0x9ef7a8d9c7193a0f;
-//    word Truth = 0x5052585a0002080a;
+//    word Truth = 0x9ef7a8d9c7193a0f;  // AAFFAAFF0A0F0A0F
+//    word Truth = 0x34080226CD163000;
+    word Truth = 0x5052585a0002080a;
     int nVars     =    6;
     int nCands    =  200;// 75;
     int nGatesMax =   20;
@@ -360,6 +374,518 @@ void Bdc_SpfdDecomposeTest()
 */
 }
 
+
+
+
+typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
+struct Bdc_Ent_t_
+{
+    unsigned         iFan0   : 30;
+    unsigned         fCompl0 :  1;
+    unsigned         fCompl  :  1;
+    unsigned         iFan1   : 30;
+    unsigned         fCompl1 :  1;
+    unsigned         fExor   :  1;
+    int              iNext;
+    int              iList;
+    word             Truth;
+};
+
+#define BDC_TERM 0x3FFFFFFF
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdHashValue( word t, int Size )
+{
+    // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
+    // 53,
+    // 97,
+    // 193,
+    // 389,
+    // 769,
+    // 1543,
+    // 3079,
+    // 6151,
+    // 12289,
+    // 24593,
+    // 49157,
+    // 98317,
+    // 196613,
+    // 393241,
+    // 786433,
+    // 1572869,
+    // 3145739,
+    // 6291469,
+    // 12582917,
+    // 25165843,
+    // 50331653,
+    // 100663319,
+    // 201326611,
+    // 402653189,
+    // 805306457,
+    // 1610612741,
+    static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
+    unsigned char * s = (unsigned char *)&t;
+    unsigned i, Value = 0;
+    for ( i = 0; i < 8; i++ )
+        Value ^= BigPrimes[i] * s[i];
+    return Value % Size;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
+{
+    Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
+    if ( pBin->iList == 0 )
+        return &pBin->iList;
+    for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
+    {
+        if ( pBin->Truth == t )
+            return NULL;
+        if ( pBin->iNext == 0 )
+            return &pBin->iNext;
+    }
+    assert( 0 );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
+{
+    int nFuncs = 3000000; // the number of functions to compute
+    int nSize  = 2777111; // the hash table size to use
+    int Limit  = 5;
+
+    
+//    int nFuncs = 13000000; // the number of functions to compute
+//    int nSize  = 12582917; // the hash table size to use
+//    int Limit  = 6;
+
+//    int nFuncs =  60000000; // the number of functions to compute
+//    int nSize  =  50331653; // the hash table size to use
+//    int Limit  = 6;
+
+    int * pPlace, i, n, m, s, fCompl, clk = clock(), clk2;
+    Vec_Int_t * vStops;
+    Vec_Wrd_t * vTruths;
+    Vec_Int_t * vWeights;
+    Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
+    word t0, t1, t;
+    assert( nSize <= nFuncs );
+
+    printf( "Allocating %.2f Mb of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );
+
+    p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
+    memset( p, 255, sizeof(Bdc_Ent_t) );
+    p->iList = 0;
+    q = p + 1;
+    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
+
+    vTruths = Vec_WrdAlloc( 100 );
+    vWeights = Vec_IntAlloc( 100 );
+
+    // create elementary vars
+    vStops = Vec_IntAlloc( 10 );
+    Vec_IntPush( vStops, 1 );
+    for ( i = 0; i < 6; i++ )
+    {
+        q->iFan0 = BDC_TERM;
+        q->iFan1 = i;
+        q->Truth = Truths[i];
+        pPlace   = Bdc_SpfdHashLookup( p, nSize, q->Truth );
+        *pPlace  = q-p;
+        q++;
+        Vec_WrdPush( vTruths, Truths[i] );
+        Vec_IntPush( vWeights, 0 );
+    }
+    Vec_IntPush( vStops, 7 );
+    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
+
+    // create gates
+    for ( n = 0; n < 10; n++ )
+    {
+        // set the start and stop
+        pBeg1 = p + Vec_IntEntry( vStops, n );
+        pEnd1 = p + Vec_IntEntry( vStops, n+1 );
+
+        // try previous
+        for ( m = 0; m < n; m++ )
+        if ( m+n+1 <= Limit )
+        {
+            clk2 = clock();
+            pBeg0 = p + Vec_IntEntry( vStops, m );
+            pEnd0 = p + Vec_IntEntry( vStops, m+1 );
+            printf( "Trying %6d x %6d.  ", pEnd0-pBeg0, pEnd1-pBeg1 );
+            for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
+            for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
+            for ( s = 0; s < 5; s++ )
+            {
+                t0 = (s&1)      ? ~pThis0->Truth : pThis0->Truth;
+                t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
+                t  = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
+                fCompl = t & 1;
+                if ( fCompl )
+                    t = ~t;
+                if ( t == 0 )
+                    continue;
+                pPlace = Bdc_SpfdHashLookup( p, nSize, t );
+                if ( pPlace == NULL )
+                    continue;
+                q->iFan0   = pThis0-p;
+                q->fCompl0 = s&1;
+                q->iFan1   = pThis1-p;
+                q->fCompl1 = (s>>1)&1;
+                q->fExor   = (s>>2)&1;
+                q->Truth   = t;
+                q->fCompl  = fCompl;
+                *pPlace = q-p;
+                q++;
+                Vec_WrdPush( vTruths, t );
+                Vec_IntPush( vWeights, m+n+1 );
+                if ( q-p == nFuncs )
+                    goto finish;
+            }
+            Vec_IntPush( vStops, q-p );
+            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", m, n, m+n+1, q-p );
+            Abc_PrintTime( 1, "Time", clock() - clk2 );
+        }
+        if ( n+n+1 > Limit )
+            continue;
+
+        // try current
+        clk2 = clock();
+        printf( "Trying %6d x %6d.  ", pEnd1-pBeg1, pEnd1-pBeg1 );
+        for ( pThis0 = pBeg1; pThis0 < pEnd1; pThis0++ )
+        for ( pThis1 = pThis0+1; pThis1 < pEnd1; pThis1++ )
+        for ( s = 0; s < 5; s++ )
+        {
+            t0 = (s&1)      ? ~pThis0->Truth : pThis0->Truth;
+            t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
+            t  = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
+            fCompl = t & 1;
+            if ( fCompl )
+                t = ~t;
+            if ( t == 0 )
+                continue;
+            pPlace = Bdc_SpfdHashLookup( p, nSize, t );
+            if ( pPlace == NULL )
+                continue;
+            q->iFan0   = pThis0-p;
+            q->fCompl0 = s&1;
+            q->iFan1   = pThis1-p;
+            q->fCompl1 = (s>>1)&1;
+            q->fExor   = (s>>2)&1;
+            q->Truth   = t;
+            q->fCompl  = fCompl;
+            *pPlace = q-p;
+            q++;
+            Vec_WrdPush( vTruths, t );
+            Vec_IntPush( vWeights, n+n+1 );
+            if ( q-p == nFuncs )
+                goto finish;
+        }
+        Vec_IntPush( vStops, q-p );
+        assert( n || q-p == 82 );
+        printf( "Added %d + %d + 1 = %d. Total = %8d.   ", n, n, n+n+1, q-p );
+        Abc_PrintTime( 1, "Time", clock() - clk2 );
+    }
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+/*
+    {
+        FILE * pFile = fopen( "func6var5node.txt", "w" );
+        word t;
+        Vec_WrdSortUnsigned( vTruths );
+        Vec_WrdForEachEntry( vTruths, t, i )
+            Extra_PrintHex( pFile, (unsigned *)&t, 6 ), fprintf( pFile, "\n" );
+        fclose( pFile );
+    }
+*/
+    {
+        FILE * pFile = fopen( "func6v5n_bin.txt", "wb" );
+//        Vec_WrdSortUnsigned( vTruths );
+        fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
+        fclose( pFile );
+    }
+    {
+        FILE * pFile = fopen( "func6v5nW_bin.txt", "wb" );
+        fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
+        fclose( pFile );
+    }
+
+finish:
+    Vec_IntFree( vStops );
+//    Vec_WrdFree( vTruths );
+    free( p );
+
+    *pvWeights = vWeights;
+    return vTruths;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Bdc_SpfdReadFiles( Vec_Int_t ** pvWeights )
+{
+    Vec_Int_t * vWeights;
+    Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
+    FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
+    fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
+    fclose( pFile );
+
+    vWeights = Vec_IntStart( 12776759 );
+    pFile = fopen( "func6v6nW_bin.txt", "rb" );
+    fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
+    fclose( pFile );
+
+    *pvWeights = vWeights;
+    return vDivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
+{
+    int Ones = Bdc_CountOnes(f);
+    if ( Ones == 0 )
+        return -1;
+    return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
+//    return Bdc_CountOnes(f);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
+{
+    word Func, FuncBest;
+    int i, Cost, CostBest = -1, NumBest;
+    Vec_WrdForEachEntry( vDivs, Func, i )
+    {
+        if ( (Func & F0) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = Func;
+                NumBest  = i;
+            }
+        }
+        if ( (Func & F1) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = Func;
+                NumBest  = i;
+            }
+        }
+        if ( (~Func & F0) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = ~Func;
+                NumBest  = i;
+            }
+        }
+        if ( (~Func & F1) == 0 )
+        {
+            Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
+            if ( CostBest < Cost )
+            {
+                CostBest = Cost;
+                FuncBest = ~Func;
+                NumBest  = i;
+            }
+        }
+    }
+    (*pCost) += Vec_IntEntry(vWeights, NumBest);
+    assert( CostBest > 0 );
+    printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
+    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
+    return FuncBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
+{
+    extern void Abc_Show6VarFunc( word F0, word F1 );
+    word F1 = t;
+    word F0 = ~F1;
+    word Func;
+    int i, Cost = 0;
+//    Abc_Show6VarFunc( F0, F1 );   
+    for ( i = 0; F0 && F1; i++ )
+    {
+        printf( "*** ITER %2d   ", i );
+        Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
+        F0 &= ~Func;
+        F1 &= ~Func;
+//        Abc_Show6VarFunc( F0, F1 );    
+    }
+    Cost += (i-1);
+    printf( "Produce solution with cost %d.\n", Cost );
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_SpfdDecomposeTest()
+{
+//    word t = 0x5052585a0002080a;
+
+    word t = 0x9ef7a8d9c7193a0f;
+//    word t = 0x6BFDA276C7193A0F;
+//    word t = 0xA3756AFE0B1DF60B;
+
+    int clk = clock();
+//    Vec_Int_t * vWeights;
+//    Vec_Wrd_t * vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
+    Vec_Int_t * vWeights;
+    Vec_Wrd_t * vDivs = Bdc_SpfdReadFiles( &vWeights );
+
+    word c0, c1, s, tt, ttt, tbest;
+    int i, j, k, n, Cost, CostBest = 100000;
+
+    return;
+
+    Abc_Show6VarFunc( ~t, t );  
+/*
+    for ( i = 0; i < 6; i++ )
+    for ( j = 0; j < 6; j++ )
+    {
+        if ( i == j )
+            continue;
+        c0 = Bdc_Cof6( t, i, 0 );
+        c1 = Bdc_Cof6( t, i, 1 );
+        s  = Truths[i] ^ Truths[j];
+        tt = (~s & c0) | (s & c1);
+
+        Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
+        if ( CostBest > Cost )
+        {
+            CostBest = Cost;
+            tbest = tt;
+        }
+    }
+*/
+
+    for ( i = 0; i < 6; i++ )
+    for ( j = 0; j < 6; j++ )
+    {
+        if ( i == j )
+            continue;
+        c0 = Bdc_Cof6( t, i, 0 );
+        c1 = Bdc_Cof6( t, i, 1 );
+        s  = Truths[i] ^ Truths[j];
+        tt = (~s & c0) | (s & c1);
+
+        for ( k = 0; k < 6; k++ )
+        for ( n = 0; n < 6; n++ )
+        {
+            if ( k == n )
+                continue;
+            c0 = Bdc_Cof6( tt, k, 0 );
+            c1 = Bdc_Cof6( tt, k, 1 );
+            s  = Truths[k] ^ Truths[n];
+            ttt= (~s & c0) | (s & c1);
+
+            Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
+            if ( CostBest > Cost )
+            {
+                CostBest = Cost;
+                tbest = ttt;
+            }
+        }
+    }
+
+
+    printf( "Best solution found with cost %d.  ", CostBest );
+    Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
+    Abc_PrintTime( 1, "  Time", clock() - clk );
+
+    Vec_WrdFree( vDivs );
+    Vec_IntFree( vWeights );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e7b8beb6..cf0526a9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -766,6 +766,7 @@ extern ABC_DLL void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * p
 extern ABC_DLL void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 extern ABC_DLL void               Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
 extern ABC_DLL void               Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_NtkShow6VarFunc( char * pF0, char * pF1 );
 /*=== abcProve.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
 extern ABC_DLL int                Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 63d22148..f2348d34 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1878,13 +1878,17 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( argc == globalUtilOptind + 2 )
+    {
+        Abc_NtkShow6VarFunc( argv[globalUtilOptind], argv[globalUtilOptind+1] );
+        return 0;
+    }
 
     if ( pNtk == NULL )
     {
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-
     if ( !Abc_NtkIsLogic(pNtk) )
     {
         Abc_Print( -1, "Visualization of Karnaugh maps works for logic networks.\n" );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 352ddf52..9e2f48d3 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1384,6 +1384,118 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
     return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints K-map of 6-var function represented by truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Show6VarFunc( word F0, word F1 )
+{
+    // order of cells in the Karnaugh map
+//    int Cells[8] = { 0, 1, 3, 2, 6, 7, 5, 4 };
+    int Cells[8] = { 0, 4, 6, 2, 3, 7, 5, 1 };
+    // intermediate variables
+    int s; // symbol counter
+    int h; // horizontal coordinate;
+    int v; // vertical coordinate;
+    assert( (F0 & F1) == 0 );
+
+    // output minterms above
+    for ( s = 0; s < 4; s++ )
+        printf( " " );
+    printf( " " );
+    for ( h = 0; h < 8; h++ )
+    {
+        for ( s = 0; s < 3; s++ )
+            printf( "%d",  ((Cells[h] >> (2-s)) & 1) );
+        printf( " " );
+    }
+    printf( "\n" );
+
+    // output horizontal line above
+    for ( s = 0; s < 4; s++ )
+        printf( " " );
+    printf( "+" );
+    for ( h = 0; h < 8; h++ )
+    {
+        for ( s = 0; s < 3; s++ )
+            printf( "-" );
+        printf( "+" );
+    }
+    printf( "\n" );
+
+    // output lines with function values
+    for ( v = 0; v < 8; v++ )
+    {
+        for ( s = 0; s < 3; s++ )
+            printf( "%d",  ((Cells[v] >> (2-s)) & 1) );
+        printf( " |" );
+
+        for ( h = 0; h < 8; h++ )
+        {
+            printf( " " );
+            if ( ((F0 >> ((Cells[v]*8)+Cells[h])) & 1) )
+                printf( "0" );
+            else if ( ((F1 >> ((Cells[v]*8)+Cells[h])) & 1) )
+                printf( "1" );
+            else
+                printf( " " );
+            printf( " |" );
+        }
+        printf( "\n" );
+
+        // output horizontal line above
+        for ( s = 0; s < 4; s++ )
+            printf( " " );
+//        printf( "%c", v == 7 ? '+' : '|' );
+        printf( "+" );
+        for ( h = 0; h < 8; h++ )
+        {
+            for ( s = 0; s < 3; s++ )
+                printf( "-" );
+//            printf( "%c", v == 7 ? '+' : '|' );
+            printf( "%c", (v == 7 || h == 7) ? '+' : '|' );
+        }
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints K-map of 6-var function represented by truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShow6VarFunc( char * pF0, char * pF1 )
+{
+    word F0, F1;
+    if ( strlen(pF0) != 16 )
+    {
+        printf( "Wrong length (%d) of 6-var truth table (%s).\n", strlen(pF0), pF0 );
+        return;
+    }
+    if ( strlen(pF1) != 16 )
+    {
+        printf( "Wrong length (%d) of 6-var truth table (%s).\n", strlen(pF1), pF1 );
+        return;
+    }
+    Extra_ReadHexadecimal( (unsigned *)&F0, pF0, 6 );
+    Extra_ReadHexadecimal( (unsigned *)&F1, pF1, 6 );
+    Abc_Show6VarFunc( F0, F1 );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////