Experiment with support minimization.

src/base/abci/abc.c

@@ -6330,6 +6330,7 @@ usage:
 int Abc_CommandVarMin( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose );
+    extern void Abc_SuppReadMinTest( char * pFileName );
     int nOnes      =  4;
     int nVars      = 20;
     int fUseSimple =  0;
@@ -6378,6 +6379,12 @@ int Abc_CommandVarMin( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    // get the file name
+    if ( argc == globalUtilOptind + 1 )
+    {
+        Abc_SuppReadMinTest( argv[globalUtilOptind] );
+        return 0;
+    }
     Abc_SuppTest( nOnes, nVars, fUseSimple, fCheck, fVerbose );
     return 0;
 

src/misc/extra/extraUtilSupp.c

@@ -23,6 +23,7 @@
 #include <string.h>
 #include <assert.h>
 #include "misc/vec/vec.h"
+#include "misc/vec/vecWec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -30,12 +31,158 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of unique entries.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Vec_IntUniqueHashKeyDebug( unsigned char * pStr, int nChars, int TableMask )
+{
+    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+    {
+        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
+        printf( "%d : ", c );
+        printf( "%3d  ", pStr[c] );
+        printf( "%12u ", Key );
+        printf( "%12u ", Key&TableMask );
+        printf( "\n" );
+    }
+    return Key;
+}
+void Vec_IntUniqueProfile( Vec_Int_t * vData, int * pTable, int * pNexts, int TableMask, int nIntSize )
+{
+    int i, Key, Counter;
+    for ( i = 0; i <= TableMask; i++ )
+    {
+        Counter = 0;
+        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
+            Counter++;
+        if ( Counter < 7 )
+            continue;
+        printf( "%d\n", Counter );
+        for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] )
+        {
+            Extra_PrintBinary( stdout, Vec_IntEntryP(vData, Key*nIntSize), 40 ), printf( "\n" );
+//            Vec_IntUniqueHashKeyDebug( (unsigned char *)Vec_IntEntryP(vData, Key*nIntSize), 4*nIntSize, TableMask );
+        }
+    }
+    printf( "\n" );
+}
+
+
+static inline unsigned Vec_IntUniqueHashKey2( unsigned char * pStr, int nChars )
+{
+    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
+    return Key;
+}
+
+static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars )
+{
+    static unsigned s_BigPrimes[16] = 
+    {
+        0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
+        0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055
+    };
+    static unsigned s_BigPrimes2[16] = 
+    {
+        0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
+        0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10
+    };
+    unsigned Key = 0; int c;
+    for ( c = 0; c < nChars; c++ )
+        Key += s_BigPrimes2[(2*c)&15]   * s_BigPrimes[(unsigned)pStr[c] & 15] +
+               s_BigPrimes2[(2*c+1)&15] * s_BigPrimes[(unsigned)pStr[c] >> 4];
+    return Key;
+}
+static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart )
+{
+    int * pData = Vec_IntEntryP( vData, i*nIntSize );
+    for ( ; *pStart != -1; pStart = pNexts + *pStart )
+        if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) )
+            return pStart;
+    return pStart;
+}
+static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap )
+{
+    int nEntries  = Vec_IntSize(vData) / nIntSize;
+    int TableMask = (1 << Abc_Base2Log(nEntries)) - 1;
+    int * pTable  = ABC_FALLOC( int, TableMask+1 );
+    int * pNexts  = ABC_FALLOC( int, TableMask+1 );
+    int * pClass  = ABC_ALLOC( int, nEntries );
+    int i, Key, * pEnt, nUnique = 0;
+    assert( nEntries * nIntSize == Vec_IntSize(vData) );
+    for ( i = 0; i < nEntries; i++ )
+    {
+        pEnt = Vec_IntEntryP( vData, i*nIntSize );
+        Key  = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize );
+        pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key );
+        if ( *pEnt == -1 )
+            *pEnt = i, nUnique++;
+        pClass[i] = *pEnt;
+    }
+//    Vec_IntUniqueProfile( vData, pTable, pNexts, TableMask, nIntSize );
+    ABC_FREE( pTable );
+    ABC_FREE( pNexts );
+    if ( pvMap )
+        *pvMap = Vec_IntAllocArray( pClass, nEntries );
+    else
+        ABC_FREE( pClass );
+    return nUnique;
+}
+static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize )
+{
+    Vec_Int_t * vMap, * vUnique;
+    int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap );
+    vUnique = Vec_IntAlloc( nUnique * nIntSize );
+    Vec_IntForEachEntry( vMap, Ent, i )
+    {
+        if ( Ent < i ) continue;
+        assert( Ent == i );
+        Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize );
+    }
+    assert( Vec_IntSize(vUnique) == nUnique * nIntSize );
+    Vec_IntFree( vMap );
+    return vUnique;
+}
+static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize )
+{
+    Vec_Int_t * vResInt;
+    Vec_Int_t * vDataInt = (Vec_Int_t *)vData;
+    vDataInt->nSize *= 2;
+    vDataInt->nCap *= 2;
+    vResInt = Vec_IntUniqifyHash( vDataInt, 2 * nWordSize );
+    vDataInt->nSize /= 2;
+    vDataInt->nCap /= 2;
+    vResInt->nSize /= 2;
+    vResInt->nCap /= 2;
+    return (Vec_Wrd_t *)vResInt;
+}
+static inline word * Vec_WrdLimit( Vec_Wrd_t * p )
+{
+    return p->pArray + p->nSize;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Generate m-out-of-n vectors.]
 
   Description []
@@ -52,13 +199,13 @@ static inline int Abc_SuppCountOnes( unsigned i )
     i = ((i + (i >> 4)) & 0x0F0F0F0F);
     return (i*(0x01010101))>>24;
 }
-Vec_Int_t * Abc_SuppGen( int m, int n )
+Vec_Wrd_t * Abc_SuppGen( int m, int n )
 {
-    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
     int i, Size = (1 << n);
     for ( i = 0; i < Size; i++ )
         if ( Abc_SuppCountOnes(i) == m )
-            Vec_IntPush( vRes, i );
+            Vec_WrdPush( vRes, i );
     return vRes;
 }
 
@@ -73,13 +220,14 @@ Vec_Int_t * Abc_SuppGen( int m, int n )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin )
+void Abc_SuppVerify( Vec_Wrd_t * p, word * pMatrix, int nVars, int nVarsMin )
 {
-    Vec_Int_t * pNew;
-    int * pLimit, * pEntry1, * pEntry2;
-    int i, k, v, Entry, EntryNew, Value, Counter = 0;
-    pNew = Vec_IntAlloc( Vec_IntSize(p) );
-    Vec_IntForEachEntry( p, Entry, i )
+    Vec_Wrd_t * pNew;
+    word * pLimit, * pEntry1, * pEntry2;
+    word Entry, EntryNew;
+    int i, k, v, Value, Counter = 0;
+    pNew = Vec_WrdAlloc( Vec_WrdSize(p) );
+    Vec_WrdForEachEntry( p, Entry, i )
     {
         EntryNew = 0;
         for ( v = 0; v < nVarsMin; v++ )
@@ -89,13 +237,13 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin
                 if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) )
                     Value ^= 1;
             if ( Value )
-                EntryNew |= (1 << v);            
+                EntryNew |= (((word)1) << v);            
         }
-        Vec_IntPush( pNew, EntryNew );
+        Vec_WrdPush( pNew, EntryNew );
     }
     // check that they are disjoint
-    pLimit  = Vec_IntLimit(pNew);
-    pEntry1 = Vec_IntArray(pNew);
+    pLimit  = Vec_WrdLimit(pNew);
+    pEntry1 = Vec_WrdArray(pNew);
     for ( ; pEntry1 < pLimit; pEntry1++ )
     for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
         if ( *pEntry1 == *pEntry2 )
@@ -104,7 +252,7 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin
         printf( "The total of %d pairs fail verification.\n", Counter );
     else
         printf( "Verification successful.\n" );
-    Vec_IntFree( pNew );
+    Vec_WrdFree( pNew );
 }
 
 /**Function*************************************************************
@@ -118,28 +266,28 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_SuppGenPairs( Vec_Int_t * p, int nBits )
+Vec_Wrd_t * Abc_SuppGenPairs( Vec_Wrd_t * p, int nBits )
 {
-    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
     unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) ); 
-    int * pLimit = Vec_IntLimit(p);
-    int * pEntry1 = Vec_IntArray(p);
-    int * pEntry2, Value;
+    word * pLimit = Vec_WrdLimit(p);
+    word * pEntry1 = Vec_WrdArray(p);
+    word * pEntry2, Value;
     for ( ; pEntry1 < pLimit; pEntry1++ )
     for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ )
     {
         Value = *pEntry1 ^ *pEntry2;
-        if ( Abc_InfoHasBit(pMap, Value) )
+        if ( Abc_InfoHasBit(pMap, (int)Value) )
             continue;
-        Abc_InfoXorBit( pMap, Value );
-        Vec_IntPush( vRes, Value );
+        Abc_InfoXorBit( pMap, (int)Value );
+        Vec_WrdPush( vRes, Value );
     }
     ABC_FREE( pMap );
     return vRes;
 }
-Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits )
+Vec_Wrd_t * Abc_SuppGenPairs2( int nOnes, int nBits )
 {
-    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
     int i, k, Size = (1 << nBits), Value;
     for ( i = 0; i < Size; i++ )
     {
@@ -148,7 +296,7 @@ Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits )
             if ( Value == 2*k )
                 break;
         if ( k <= nOnes )
-            Vec_IntPush( vRes, i );
+            Vec_WrdPush( vRes, i );
     }
     return vRes;
 }
@@ -164,30 +312,31 @@ Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_SuppPrintMask( unsigned uMask, int nBits )
+void Abc_SuppPrintMask( word uMask, int nBits )
 {
     int i;
     for ( i = 0; i < nBits; i++ )
         printf( "%d", (uMask >> i) & 1 );
     printf( "\n" );
 }
-void Abc_SuppGenProfile( Vec_Int_t * p, int nBits, int * pCounts )
+void Abc_SuppGenProfile( Vec_Wrd_t * p, int nBits, int * pCounts )
 {
-    int i, k, b, Ent;
-    Vec_IntForEachEntry( p, Ent, i )
+    word Ent;
+    int i, k, b;
+    Vec_WrdForEachEntry( p, Ent, i )
         for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ )
             pCounts[k] += ((Ent >> k) & 1) ^ b;
 }
-void Abc_SuppPrintProfile( Vec_Int_t * p, int nBits )
+void Abc_SuppPrintProfile( Vec_Wrd_t * p, int nBits )
 {
-    int k, Counts[32] = {0};
+    int k, Counts[64] = {0};
     Abc_SuppGenProfile( p, nBits, Counts );
     for ( k = 0; k < nBits; k++ )
-        printf( "%2d : %6d  %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_IntSize(p) );
+        printf( "%2d : %6d  %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_WrdSize(p) );
 }
-int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit )
+int Abc_SuppGenFindBest( Vec_Wrd_t * p, int nBits, int * pMerit )
 {
-    int k, kBest = 0, Counts[32] = {0};
+    int k, kBest = 0, Counts[64] = {0};
     Abc_SuppGenProfile( p, nBits, Counts );
     for ( k = 1; k < nBits; k++ )
         if ( Counts[kBest] < Counts[k] )
@@ -195,25 +344,26 @@ int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit )
     *pMerit = Counts[kBest];
     return kBest;
 }
-void Abc_SuppGenSelectVar( Vec_Int_t * p, int nBits, int iVar )
+void Abc_SuppGenSelectVar( Vec_Wrd_t * p, int nBits, int iVar )
 {
-    int * pEntry = Vec_IntArray(p);
-    int * pLimit = Vec_IntLimit(p);
+    word * pEntry = Vec_WrdArray(p);
+    word * pLimit = Vec_WrdLimit(p);
     for ( ; pEntry < pLimit; pEntry++ )
         if ( (*pEntry >> iVar) & 1 )
-            *pEntry ^= (1 << nBits);
+            *pEntry ^= (((word)1) << nBits);
 }
-void Abc_SuppGenFilter( Vec_Int_t * p, int nBits )
+void Abc_SuppGenFilter( Vec_Wrd_t * p, int nBits )
 {
-    int i, k = 0, Ent;
-    Vec_IntForEachEntry( p, Ent, i )
+    word Ent;
+    int i, k = 0;
+    Vec_WrdForEachEntry( p, Ent, i )
         if ( ((Ent >> nBits) & 1) == 0 )
-            Vec_IntWriteEntry( p, k++, Ent );
-    Vec_IntShrink( p, k );
+            Vec_WrdWriteEntry( p, k++, Ent );
+    Vec_WrdShrink( p, k );
 }
-unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits )
+word Abc_SuppFindOne( Vec_Wrd_t * p, int nBits )
 {
-    unsigned uMask = 0;
+    word uMask = 0;
     int Prev = -1, This, Var;
     while ( 1 )
     {
@@ -222,14 +372,14 @@ unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits )
             break;
         Prev = This;
         Abc_SuppGenSelectVar( p, nBits, Var );
-        uMask |= (1 << Var);
+        uMask |= (((word)1) << Var);
     }
     return uMask;
 }
-int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose )
+int Abc_SuppMinimize( word * pMatrix, Vec_Wrd_t * p, int nBits, int fVerbose )
 {
     int i;
-    for ( i = 0; Vec_IntSize(p) > 0; i++ )
+    for ( i = 0; Vec_WrdSize(p) > 0; i++ )
     {
 //        Abc_SuppPrintProfile( p, nBits );
         pMatrix[i] = Abc_SuppFindOne( p, nBits );
@@ -238,7 +388,7 @@ int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose
             continue;
         // print stats
         printf( "%2d : ", i );
-        printf( "%6d  ", Vec_IntSize(p) );
+        printf( "%6d  ", Vec_WrdSize(p) );
         Abc_SuppPrintMask( pMatrix[i], nBits );
 //        printf( "\n" );
     }
@@ -259,16 +409,16 @@ int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose
 void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose )
 {
     int nVarsMin;
-    unsigned Matrix[100];
+    word Matrix[64];
     abctime clk = Abc_Clock();
     // create the problem
-    Vec_Int_t * vRes = Abc_SuppGen( nOnes, nVars );
-    Vec_Int_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars );
+    Vec_Wrd_t * vRes = Abc_SuppGen( nOnes, nVars );
+    Vec_Wrd_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars );
     assert( nVars < 100 );
     printf( "M = %2d  N = %2d : ", nOnes, nVars );
-    printf( "K = %6d   ",  Vec_IntSize(vRes) );
-    printf( "Total = %12.0f  ", 0.5 * Vec_IntSize(vRes) * (Vec_IntSize(vRes) - 1) );
-    printf( "Distinct = %8d  ",  Vec_IntSize(vPairs) );
+    printf( "K = %6d   ",  Vec_WrdSize(vRes) );
+    printf( "Total = %12.0f  ", 0.5 * Vec_WrdSize(vRes) * (Vec_WrdSize(vRes) - 1) );
+    printf( "Distinct = %8d  ",  Vec_WrdSize(vPairs) );
     Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk );
     // solve the problem
     clk = Abc_Clock();
@@ -277,8 +427,243 @@ void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbos
     Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
     if ( fCheck )
         Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin );
-    Vec_IntFree( vPairs );
-    Vec_IntFree( vRes );
+    Vec_WrdFree( vPairs );
+    Vec_WrdFree( vRes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the input part of the cubes specified in MIN format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Abc_SuppReadMin( char * pFileName, int * pnVars )
+{
+    extern char * Extra_FileReadContents( char * pFileName );
+    Vec_Wrd_t * vRes; word uCube;
+    int nCubes = 0, nVars = -1, iVar;
+    char * pCur, * pToken, * pStart = "INPUT F-COVER";
+    char * pStr = Extra_FileReadContents( pFileName );
+    if ( pStr == NULL )
+        { printf( "Cannot open input file (%s).\n", pFileName ); return NULL; }
+    pCur = strstr( pStr, pStart );
+    if ( pCur == NULL )
+        { printf( "Cannot find beginning of cube cover (%s).\n", pStart ); return NULL; }
+    pToken = strtok( pCur + strlen(pStart), " \t\r\n," );
+    nCubes = atoi( pToken );
+    if ( nCubes < 1 || nCubes > 1000000 )
+        { printf( "The number of cubes in not in the range [1; 1000000].\n" ); return NULL; }
+    vRes = Vec_WrdAlloc( 1000 );
+    uCube = 0; iVar = 0;
+    while ( (pToken = strtok(NULL, " \t\r\n,")) != NULL )
+    {
+        if ( strlen(pToken) > 2 )
+        {
+            if ( !strncmp(pToken, "INPUT", strlen("INPUT")) )
+                break;
+            if ( iVar > 64 )
+                { printf( "The number of inputs (%d) is too high.\n", iVar ); Vec_WrdFree(vRes); return NULL; }
+            if ( nVars == -1 )
+                nVars = iVar;
+            else if ( nVars != iVar )
+                { printf( "The number of inputs (%d) does not match declaration (%d).\n", nVars, iVar ); Vec_WrdFree(vRes); return NULL; }
+            Vec_WrdPush( vRes, uCube );
+            uCube = 0; iVar = 0;
+            continue;
+        }
+        if ( pToken[1] == '0' && pToken[0] == '1' ) // value 1
+            uCube |= (((word)1) << iVar);
+        else if ( pToken[1] != '1' || pToken[0] != '0' ) // value 0
+            { printf( "Strange literal representation (%s) of cube %d.\n", pToken, nCubes ); Vec_WrdFree(vRes); return NULL; }
+        iVar++;
+    }
+    ABC_FREE( pStr );
+    if ( Vec_WrdSize(vRes) != nCubes )
+        { printf( "The number of cubes (%d) does not match declaration (%d).\n", Vec_WrdSize(vRes), nCubes ); Vec_WrdFree(vRes); return NULL; }
+    else
+        printf( "Successfully parsed function with %d inputs and %d cubes.\n", nVars, nCubes );
+    *pnVars = nVars;
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Abc_SuppDiffMatrix( Vec_Wrd_t * vCubes )
+{
+    abctime clk = Abc_Clock();
+    word * pEnt2, * pEnt = Vec_WrdArray( vCubes );
+    word * pLimit = Vec_WrdLimit( vCubes );
+    Vec_Wrd_t * vRes, * vPairs = Vec_WrdAlloc( Vec_WrdSize(vCubes) * (Vec_WrdSize(vCubes) - 1) / 2 );
+    word * pStore = Vec_WrdArray( vPairs );
+    for ( ; pEnt < pLimit; pEnt++ )
+    for ( pEnt2 = pEnt+1; pEnt2 < pLimit; pEnt2++ )
+        *pStore++ = *pEnt ^ *pEnt2;
+    vPairs->nSize = Vec_WrdCap(vPairs);
+    assert( pStore == Vec_WrdLimit(vPairs) );
+//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+//    vRes = Vec_WrdUniqifyHash( vPairs, 1 );
+    vRes = Vec_WrdDup( vPairs );
+    printf( "Successfully generated diff matrix with %10d rows (%6.2f %%).  ", 
+        Vec_WrdSize(vRes), 100.0 * Vec_WrdSize(vRes) / Vec_WrdSize(vPairs) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Vec_WrdFree( vPairs );
+    return vRes;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solve difference matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_SuppCountOnes64( word i )
+{
+    i = i - ((i >> 1) & 0x5555555555555555);
+    i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
+    i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
+    return (i*(0x0101010101010101))>>56;
+}
+int Abc_SuppFindVar( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
+{
+    int v, vBest = -1, dBest;
+    for ( v = 0; v < nVars; v++ )
+    {
+        if ( Vec_WecLevelSize(pS, v) )
+            continue;
+        if ( vBest == -1 || dBest > Vec_WecLevelSize(pD, v) )
+            vBest = v, dBest = Vec_WecLevelSize(pD, v);
+    }
+    return vBest;
+}
+void Abc_SuppRemove( Vec_Wrd_t * p, int * pCounts, Vec_Wec_t * pS, Vec_Wec_t * pD, int iVar, int nVars )
+{
+    word Entry; int i, v;
+    assert( Vec_WecLevelSize(pS, iVar) == 0 );
+    Vec_IntClear( Vec_WecEntry(pD, iVar) );
+    Vec_WrdForEachEntry( p, Entry, i )
+    {
+        if ( ((Entry >> iVar) & 1) == 0 )
+            continue;
+        pCounts[i]--;
+        if ( pCounts[i] == 1 )
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( (Entry >> v) & 1 )
+                {
+                    Vec_IntRemove( Vec_WecEntry(pD, v), i );
+                    Vec_WecPush( pS, v, i );
+                }
+        }
+        else if ( pCounts[i] == 2 )
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( (Entry >> v) & 1 )
+                    Vec_WecPush( pD, v, i );
+        }        
+    }
+}
+void Abc_SuppProfile( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars )
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+        printf( "%2d : S = %3d  D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) );
+}
+int Abc_SuppSolve( Vec_Wrd_t * p, int nVars )
+{
+    abctime clk = Abc_Clock();
+    Vec_Wrd_t * pNew = Vec_WrdDup( p );
+    Vec_Wec_t * vSingles = Vec_WecStart( 64 );
+    Vec_Wec_t * vDoubles = Vec_WecStart( 64 );
+    word Entry; int i, v, iVar, nVarsNew = nVars;
+    int * pCounts = ABC_ALLOC( int, Vec_WrdSize(p) );
+    Vec_WrdForEachEntry( p, Entry, i )
+    {
+        pCounts[i] = Abc_SuppCountOnes64( Entry );
+        if ( pCounts[i] == 1 )
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( (Entry >> v) & 1 )
+                    Vec_WecPush( vSingles, v, i );
+        }
+        else if ( pCounts[i] == 2 )
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( (Entry >> v) & 1 )
+                    Vec_WecPush( vDoubles, v, i );
+        }
+    }
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+//    Abc_SuppProfile( vSingles, vDoubles, nVars );
+    // find variable in 0 singles and the smallest doubles
+    while ( 1 )
+    {
+        iVar = Abc_SuppFindVar( vSingles, vDoubles, nVars );
+        if ( iVar == -1 )
+            break;
+//        printf( "Selected variable %d.\n", iVar );
+        Abc_SuppRemove( pNew, pCounts, vSingles, vDoubles, iVar, nVars );
+//        Abc_SuppProfile( vSingles, vDoubles, nVars );
+        nVarsNew--;
+    }
+//    printf( "Result = %d (out of %d)\n", nVarsNew, nVars );
+    Vec_WecFree( vSingles );
+    Vec_WecFree( vDoubles );
+    Vec_WrdFree( pNew );
+    ABC_FREE( pCounts );
+    return nVarsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_SuppReadMinTest( char * pFileName )
+{
+    int fVerbose = 0;
+    abctime clk = Abc_Clock();
+    word Matrix[64];
+    int nVars, nVarsMin;
+    Vec_Wrd_t * vPairs, * vCubes;
+    vCubes = Abc_SuppReadMin( pFileName, &nVars );
+    if ( vCubes == NULL )
+        return;
+    vPairs = Abc_SuppDiffMatrix( vCubes );
+    Vec_WrdFreeP( &vCubes );
+    // solve the problem
+    clk = Abc_Clock();
+//    nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose );
+    nVarsMin = Abc_SuppSolve( vPairs, nVars );
+    printf( "Solution with %d variables found.  ", nVarsMin );
+    Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk );
+
+    Vec_WrdFreeP( &vPairs );
 }
 
 ////////////////////////////////////////////////////////////////////////