From f9da2c790f68462fd68924c94ecf6f02d442632a Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 18 May 2013 11:03:32 -0700
Subject: SAT variable profiling.
---
src/base/abci/abc.c | 40 ++++++++++++++++++++++++++++++++++++++--
src/sat/bmc/bmc.h | 3 +++
src/sat/bmc/bmcBmc3.c | 10 ++++++++--
src/sat/bsat/satClause.h | 4 ++--
src/sat/bsat/satSolver.c | 4 ++--
5 files changed, 53 insertions(+), 8 deletions(-)
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a30a2e55..62bed4c1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21246,7 +21246,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJILaxdruvzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLaxdruvzh" ) ) != EOF )
{
switch ( c )
{
@@ -21349,6 +21349,39 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nPisAbstract < 0 )
goto usage;
break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLearnedStart = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLearnedStart < 0 )
+ goto usage;
+ break;
+ case 'Q':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLearnedDelta = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLearnedDelta < 0 )
+ goto usage;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLearnedPerce = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLearnedPerce < 0 )
+ goto usage;
+ break;
case 'L':
if ( globalUtilOptind >= argc )
{
@@ -21433,7 +21466,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: bmc3 [-SFTHGCDJI num] [-L file] [-axduvzh]\n" );
+ Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-L file] [-axduvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@@ -21444,6 +21477,9 @@ usage:
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
+ Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
+ Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
+ Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 955cd79e..b5f07151 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -56,6 +56,9 @@ struct Saig_ParBmc_t_
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions
+ int nLearnedStart; // starting learned clause limit
+ int nLearnedDelta; // delta of learned clause limit
+ int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
int iFrame; // explored up to this frame
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 8e314279..e3fb8c68 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1314,6 +1314,9 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->nPisAbstract = 0; // the number of PIs to abstract
p->fSolveAll = 0; // stops on the first SAT instance
p->fDropSatOuts = 0; // replace sat outputs by constant 0
+ p->nLearnedStart = 10000; // starting learned clause limit
+ p->nLearnedDelta = 2000; // delta of learned clause limit
+ p->nLearnedPerce = 80; // ratio of learned clause limit
p->fVerbose = 0; // verbose
p->fNotVerbose = 0; // skip line-by-line print-out
p->iFrame = -1; // explored up to this frame
@@ -1404,6 +1407,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
p->pPars = pPars;
+ p->pSat->nLearntStart = p->pPars->nLearnedStart;
+ p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
+ p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
if ( pPars->fVerbose )
{
printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n",
@@ -1636,9 +1642,9 @@ nTimeUndec += clock() - clk2;
}
printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
printf( "Var =%8.0f. ", (double)p->nSatVars );
- printf( "Var2 =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
+ printf( "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
- printf( "Cnf =%7.0f. ",(double)p->pSat->stats.conflicts );
+ printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
if ( pPars->fSolveAll )
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 6a034326..0b1756ff 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -35,8 +35,8 @@ ABC_NAMESPACE_HEADER_START
//#define LEARNT_MAX_START_DEFAULT 0
#define LEARNT_MAX_START_DEFAULT 10000
-#define LEARNT_MAX_INCRE_DEFAULT 2000
-#define LEARNT_MAX_RATIO_DEFAULT 80
+#define LEARNT_MAX_INCRE_DEFAULT 1000
+#define LEARNT_MAX_RATIO_DEFAULT 50
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 31d4b0df..50df6a84 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1039,7 +1039,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
#endif
- s->pFreqs = ABC_REALLOC(char, s->tags, s->cap);
+ s->pFreqs = ABC_REALLOC(char, s->pFreqs, s->cap);
if ( s->factors )
s->factors = ABC_REALLOC(double, s->factors, s->cap);
@@ -1331,7 +1331,7 @@ void sat_solver_reducedb(sat_solver* s)
// report the results
TimeTotal += clock() - clk;
-// if ( s->fVerbose )
+ if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
--
cgit v1.2.3