summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAig.c2
-rw-r--r--src/aig/ivy/ivyFraig.c4
-rw-r--r--src/base/abci/abc.c54
-rw-r--r--src/base/abci/abcDar.c6
-rw-r--r--src/base/abci/abcIvy.c4
-rw-r--r--src/base/abci/abcQbf.c4
-rw-r--r--src/proof/fra/fra.h2
-rw-r--r--src/proof/fra/fraCec.c19
-rw-r--r--src/proof/int/intContain.c4
-rw-r--r--src/sat/bsat/satSolver.c18
-rw-r--r--src/sat/bsat/satSolver.h3
11 files changed, 89 insertions, 31 deletions
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 4099fe54..dbe396ab 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -572,7 +572,7 @@ int Gia_ManSolveSat( Gia_Man_t * p )
Aig_Man_t * pNew;
int RetValue;//, clk = clock();
pNew = Gia_ManToAig( p, 0 );
- RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 );
+ RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
if ( RetValue == 0 )
{
Gia_Obj_t * pObj;
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index d4cbd57a..9874a93c 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2923,14 +2923,14 @@ printf( "***************\n" );
***********************************************************************/
int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
{
- extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
+ extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Vec_Int_t * vLeaves;
Aig_Man_t * pMan;
Aig_Obj_t * pObj;
int i, RetValue;
vLeaves = Vec_IntAlloc( 100 );
pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
- RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 1 );
+ RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 0, 0, 0, 1 );
if ( RetValue == 0 )
{
int Counter = 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9d06104d..daf265e8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17692,7 +17692,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fPartition;
int fMiter;
- extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
+ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -17797,7 +17797,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform equivalence checking
if ( fSat && fMiter )
- Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose );
+ Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, 0, 0, 0, fVerbose );
else
Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
@@ -18943,10 +18943,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewSolver;
int fVerbose;
int nConfLimit;
+ int nStartLearned;
+ int nDeltaLearned;
+ int nRatioLearned;
int nInsLimit;
clock_t clk;
- extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
+ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
// set defaults
fAlignPol = 0;
fAndOuts = 0;
@@ -18954,8 +18957,11 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
nConfLimit = 0;
nInsLimit = 0;
+ nStartLearned = 0;
+ nDeltaLearned = 0;
+ nRatioLearned = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CISDRpanvh" ) ) != EOF )
{
switch ( c )
{
@@ -18981,6 +18987,39 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInsLimit < 0 )
goto usage;
break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nStartLearned = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nStartLearned < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nDeltaLearned = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nDeltaLearned < 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;
+ }
+ nRatioLearned = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nRatioLearned < 0 )
+ goto usage;
+ break;
case 'p':
fAlignPol ^= 1;
break;
@@ -19024,7 +19063,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
clk = clock();
- RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
+ RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
{
@@ -19046,11 +19085,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" );
+ Abc_Print( -2, "usage: dsat [-CISDR num] [-panvh]\n" );
Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
Abc_Print( -2, "\t derives CNF from the current network and leave it unchanged\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
+ Abc_Print( -2, "\t-S num : starting value for learned clause removal [default = %d]\n", nStartLearned );
+ Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nDeltaLearned );
+ Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", nRatioLearned );
Abc_Print( -2, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
Abc_Print( -2, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
Abc_Print( -2, "\t-n : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 75df783f..82656d98 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1403,7 +1403,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
SeeAlso []
***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue;//, clk = clock();
@@ -1411,7 +1411,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
assert( Abc_NtkLatchNum(pNtk) == 0 );
// assert( Abc_NtkPoNum(pNtk) == 1 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
- RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
+ RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
@@ -2056,7 +2056,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
if ( Aig_ManRegNum(pTemp) == 0 )
{
pTemp->pSeqModel = NULL;
- RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 );
+ RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 );
if ( pTemp->pData )
pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
// pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 2d53a1ee..ae75e9fc 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -533,7 +533,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
// if SAT only, solve without iteration
// RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
- RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
+ RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
// pNtk->pModel = Aig_ManReleaseData( pMan2 );
@@ -583,7 +583,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
}
- RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose );
+ RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
}
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 0b53bc8a..a77ddf94 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
-extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
+extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
// solve the synthesis instance
clkS = clock();
// RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
- RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 );
+ RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
clkS = clock() - clkS;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkSyn, vPiValues );
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 922a3c47..8be02e45 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -285,7 +285,7 @@ static inline int Fra_ImpCreate( int Left, int Right )
////////////////////////////////////////////////////////////////////////
/*=== fraCec.c ========================================================*/
-extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
+extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index f1f15155..0e483b1f 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
{
if ( fNewSolver )
{
@@ -75,7 +75,6 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
return 1;
}
-
if ( fAndOuts )
{
// assert each output independently
@@ -182,6 +181,14 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
return 1;
}
+ if ( nStartLearned )
+ pSat->nLearntStart = nStartLearned;
+ if ( nDeltaLearned )
+ pSat->nLearntDelta = nDeltaLearned;
+ if ( nRatioLearned )
+ pSat->nLearntRatio = nRatioLearned;
+ if ( fVerbose )
+ pSat->fVerbose = fVerbose;
if ( fAndOuts )
{
@@ -225,8 +232,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
// solve the miter
clk = clock();
- if ( fVerbose )
- pSat->verbosity = 1;
+// if ( fVerbose )
+// pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
@@ -303,7 +310,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
// if SAT only, solve without iteration
clk = clock();
- RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
+ RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
@@ -371,7 +378,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 )
{
clk = clock();
- RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0, 0 );
+ RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 8ed6624d..f10006b7 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -57,7 +57,7 @@ int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
RetValue = Fra_FraigMiterStatus( pAigTemp );
Aig_ManStop( pAigTemp );
-// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
+// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
}
assert( RetValue != -1 );
Aig_ManStop( pMiter );
@@ -88,7 +88,7 @@ int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
RetValue = Fra_FraigMiterStatus( pAigTemp );
Aig_ManStop( pAigTemp );
-// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
+// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
}
assert( RetValue != -1 );
Aig_ManStop( pMiter );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 2a759da3..7a703830 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -29,9 +29,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
-//#define LEARNT_MAX_START 0
-#define LEARNT_MAX_START 20000
-#define LEARNT_MAX_INCRE 1000
+//#define LEARNT_MAX_START_DEFAULT 0
+#define LEARNT_MAX_START_DEFAULT 20000
+#define LEARNT_MAX_INCRE_DEFAULT 1000
+#define LEARNT_MAX_RATIO_DEFAULT 50
#define SAT_USE_ANALYZE_FINAL
@@ -921,7 +922,11 @@ sat_solver* sat_solver_new(void)
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->binary = clause_read( s, s->hBinary );
- s->nLearntMax = LEARNT_MAX_START;
+ s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
+ s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
+ s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
+
+ s->nLearntMax = s->nLearntStart;
// initialize vectors
veci_new(&s->order);
@@ -1188,7 +1193,7 @@ void sat_solver_reducedb(sat_solver* s)
s->nDBreduces++;
// printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
- s->nLearntMax = LEARNT_MAX_START + LEARNT_MAX_INCRE * s->nDBreduces;
+ s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
// return;
// create sorting values
@@ -1205,7 +1210,7 @@ void sat_solver_reducedb(sat_solver* s)
CounterStart = nLearnedOld - (s->nLearntMax / 20);
// preserve 3/4 of most active clauses
- nSelected = nLearnedOld*5/10;
+ nSelected = nLearnedOld*s->nLearntRatio/100;
// find non-decreasing permutation
pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
@@ -1494,6 +1499,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
lbool status = l_Undef;
lit* i;
+ printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
////////////////////////////////////////////////
if ( s->fSolved )
{
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5215267b..8998b78c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -141,6 +141,9 @@ struct sat_solver_t
int fVerbose;
stats_t stats;
+ int nLearntStart; // starting learned clause limit
+ int nLearntDelta; // delta of learned clause limit
+ int nLearntRatio; // ratio percentage of learned clauses
int nLearntMax; // max number of learned clauses
int nDBreduces; // number of DB reductions
// veci learned; // contain learnt clause handles
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-08 16:25:03 +0000