From 89e1ee8bc94651f91d6262a5d5f2db7f2cd1f5e6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 3 Aug 2022 20:59:44 -0700 Subject: Improvements to command 'twoexact'. --- src/base/abci/abc.c | 12 ++++- src/sat/bmc/bmc.h | 4 ++ src/sat/bmc/bmcMaj.c | 127 ++++++++++++++++++++++++++++++++++++++++++++------- 3 files changed, 124 insertions(+), 19 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0414687e..eb6f6145 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8770,7 +8770,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, "INTaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTadcogvh" ) ) != EOF ) { switch ( c ) { @@ -8810,6 +8810,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fOnlyAnd ^= 1; break; + case 'd': + pPars->fDynConstr ^= 1; + break; + case 'c': + pPars->fDumpCnf ^= 1; + break; case 'o': pPars->fFewerVars ^= 1; break; @@ -8854,12 +8860,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INT ] [-aogvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INT ] [-adcogvh] \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 ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); + Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); 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-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 12439faa..4de0bd7d 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -54,6 +54,8 @@ struct Bmc_EsPar_t_ int fMajority; int fUseIncr; int fOnlyAnd; + int fDynConstr; + int fDumpCnf; int fGlucose; int fOrderNodes; int fEnumSols; @@ -73,6 +75,8 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fMajority = 0; pPars->fUseIncr = 0; pPars->fOnlyAnd = 0; + pPars->fDynConstr = 0; + pPars->fDumpCnf = 0; pPars->fGlucose = 0; pPars->fOrderNodes = 0; pPars->fEnumSols = 0; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index fc77398a..075288cd 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -422,6 +422,8 @@ struct Exa_Man_t_ int VarVals[MAJ_NOBJS]; // values of the first nVars variables Vec_Wec_t * vOutLits; // output vars bmcg_sat_solver * pSat; // SAT solver + FILE * pFile; + int nCnfClauses; }; static inline word * Exa_ManTruth( Exa_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); } @@ -502,10 +504,26 @@ Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) bmcg_sat_solver_set_nvars( p->pSat, p->iVar ); if ( pPars->RuntimeLim ) bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC ); + if ( pPars->fDumpCnf ) + { + char Buffer[1000]; + sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes ); + p->pFile = fopen( Buffer, "wb" ); + fputs( "p cnf \n", p->pFile ); + } return p; } void Exa_ManFree( Exa_Man_t * p ) { + if ( p->pFile ) + { + char Buffer[1000]; + sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes ); + rewind( p->pFile ); + fprintf( p->pFile, "p cnf %d %d", bmcg_sat_solver_varnum(p->pSat), p->nCnfClauses ); + fclose( p->pFile ); + printf( "CNF was dumped into file \"%s\".\n", Buffer ); + } bmcg_sat_solver_stop( p->pSat ); Vec_WrdFree( p->vInfo ); Vec_WecFree( p->vOutLits ); @@ -666,43 +684,115 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) SeeAlso [] ***********************************************************************/ -int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) +static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits ) +{ + int i; + if ( p->pFile ) + { + p->nCnfClauses++; + for ( i = 0; i < nLits; i++ ) + fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) ); + fprintf( p->pFile, "0\n" ); + } + return bmcg_sat_solver_addclause( p->pSat, pLits, nLits ); +} +int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded ) { int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; - // input constraints + *pnAdded = 0; for ( i = p->nVars; i < p->nObjs; i++ ) { - int iVarStart = 1 + 3*(i - p->nVars); for ( k = 0; k < 2; k++ ) { int nLits = 0; for ( j = 0; j < p->nObjs; j++ ) - if ( p->VarMarks[i][k][j] ) + if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) ) pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 ); assert( nLits > 0 ); // input uniqueness - if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) ) - return 0; for ( n = 0; n < nLits; n++ ) for ( m = n+1; m < nLits; m++ ) { + (*pnAdded)++; pLits2[0] = Abc_LitNot(pLits[n]); pLits2[1] = Abc_LitNot(pLits[m]); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) ) + if ( !Exa_ManAddClause( p, pLits2, 2 ) ) return 0; } if ( k == 1 ) break; // symmetry breaking - for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] ) - for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] ) + for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) ) + for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k+1][j]) ) { + (*pnAdded)++; pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 ); pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) ) + if ( !Exa_ManAddClause( p, pLits2, 2 ) ) return 0; } } + } + return 1; +} +int Exa_ManSolverSolve( Exa_Man_t * p ) +{ + int nAdded = 1; + while ( nAdded ) + { + int status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); + if ( status != GLUCOSE_SAT ) + return status; + status = Exa_ManAddCnfAdd( p, &nAdded ); + //printf( "Added %d clauses.\n", nAdded ); + if ( status != GLUCOSE_SAT ) + return status; + } + return GLUCOSE_SAT; +} +int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) +{ + int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; + // input constraints + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iVarStart = 1 + 3*(i - p->nVars); + for ( k = 0; k < 2; k++ ) + { + int nLits = 0; + for ( j = 0; j < p->nObjs; j++ ) + if ( p->VarMarks[i][k][j] ) + pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 ); + assert( nLits > 0 ); + if ( !Exa_ManAddClause( p, pLits, nLits ) ) + return 0; + // input uniqueness + if ( !p->pPars->fDynConstr ) + { + for ( n = 0; n < nLits; n++ ) + for ( m = n+1; m < nLits; m++ ) + { + pLits2[0] = Abc_LitNot(pLits[n]); + pLits2[1] = Abc_LitNot(pLits[m]); + if ( !Exa_ManAddClause( p, pLits2, 2 ) ) + return 0; + } + } + if ( k == 1 ) + break; + // symmetry breaking + if ( !p->pPars->fDynConstr ) + { + for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] ) + for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] ) + { + pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 ); + pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 ); + if ( !Exa_ManAddClause( p, pLits2, 2 ) ) + return 0; + } + } + } #ifdef USE_NODE_ORDER // node ordering for ( j = p->nVars; j < i; j++ ) @@ -711,7 +801,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) { pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 ); pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) ) + if ( !Exa_ManAddClause( p, pLits2, 2 ) ) return 0; } #endif @@ -721,7 +811,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) pLits[0] = Abc_Var2Lit( iVarStart, k==1 ); pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 ); pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) ) + if ( !Exa_ManAddClause( p, pLits, 3 ) ) return 0; } if ( fOnlyAnd ) @@ -729,7 +819,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) pLits[0] = Abc_Var2Lit( iVarStart, 1 ); pLits[1] = Abc_Var2Lit( iVarStart+1, 1 ); pLits[2] = Abc_Var2Lit( iVarStart+2, 0 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) ) + if ( !Exa_ManAddClause( p, pLits, 3 ) ) return 0; } } @@ -738,7 +828,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) { Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i); assert( Vec_IntSize(vArray) > 0 ); - if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) ) + if ( !Exa_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) ) ) return 0; } return 1; @@ -770,7 +860,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n ); else if ( p->VarVals[j] == n ) continue; - if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) ) + if ( !Exa_ManAddClause( p, pLits, nLits ) ) return 0; } } @@ -790,7 +880,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n ); if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n ); assert( nLits <= 4 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) ) + if ( !Exa_ManAddClause( p, pLits, nLits ) ) return 0; } } @@ -815,7 +905,10 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) abctime clk = Abc_Clock(); if ( !Exa_ManAddCnf( p, iMint ) ) break; - status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); + if ( pPars->fDynConstr ) + status = Exa_ManSolverSolve( p ); + else + status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); if ( pPars->fVerbose ) { printf( "Iter %3d : ", i ); -- cgit v1.2.3