summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-05-18 10:52:07 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-05-18 10:52:07 -0700
commit0328488bdf845b711f74d2e1a30cbab4f63de825 (patch)
treef53a86c28ce0fee1bfce8fa541bcac17c7e2bbdf
parent29ee997bb922974b13582532ea9e6dd80a48f928 (diff)
downloadabc-0328488bdf845b711f74d2e1a30cbab4f63de825.tar.gz
abc-0328488bdf845b711f74d2e1a30cbab4f63de825.tar.bz2
abc-0328488bdf845b711f74d2e1a30cbab4f63de825.zip
SAT variable profiling.
-rw-r--r--src/sat/bmc/bmcBmc3.c1
-rw-r--r--src/sat/bsat/satClause.h4
-rw-r--r--src/sat/bsat/satSolver.c12
-rw-r--r--src/sat/bsat/satSolver.h14
4 files changed, 28 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index b3a92950..8e314279 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1636,6 +1636,7 @@ 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( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Cnf =%7.0f. ",(double)p->pSat->stats.conflicts );
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 0b1756ff..6a034326 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 1000
-#define LEARNT_MAX_RATIO_DEFAULT 50
+#define LEARNT_MAX_INCRE_DEFAULT 2000
+#define LEARNT_MAX_RATIO_DEFAULT 80
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 8f3098d8..31d4b0df 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -466,6 +466,12 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
{
int v = lit_var(l);
+ if ( s->pFreqs[v] == 0 )
+// {
+ s->pFreqs[v] = 1;
+// s->nVarUsed++;
+// }
+
#ifdef VERBOSEDEBUG
printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
#endif
@@ -1033,6 +1039,8 @@ 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);
+
if ( s->factors )
s->factors = ABC_REALLOC(double, s->factors, s->cap);
s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
@@ -1054,6 +1062,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
#else
s->activity[var] = (1<<10);
#endif
+ s->pFreqs[var] = 0;
if ( s->factors )
s->factors [var] = 0;
// *((int*)s->vi + var) = 0; s->vi[var].val = varX;
@@ -1106,6 +1115,7 @@ void sat_solver_delete(sat_solver* s)
ABC_FREE(s->tags );
ABC_FREE(s->activity );
ABC_FREE(s->activity2);
+ ABC_FREE(s->pFreqs );
ABC_FREE(s->factors );
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
@@ -1321,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 );
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index acaceef9..e5ea1ba5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -121,6 +121,8 @@ struct sat_solver_t
unsigned* activity; // A heuristic measurement of the activity of a variable.
unsigned* activity2; // backup variable activity
#endif
+ char * pFreqs; // how many times this variable was assigned a value
+ int nVarUsed;
// varinfo * vi; // variable information
int* levels; //
@@ -248,6 +250,18 @@ static inline void sat_solver_bookmark(sat_solver* s)
}
}
+static inline int sat_solver_count_usedvars(sat_solver* s)
+{
+ int i, nVars = 0;
+ for ( i = 0; i < s->size; i++ )
+ if ( s->pFreqs[i] )
+ {
+ s->pFreqs[i] = 0;
+ nVars++;
+ }
+ return nVars;
+}
+
static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
{
lit Lits[1];