From 51c5ff3b81df553b7d872cf1c675789e807dc158 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 20 Nov 2025 13:35:47 -0800
Subject: [PATCH] Updated to "lutexact".

---
 src/base/abci/abc.c   |  9 +++++++--
 src/sat/bmc/bmc.h     |  1 +
 src/sat/bmc/bmcMaj8.c | 39 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 47 insertions(+), 2 deletions(-)

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 49a789fcb..fc6592452 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10757,6 +10757,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern int  Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars );
     extern int  Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars );
+    extern int  Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
     extern int  Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars );
     extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars );
     extern void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars );
@@ -10765,7 +10766,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10890,6 +10891,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fSilent ^= 1;
             break;
+        case 'm':
+            pPars->fMinNodes ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -10966,7 +10970,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsvh] <hex>\n" );
+    Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of I-input function using N K-input gates\n" );
     Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
     Abc_Print( -2, "\t-M <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
@@ -10987,6 +10991,7 @@ usage:
     Abc_Print( -2, "\t-k       : toggle using Kissat 4.0.2 by Armin Biere [default = %s]\n", pPars->fKissat ? "yes" : "no" );
     Abc_Print( -2, "\t-d       : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
     Abc_Print( -2, "\t-s       : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
+    Abc_Print( -2, "\t-m       : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
     Abc_Print( -2, "\t<hex>    : truth table in hex notation\n" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 85fd0265c..374945039 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -67,6 +67,7 @@ struct Bmc_EsPar_t_
     int        fUniqFans;
     int        fLutCascade;
     int        fLutInFixed;
+    int        fMinNodes;
     int        RuntimeLim;
     int        nRandFuncs;
     int        nMintNum;
diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c
index 902c5006a..ae0307994 100644
--- a/src/sat/bmc/bmcMaj8.c
+++ b/src/sat/bmc/bmcMaj8.c
@@ -670,6 +670,9 @@ static int Exa8_ManAddCnf( Exa8_Man_t * p, int iMint )
 
 int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
 {
+    extern int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
+    if ( pPars->fMinNodes )
+        return Exa8_ManExactSynthesisIter( pPars );
     int status = KISSAT_UNDEC;
     int Res = 0;
     abctime clkTotal = Abc_Clock();
@@ -744,6 +747,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
     }
     else
     {
+        Res = 0;
         if ( pPars->RuntimeLim )
             printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
     }
@@ -757,6 +761,41 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
     return Res;
 }
 
+int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
+{
+    pPars->fMinNodes = 0;
+    int nNodeMin = (pPars->nVars-2)/(pPars->nLutSize-1) + 1;
+    int nNodeMax = pPars->nNodes, Result = 0;
+    int fGenPerm = pPars->pPermStr == NULL;
+    for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
+        printf( "\nTrying M = %d:\n", n );
+        pPars->nNodes = n;
+        if ( fGenPerm ) {
+            Vec_Str_t * vStr = Vec_StrAlloc( 100 );
+            for ( int v = 0; v < pPars->nLutSize; v++ )
+                Vec_StrPush( vStr, 'a'+v );
+            int nDupVars = Abc_MaxInt(0, (pPars->nLutSize-1) - (pPars->nVars-pPars->nLutSize));
+            Vec_StrPush( vStr, '_' );
+            for ( int v = 0; v < nDupVars; v++ )
+                Vec_StrPush( vStr, 'a'+v );
+            for ( int v = 0; v < pPars->nLutSize-1-nDupVars; v++ )
+                Vec_StrPush( vStr, '*' );
+            for ( int m = 2; m < pPars->nNodes; m++ ) {
+                Vec_StrPush( vStr, '_' );
+                for ( int v = 0; v < pPars->nLutSize-1; v++ )
+                    Vec_StrPush( vStr, '*' );
+            }
+            Vec_StrPush( vStr, '\0' );
+            ABC_FREE( pPars->pPermStr );
+            pPars->pPermStr = Vec_StrReleaseArray(vStr);
+            Vec_StrFree( vStr );
+        }
+        Result = Exa8_ManExactSynthesis(pPars);
+        if ( Result != 2 )
+            break;
+    }
+    return Result;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///