From 0ebc9dbbaecc1c1c1471b43774088d0fb357d539 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Mar 2025 09:39:04 -0700 Subject: [PATCH] Experiments with exact synthesis. --- src/aig/gia/giaSimBase.c | 4 +-- src/base/abci/abc.c | 10 +++++-- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcMaj.c | 60 ++++++++++++++++++++++++++-------------- 4 files changed, 50 insertions(+), 25 deletions(-) diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 87614c490..e5cf77dcb 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) { - extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose ); + extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard ); int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); @@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In } assert( iMint == nMints ); printf( "Created %d minterms.\n", iMint ); - Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 ); + Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0 ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a4078d54c..1c2e39501 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10061,7 +10061,7 @@ int Abc_CommandTwoExact( 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, "INTGabdconugklvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklmvh" ) ) != EOF ) { switch ( c ) { @@ -10139,6 +10139,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': fKissat2 ^= 1; break; + case 'm': + pPars->fCard ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10179,7 +10182,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fUseNands ) Exa_ManExactSynthesis7( pPars, GateSize ); - else if ( fKissat ) + else if ( fKissat || pPars->fCard ) Exa_ManExactSynthesis4( pPars ); else if ( fKissat2 ) Exa_ManExactSynthesis5( pPars ); @@ -10190,7 +10193,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklmvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); @@ -10206,6 +10209,7 @@ usage: Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" ); + Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "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 : truth table in hex notation\n" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 92fbb7422..320a85886 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -57,6 +57,7 @@ struct Bmc_EsPar_t_ int fDynConstr; int fDumpCnf; int fGlucose; + int fCard; int fOrderNodes; int fEnumSols; int fFewerVars; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 68601338e..7cd138c5f 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1941,7 +1941,7 @@ static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Li int pLits[4] = { Lit0, Lit1, Lit2, Lit3 }; return Exa4_ManAddClause( p, pLits, 4 ); } -int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans ) +int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard ) { int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits; for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ ) @@ -1955,9 +1955,17 @@ int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 ); assert( nLits > 0 ); Exa4_ManAddClause( p, pLits, nLits ); - for ( n = 0; n < nLits; n++ ) - for ( m = n+1; m < nLits; m++ ) - Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 ); + if ( !fCard ) { + for ( n = 0; n < nLits; n++ ) + for ( m = n+1; m < nLits; m++ ) + Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 ); + } + else { + fprintf( p->pFile, "k %d ", nLits-1 ); + for ( n = 0; n < nLits; n++ ) + pLits[n] = Abc_LitNot(pLits[n]); + Exa4_ManAddClause( p, pLits, nLits ); + } if ( k == 1 ) break; for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] ) @@ -2096,17 +2104,17 @@ void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy ) Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0); } } -void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans ) +void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard ) { int m; assert( p->pFile == NULL ); p->pFile = fopen( pFileName, "wb" ); fputs( "p cnf \n", p->pFile ); - Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans ); + Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard ); for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ ) Exa4_ManGenMint( p, m, fOnlyAnd, fFancy ); rewind( p->pFile ); - fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses ); + fprintf( p->pFile, "p %cnf %d %d", fCard ? 'k' : 'c', p->nCnfVars, p->nCnfClauses ); fclose( p->pFile ); } @@ -2130,6 +2138,8 @@ static inline int Exa4_ManFindFanin( Exa4_Man_t * p, Vec_Int_t * vValues, int i, iVar = j; Count++; } + if ( Count != 1 ) + printf( "Fanin count is %d instead of %d.\n", Count, 1 ); assert( Count == 1 ); return iVar; } @@ -2268,21 +2278,27 @@ Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy ) SeeAlso [] ***********************************************************************/ -Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose ) +Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard ) { + extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose, int * pStatus ); Mini_Aig_t * pMini = NULL; abctime clkTotal = Abc_Clock(); Vec_Int_t * vValues = NULL; - char * pFileNameIn = "_temp_.cnf"; - char * pFileNameOut = "_temp_out.cnf"; + srand(time(NULL)); + int Status = 0, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF; + char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand ); + char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand ); Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose ); Exa_ManIsNormalized( vSimsIn, vSimsOut ); - Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans ); + Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard ); if ( fVerbose ) printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose ); if ( fVerbose ) printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn ); - vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose ); + if ( fCard ) + vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, TimeOut, fVerbose, &Status ); + else + vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose ); if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy ); //if ( vValues ) Exa4_ManPrintSolution( p, vValues, fFancy ); if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns ); @@ -2310,7 +2326,7 @@ void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars ) if ( (m >> i) & 1 ) Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i ); } - pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose ); + pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0 ); if ( pMini ) Mini_AigStop( pMini ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); @@ -2332,7 +2348,7 @@ void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ) Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i ); } assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) ); - pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose ); + pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard ); if ( pMini ) Mini_AigStop( pMini ); if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" ); Vec_WrdFree( vSimsIn ); @@ -2797,8 +2813,10 @@ Mini_Aig_t * Exa5_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn abctime clkTotal = Abc_Clock(); Mini_Aig_t * pMini = NULL; Vec_Int_t * vValues = NULL; - char * pFileNameIn = "_temp_.cnf"; - char * pFileNameOut = "_temp_out.cnf"; + srand(time(NULL)); + int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF; + char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand ); + char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand ); Exa5_Man_t * p = Exa5_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose ); Exa_ManIsNormalized( vSimsIn, vSimsOut ); Exa5_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans ); @@ -3717,8 +3735,9 @@ Mini_Aig_t * Exa6_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn Mini_Aig_t * pMini = NULL; abctime clkTotal = Abc_Clock(); Vec_Int_t * vValues = NULL; - char * pFileNameIn = "_temp_.cnf"; - char * pFileNameOut = "_temp_out.cnf"; + int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF; + char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand ); + char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand ); Exa6_Man_t * p = Exa6_ManAlloc( vSimsIn, vSimsOut, nIns, 1+nIns+nDivs, nOuts, nNodes, fVerbose ); Exa_ManIsNormalized( vSimsIn, vSimsOut ); Exa6_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans ); @@ -4016,8 +4035,9 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ) int nV = pPars->nVars + pPars->nNodes; word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); Vec_Int_t * vValues = NULL; - char * pFileNameIn = "_temp_.cnf"; - char * pFileNameOut = "_temp_out.cnf"; + int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF; + char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand ); + char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand ); int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize ); if ( pPars->fVerbose ) printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );