diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 12:35:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 12:35:29 -0700 |
| commit | c83e1d906a427aa8a60b17e988520db3528ba595 (patch) | |
| tree | cc525d070ff2b21778fb1a762bbbad51284dc221 /src/sat/bmc/bmcBmc2.c | |
| parent | 5766472bb6e88b68cb1a4f770bb82f81501442e9 (diff) | |
| download | abc-c83e1d906a427aa8a60b17e988520db3528ba595.tar.gz abc-c83e1d906a427aa8a60b17e988520db3528ba595.tar.bz2 abc-c83e1d906a427aa8a60b17e988520db3528ba595.zip | |
SAT variable profiling.
Diffstat (limited to 'src/sat/bmc/bmcBmc2.c')
| -rw-r--r-- | src/sat/bmc/bmcBmc2.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c index 0f55f7ce..658010c0 100644 --- a/src/sat/bmc/bmcBmc2.c +++ b/src/sat/bmc/bmcBmc2.c @@ -304,6 +304,10 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, // create SAT solver p->nSatVars = 1; p->pSat = sat_solver_new(); + p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart; + p->pSat->nLearntDelta = 5000;//p->pPars->nLearnedDelta; + p->pSat->nLearntRatio = 75;//p->pPars->nLearnedPerce; + p->pSat->nLearntMax = p->pSat->nLearntStart; sat_solver_setnvars( p->pSat, 2000 ); Lit = toLit( p->nSatVars ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); |