Experiments with precomputation and matching.

5 files changed, 186 insertions, 99 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cbfb7b31..bb6e4aa7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5160,7 +5160,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault3( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdaovwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHMCNdazovwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5200,37 +5200,37 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFanoutMax < 0 )
                 goto usage;
             break;
-        case 'X':
+        case 'L':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nMffcMax = atoi(argv[globalUtilOptind]);
+            pPars->nMffcMin = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nMffcMax < 0 )
+            if ( pPars->nMffcMin < 0 )
                 goto usage;
             break;
-        case 'M':
+        case 'H':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            pPars->nMffcMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nWinSizeMax < 0 )
+            if ( pPars->nMffcMax < 0 )
                 goto usage;
             break;
-        case 'L':
+        case 'M':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nGrowthLevel < -ABC_INFINITY || pPars->nGrowthLevel > ABC_INFINITY )
+            if ( pPars->nWinSizeMax < 0 )
                 goto usage;
             break;
         case 'C':
@@ -5258,6 +5258,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'z':
+            pPars->fZeroCost ^= 1;
+            break;
         case 'o':
             pPars->fRrOnly ^= 1;
             break;
@@ -5288,17 +5291,18 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-aovwh]\n" );
+    Abc_Print( -2, "usage: mfs3 [-OIFLHMCN <num>] [-azovwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of mapped networks\n" );
     Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
     Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n",             pPars->nTfiLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nFanoutMax );
-    Abc_Print( -2, "\t-X <num> : the max size of max fanout-free cone (MFFC) [default = %d]\n",                 pPars->nMffcMax );
+    Abc_Print( -2, "\t-L <num> : the min size of max fanout-free cone (MFFC) [default = %d]\n",                 pPars->nMffcMin );
+    Abc_Print( -2, "\t-H <num> : the max size of max fanout-free cone (MFFC) [default = %d]\n",                 pPars->nMffcMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
-    Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
     Abc_Print( -2, "\t-N <num> : the max number of nodes to try (0 = all) [default = %d]\n",                    pPars->nNodesMax );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-z       : toggle zero-cost replacements [default = %s]\n",                               pPars->fZeroCost? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggle using old implementation for comparison [default = %s]\n",              pPars->fRrOnly? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 38744ae1..fbdcd042 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -46,6 +46,7 @@ struct Sfm_Par_t_
     int             nTfiLevMax;    // the maximum fanin levels
     int             nFanoutMax;    // the maximum number of fanouts
     int             nDepthMax;     // the maximum depth to try
+    int             nMffcMin;      // the minimum MFFC size
     int             nMffcMax;      // the maximum MFFC size
     int             nWinSizeMax;   // the maximum window size
     int             nGrowthLevel;  // the maximum allowed growth in level
@@ -55,6 +56,7 @@ struct Sfm_Par_t_
     int             fRrOnly;       // perform redundance removal
     int             fArea;         // performs optimization for area
     int             fMoreEffort;   // performs high-affort minimization
+    int             fZeroCost;     // enable zero-cost replacement
     int             fVerbose;      // enable basic stats
     int             fVeryVerbose;  // enable detailed stats
 };
diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index 03f80bf9..0c48ebc1 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -89,6 +89,7 @@ struct Sfm_Dec_t_
     int               nNodesConst1;
     int               nNodesBuf;
     int               nNodesInv;
+    int               nNodesAndOr;
     int               nNodesResyn;
     int               nSatCalls;
     int               nTimeOuts;
@@ -120,6 +121,7 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
     pPars->nTfoLevMax   = 1000;  // the maximum fanout levels
     pPars->nTfiLevMax   = 1000;  // the maximum fanin levels
     pPars->nFanoutMax   =   30;  // the maximum number of fanoutsp
+    pPars->nMffcMin     =    1;  // the maximum MFFC size
     pPars->nMffcMax     =    3;  // the maximum MFFC size
     pPars->nWinSizeMax  =  300;  // the maximum window size
     pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
@@ -280,11 +282,11 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit, word Mask )
+int Sfm_DecFindCost( Sfm_Dec_t * p, int c, int iLit, word Mask )
 {
     int Value0 = Abc_TtCountOnes( Vec_WrdEntry(&p->vSets[!c], Abc_Lit2Var(iLit)) & Mask );
-    int Weight0 = Abc_LitIsCompl(iLit) ? Abc_TtCountOnes( p->uMask[!c] & Mask ) - Value0 : Value0;
-    return Weight0;
+    int Cost0 = Abc_LitIsCompl(iLit) ? Abc_TtCountOnes( p->uMask[!c] & Mask ) - Value0 : Value0;
+    return Cost0;
 }
 void Sfm_DecPrint( Sfm_Dec_t * p, word * Masks )
 {
@@ -292,7 +294,7 @@ void Sfm_DecPrint( Sfm_Dec_t * p, word * Masks )
     for ( c = 0; c < 2; c++ )
     {
         Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
-        printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ", 
+        printf( "%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ", 
             c ? "OFF": "ON", p->iTarget, p->nDivs, 
             Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) );
         Vec_IntForEachEntry( vLevel, Entry, i )
@@ -301,24 +303,24 @@ void Sfm_DecPrint( Sfm_Dec_t * p, word * Masks )
 
         printf( "Implications: " );
         Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
-            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry, Masks ? Masks[!c] : ~(word)0) );
+            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindCost(p, c, Entry, Masks ? Masks[!c] : ~(word)0) );
         printf( "\n" );
         printf( "     " );
-        for ( i = 0; i <= p->iTarget; i++ )
-            printf( "%d", i / 10 );
+        for ( i = 0; i < p->nDivs; i++ )
+            printf( "%d", (i / 10) % 10 );
         printf( "\n" );
         printf( "     " );
-        for ( i = 0; i <= p->iTarget; i++ )
+        for ( i = 0; i < p->nDivs; i++ )
             printf( "%d", i % 10 );
         printf( "\n" );
         for ( k = 0; k < p->nPats[c]; k++ )
         {
             printf( "%2d : ", k );
-            for ( i = 0; i <= p->iTarget; i++ )
+            for ( i = 0; i < p->nDivs; i++ )
                 printf( "%d", (int)((Vec_WrdEntry(&p->vSets[c], i) >> k) & 1) );
             printf( "\n" );
         }
-        printf( "\n" );
+        //printf( "\n" );
     }
 }
 int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
@@ -326,7 +328,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     int fVerbose = p->pPars->fVeryVerbose;
     int nBTLimit = 0;
     int i, k, c, Entry, status, Lits[3], RetValue;
-    int iLitBest = -1, iCBest = -1, WeightBest = ABC_INFINITY, Weight;
+    int iLitBest = -1, iCBest = -1, CostMin = ABC_INFINITY, Cost;
     *pfConst = -1;
     // check stuck-at-0/1 (on/off-set empty)
     p->nPats[0] = p->nPats[1] = 0;
@@ -337,8 +339,8 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     Vec_WrdClear( &p->vSets[1] );
     for ( c = 0; c < 2; c++ )
     {
-        Lits[0] = Abc_Var2Lit( p->iTarget, c );
         p->nSatCalls++;
+        Lits[0] = Abc_Var2Lit( p->iTarget, c );
         status = sat_solver_solve( p->pSat, Lits, Lits + 1, nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
         {
@@ -352,7 +354,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
         }
         assert( status == l_True );
         // record this status
-        for ( i = 0; i <= p->iTarget; i++ )
+        for ( i = 0; i < p->nDivs; i++ )
             Vec_WrdPush( &p->vSets[c], (word)sat_solver_var_value(p->pSat, i) );
         p->nPats[c]++;
         p->uMask[c] = 1;
@@ -366,8 +368,8 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
             word Column = Vec_WrdEntry(&p->vSets[c], i);
             if ( Column != 0 && Column != p->uMask[c] ) // diff value is possible
                 continue;
-            Lits[1] = Abc_Var2Lit( i, Column != 0 );
             p->nSatCalls++;
+            Lits[1] = Abc_Var2Lit( i, Column != 0 );
             status = sat_solver_solve( p->pSat, Lits, Lits + 2, nBTLimit, 0, 0, 0 );
             if ( status == l_Undef )
                 return 0;
@@ -391,16 +393,16 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     {
         Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
         {
-            Weight = Sfm_DecFindWeight(p, c, Entry, (~(word)0));
-            if ( WeightBest > Weight )
+            Cost = Sfm_DecFindCost(p, c, Entry, (~(word)0));
+            if ( CostMin > Cost )
             {
-                WeightBest = Weight;
+                CostMin = Cost;
                 iLitBest = Entry;
                 iCBest = c;
             }
         }
     }
-    if ( WeightBest == ABC_INFINITY )
+    if ( CostMin == ABC_INFINITY )
     {
         p->nNoDecs++;
         return -2;
@@ -416,7 +418,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     // print the results
     if ( fVerbose )
     {
-        printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
+        printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), CostMin );
         Sfm_DecPrint( p, NULL );
     }
     return Abc_Var2Lit( iLitBest, iCBest );
@@ -545,11 +547,28 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
 {
     int nBTLimit = 0;
 //    int fVerbose = p->pPars->fVeryVerbose;
-    int c, i, d, Var, WeightBest, status;
-//    Vec_Int_t vAss = { SFM_SUPP_MAX, nAssump, pAssump };
-//    if ( nAssump > SFM_SUPP_MAX )
+    int c, i, d, Var, iLit, CostMin, status;
+    assert( nAssump <= SFM_SUPP_MAX );
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "\nObject %d\n", p->iTarget );
+        printf( "Divs = %d.  Nodes = %d.  Mffc = %d.  Mffc area = %.2f.    ", p->nDivs, Vec_IntSize(&p->vObjGates), p->nMffc, MIO_NUMINV*p->AreaMffc );
+        printf( "Pat0 = %d.  Pat1 = %d.    ", p->nPats[0], p->nPats[1] );
+        printf( "\n" );
+        if ( nAssump )
+        {
+            printf( "Cofactor: " );
+            for ( i = 0; i < nAssump; i++ )
+                printf( " %s%d", Abc_LitIsCompl(pAssump[i])? "!":"", Abc_Lit2Var(pAssump[i]) );
+            printf( "\n" );
+        }
+    }
     if ( nAssump > p->nMffc )
+    {
+        if ( p->pPars->fVeryVerbose )
+            printf( "The number of assumption is more than MFFC size.\n" );
         return -2;
+    }
     // check constant
     for ( c = 0; c < 2; c++ )
     {
@@ -563,12 +582,14 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
         if ( status == l_False )
         {
             pTruth[0] = c ? ~((word)0) : 0;
+            if ( p->pPars->fVeryVerbose )
+                printf( "Found constant %d.\n", c );
             return 0;
         }
         assert( status == l_True );
         if ( p->nPats[c] == 64 )
             return -2;//continue;
-        for ( i = 0; i <= p->iTarget; i++ )
+        for ( i = 0; i < p->nDivs; i++ )
             if ( sat_solver_var_value(p->pSat, i) )
                 *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
         p->uMask[c] |= ((word)1 << p->nPats[c]++);
@@ -586,9 +607,9 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
             assert( MaskAll );
             if ( MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros
                 continue;
+            p->nSatCalls++;
             pAssump[nAssump]   = Abc_Var2Lit( p->iTarget, c );
             pAssump[nAssump+1] = Abc_Var2Lit( d, MaskCur != 0 );
-            p->nSatCalls++;
             status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 2, nBTLimit, 0, 0, 0 );
             if ( status == l_Undef )
                 return -2;
@@ -602,31 +623,97 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
             if ( p->nPats[c] == 64 )
                 return -2;//continue;
             // record this status
-            for ( i = 0; i <= p->iTarget; i++ )
+            for ( i = 0; i < p->nDivs; i++ )
                 if ( sat_solver_var_value(p->pSat, i) )
                     *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
             p->uMask[c] |= ((word)1 << p->nPats[c]++);
         }
-        if ( Impls[0] == -1 || Impls[1] == -1 || Impls[0] == Impls[1] )
+        if ( Impls[0] == -1 || Impls[1] == -1 )
             continue;
+        if ( Impls[0] == Impls[1] )
+        {
+            Vec_IntPop( &p->vImpls[0] );
+            Vec_IntPop( &p->vImpls[1] );
+            continue;
+        }
         assert( Abc_Lit2Var(Impls[0]) == Abc_Lit2Var(Impls[1]) );
         // found buffer/inverter
         pTruth[0] = Abc_LitIsCompl(Impls[0]) ? ~p->pTtElems[0][0] : p->pTtElems[0][0];
         pSupp[0] = Abc_Lit2Var(Impls[0]);
+        if ( p->pPars->fVeryVerbose )
+            printf( "Found variable %s%d.\n", Abc_LitIsCompl(Impls[0]) ? "!":"", pSupp[0] );
         return 1;        
     }
 
+    // try using all implications at once
+//    if ( p->pPars->fVeryVerbose && p->iTarget == 56 )
+    for ( c = 0; c < 2; c++ )
+    {
+        if ( Vec_IntSize(&p->vImpls[!c]) < 2 )
+            continue;
+        p->nSatCalls++;
+        pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c );
+        assert( Vec_IntSize(&p->vImpls[!c]) < SFM_WIN_MAX-10 );
+        Vec_IntForEachEntry( &p->vImpls[!c], iLit, i )
+            pAssump[nAssump+1+i] = iLit;
+        status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump+1+i, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -2;
+        if ( status == l_False )
+        {
+            int * pFinal, nFinal = sat_solver_final( p->pSat, &pFinal );
+            if ( nFinal - nAssump - 0 > p->nMffc )
+                continue;
+            // collect only relevant literals
+            for ( i = d = 0; i < nFinal; i++ )
+                if ( Vec_IntFind(&p->vImpls[!c], Abc_LitNot(pFinal[i])) >= 0 )
+                    pSupp[d++] = Abc_LitNot(pFinal[i]);
+            nFinal = d;
+            // create AND/OR gate
+            assert( nFinal <= 6 );
+            if ( c )
+            {
+                *pTruth = ~(word)0;
+                for ( i = 0; i < nFinal; i++ )
+                {
+                    *pTruth &= Abc_LitIsCompl(pSupp[i]) ? ~s_Truths6[i] : s_Truths6[i];
+                    pSupp[i] = Abc_Lit2Var(pSupp[i]);
+                }
+            }
+            else
+            {
+                *pTruth = 0;
+                for ( i = 0; i < nFinal; i++ )
+                {
+                    *pTruth |= Abc_LitIsCompl(pSupp[i]) ? s_Truths6[i] : ~s_Truths6[i];
+                    pSupp[i] = Abc_Lit2Var(pSupp[i]);
+                }
+            }
+            p->nNodesAndOr++;
+            if ( p->pPars->fVeryVerbose )
+                printf( "Found %d-input AND/OR gate.\n", nFinal );
+            return nFinal;
+        }
+        assert( status == l_True );
+        if ( p->nPats[c] == 64 )
+            return -2;//continue;
+        for ( i = 0; i < p->nDivs; i++ )
+            if ( sat_solver_var_value(p->pSat, i) )
+                *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
+        p->uMask[c] |= ((word)1 << p->nPats[c]++);
+    }
+
+
     // find the best cofactoring variable
-    Var = -1, WeightBest = ABC_INFINITY;
+    Var = -1, CostMin = ABC_INFINITY;
     for ( c = 0; c < 2; c++ )
     {
-        int iLit, Weight;
         Vec_IntForEachEntry( &p->vImpls[c], iLit, i )
         {
-            Weight = Sfm_DecFindWeight( p, c, iLit, Masks[!c] );
-            if ( WeightBest > Weight )
+            int Cost = Sfm_DecFindCost( p, c, iLit, Masks[!c] );
+            if ( CostMin > Cost )
             {
-                WeightBest = Weight;
+                CostMin = Cost;
                 Var = Abc_Lit2Var(iLit);
             }
         }
@@ -640,10 +727,14 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
         fCofactor = 0;
     }
 
-//    printf( "Assumptions: " );
-//    Vec_IntPrint( &vAss );
-//    Sfm_DecPrint( p, Masks );
-//printf( "Best var %d with weight %d.\n", Var, WeightBest );
+    if ( p->pPars->fVeryVerbose )
+    {
+        Sfm_DecPrint( p, Masks );
+        printf( "Best var %d with weight %d.  Cofactored = %s\n", Var, CostMin, Var == p->nDivs - 1 ? "yes" : "no" );
+        printf( "\n" );
+        //if ( Var == 14 )
+        //    Var = 13;
+    }
 
     // cofactor the problem
     if ( Var >= 0 )
@@ -666,40 +757,20 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
         nSuppAll = Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );
         //if ( nSuppAll > p->nMffc )
         //    return -2;
+//        if ( p->pPars->fVeryVerbose )
+//        {
+//            int s = 0;
+//            ABC_SWAP( int, pSupp[0], pSupp[1] );
+//        }
         return nSuppAll;
     }
     return -2;
 }
-int Sfm_DecPeformDec2Int( Sfm_Dec_t * p )
-{
-    word uTruth[SFM_WORD_MAX];
-    word Masks[2] = { ~((word)0), ~((word)0) };
-    int pAssump[2*SFM_SUPP_MAX];
-    int pSupp[2*SFM_SUPP_MAX], nSupp;
-    p->nPats[0] = p->nPats[1] = 0;
-    p->uMask[0] = p->uMask[1] = 0;
-    Vec_WrdFill( &p->vSets[0], p->iTarget+1, 0 );
-    Vec_WrdFill( &p->vSets[1], p->iTarget+1, 0 );
-    nSupp = Sfm_DecPeformDec_rec( p, uTruth, pSupp, pAssump, 0, Masks, 1 );
-//printf( "%d %d  ", p->nPats[0], p->nPats[1] );
-
-//    printf( "Node %4d : ", p->iTarget );
-//    printf( "MFFC %2d  ", p->nMffc );
-    if ( nSupp == -2 )
-    {
-//        printf( "NO DEC.\n" );
-        p->nNoDecs++;
-        return -2;
-    }
-    // transform truth table
-    Dau_DsdPrintFromTruth( uTruth, nSupp );
-    return -1;
-}
 int Sfm_DecPeformDec2( Sfm_Dec_t * p )
 {
     word uTruth[SFM_WORD_MAX];
     word Masks[2] = { ~((word)0), ~((word)0) };
-    int pAssump[2*SFM_SUPP_MAX];
+    int pAssump[SFM_WIN_MAX];
     int pSupp[2*SFM_SUPP_MAX], nSupp, RetValue;
     p->nPats[0] = p->nPats[1] = 0;
     p->uMask[0] = p->uMask[1] = 0;
@@ -708,7 +779,7 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p )
     p->fUseLast = 1;
     nSupp = Sfm_DecPeformDec_rec( p, uTruth, pSupp, pAssump, 0, Masks, 1 );
     if ( p->pPars->fVeryVerbose )
-        printf( "Node %4d : ", p->iTarget );
+        printf( "\nNode %4d : ", p->iTarget );
     if ( p->pPars->fVeryVerbose )
         printf( "MFFC %2d  ", p->nMffc );
     if ( nSupp == -2 )
@@ -721,9 +792,9 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p )
     // transform truth table
     if ( p->pPars->fVeryVerbose )
         Dau_DsdPrintFromTruth( uTruth, nSupp );
-    RetValue = Sfm_LibImplement( p->pLib, uTruth[0], pSupp, nSupp, p->AreaMffc, &p->vObjGates, &p->vObjFanins );
+    RetValue = Sfm_LibImplement( p->pLib, uTruth[0], pSupp, nSupp, p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );
     if ( p->pPars->fVeryVerbose )
-        printf( "Implementation %sfound.\n", RetValue < 0 ? "NOT " : "" );
+        printf( "Area-reducing implementation %sfound.\n", RetValue < 0 ? "NOT " : "" );
     return RetValue;
 }
 
@@ -870,13 +941,14 @@ int Abc_NtkDfsCheck_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPivot )
 }
 int Sfm_DecExtract( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars, Abc_Obj_t * pPivot, Vec_Int_t * vRoots, Vec_Int_t * vGates, Vec_Wec_t * vFanins, Vec_Int_t * vMap, Vec_Int_t * vTfi, Vec_Int_t * vTfo, int * pnMffc, int * pnAreaMffc )
 {
+    int fVeryVerbose = 0; //pPars->fVeryVerbose;
     Vec_Int_t * vLevel;
     Abc_Obj_t * pObj, * pFanin;
     int nLevelMax = pPivot->Level + pPars->nTfoLevMax;
     int nLevelMin = pPivot->Level - pPars->nTfiLevMax;
     int i, k, nTfiSize, nDivs = -1;
     assert( Abc_ObjIsNode(pPivot) );
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "\n\nTarget %d\n", Abc_ObjId(pPivot) );
     // collect TFO nodes
     Vec_IntClear( vTfo );
@@ -898,9 +970,9 @@ printf( "\n\nTarget %d\n", Abc_ObjId(pPivot) );
     Abc_NtkDfsOne_rec( pPivot, vTfi, nLevelMin, SFM_MASK_PI );
     nTfiSize = Vec_IntSize(vTfi);
     // additinally mark MFFC
-    *pnMffc = Sfm_DecMarkMffc( pPivot, nLevelMin, pPars->nMffcMax, pPars->fVeryVerbose, pnAreaMffc );
+    *pnMffc = Sfm_DecMarkMffc( pPivot, nLevelMin, pPars->nMffcMax, fVeryVerbose, pnAreaMffc );
     assert( *pnMffc <= pPars->nMffcMax );
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "Mffc size = %d. Mffc area = %.2f\n", *pnMffc, *pnAreaMffc*MIO_NUMINV );
     // collect TFI(TFO)
     Abc_NtkForEachObjVec( vTfo, pNtk, pObj, i )
@@ -912,28 +984,28 @@ printf( "Mffc size = %d. Mffc area = %.2f\n", *pnMffc, *pnAreaMffc*MIO_NUMINV );
                 if ( pFanin->iTemp == SFM_MASK_INPUT )
                     pFanin->iTemp = SFM_MASK_FANIN;
     // collect nodes supported only on TFI fanins and not MFFC
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "\nDivs: " );
     Vec_IntClear( vMap );
     Vec_IntClear( vGates );
     Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
         if ( pObj->iTemp == SFM_MASK_PI )
-            Sfm_DecAddNode( pObj, vMap, vGates, Abc_ObjIsCi(pObj) || Abc_ObjLevel(pObj) < nLevelMin, pPars->fVeryVerbose );
+            Sfm_DecAddNode( pObj, vMap, vGates, Abc_ObjIsCi(pObj) || Abc_ObjLevel(pObj) < nLevelMin, fVeryVerbose );
     nDivs = Vec_IntSize(vMap);
     // add other nodes that are not in TFO and not in MFFC
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "\nSides: " );
     Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
         if ( pObj->iTemp == (SFM_MASK_PI | SFM_MASK_INPUT) || pObj->iTemp == SFM_MASK_FANIN || pObj->iTemp == 0 ) // const
-            Sfm_DecAddNode( pObj, vMap, vGates, pObj->iTemp == SFM_MASK_FANIN, pPars->fVeryVerbose );
+            Sfm_DecAddNode( pObj, vMap, vGates, pObj->iTemp == SFM_MASK_FANIN, fVeryVerbose );
     // add the TFO nodes
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "\nTFO: " );
     Abc_NtkForEachObjVec( vTfi, pNtk, pObj, i )
         if ( pObj->iTemp >= SFM_MASK_MFFC )
-            Sfm_DecAddNode( pObj, vMap, vGates, 0, pPars->fVeryVerbose );
+            Sfm_DecAddNode( pObj, vMap, vGates, 0, fVeryVerbose );
     assert( Vec_IntSize(vMap) == Vec_IntSize(vGates) );
-if ( pPars->fVeryVerbose )
+if ( fVeryVerbose )
 printf( "\n" );
     // create node IDs
     Vec_WecClear( vFanins );
@@ -1033,8 +1105,8 @@ void Sfm_DecInsert( Abc_Ntk_t * pNtk, Abc_Obj_t * pPivot, int Limit, Vec_Int_t *
 }
 void Sfm_DecPrintStats( Sfm_Dec_t * p )
 {
-    printf( "Node = %d. Try = %d. Change = %d.   Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d.\n",
-        p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn );
+    printf( "Node = %d. Try = %d. Change = %d.   Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d. AndOr = %d.\n",
+        p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn, p->nNodesAndOr );
     printf( "MaxDiv = %d. MaxWin = %d.   AveDiv = %d. AveWin = %d.   Calls = %d. T/O = %d. NoDec = %d.\n",
         p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nTimeOuts, p->nNoDecs );
 
@@ -1081,11 +1153,13 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     abctime clk;
     int i = 0, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
     //int iNode = 8;//70; //2341;//8;//70;
-    printf( "Running remapping with parameters: " );
+    printf( "Remapping parameters: " );
     printf( "TFO = %d. ", pPars->nTfoLevMax );
     printf( "TFI = %d. ", pPars->nTfiLevMax );
     printf( "FanMax = %d. ", pPars->nFanoutMax );
+    printf( "MffcMin = %d. ", pPars->nMffcMin );
     printf( "MffcMax = %d. ", pPars->nMffcMax );
+    printf( "Zero-cost = %s. ", pPars->fZeroCost ? "yes" : "no" );
     printf( "\n" );
     // enter library
     assert( Abc_NtkIsMappedLogic(pNtk) );
@@ -1113,9 +1187,13 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     {
         if ( i >= nStop || (pPars->nNodesMax && i > pPars->nNodesMax) )
             break;
+        if ( pPars->nMffcMin > 1 && Abc_NodeMffcLabel(pObj) < pPars->nMffcMin )
+            continue;
+        p->nNodesTried++;
         //if ( i == pPars->nNodesMax )
         //    pPars->fVeryVerbose = 1;
-        p->nNodesTried++;
+        //pPars->fVeryVerbose = (i % 260 == 0);
+
 clk = Abc_Clock();
         p->nDivs = Sfm_DecExtract( pNtk, pPars, pObj, &p->vObjRoots, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vTemp, &p->vTemp2, &p->nMffc, &p->AreaMffc );
 p->timeWin += Abc_Clock() - clk;
@@ -1135,14 +1213,16 @@ clk = Abc_Clock();
             RetValue = Sfm_DecPeformDec( p );
         else
             RetValue = Sfm_DecPeformDec2( p );
+        if ( p->pPars->fVeryVerbose )
+            printf( "\n\n" );
 p->timeSat += Abc_Clock() - clk;
         if ( RetValue < 0 )
             continue;
         p->nNodesChanged++;
         Abc_NtkCountStats( p, Limit );
         Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands, p->GateBuffer, p->GateInvert, &p->vGateFuncs );
-if ( pPars->fVeryVerbose )
-printf( "This was modification %d\n", Count );
+//if ( pPars->fVeryVerbose )
+//printf( "This was modification %d\n", Count );
         //if ( Count == 2 )
         //    break;
         Count++;
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 3bd218a7..cc502d6f 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -47,6 +47,7 @@ ABC_NAMESPACE_HEADER_START
 
 #define SFM_SUPP_MAX  6
 #define SFM_WORD_MAX ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)
+#define SFM_WIN_MAX   1000
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -193,7 +194,7 @@ extern int          Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, in
 extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fVerbose );
 extern void         Sfm_LibPrint( Sfm_Lib_t * p );
 extern void         Sfm_LibStop( Sfm_Lib_t * p );
-extern int          Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
+extern int          Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost );
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index 47a643fe..c68099ff 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -428,7 +428,7 @@ void Sfm_LibTest( int nVars, int fTwo, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
+int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost )
 {
     Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
     Mio_Gate_t * pGate;
@@ -460,7 +460,7 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, in
     Sfm_LibForEachSuper( p, pObj, iFunc )
         if ( !pObjMin || pObjMin->Area > pObj->Area )
             pObjMin = pObj;
-    if ( pObjMin == NULL || pObjMin->Area >= AreaMffc )
+    if ( pObjMin == NULL || (fZeroCost ? pObjMin->Area > AreaMffc : pObjMin->Area >= AreaMffc) )
         return -1;
     // get the gates
     pCellB = p->pCells + (int)pObjMin->pFansB[0];