From 581f2e59721498880d20c85444c2358e6c7c97e9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Nov 2020 22:45:23 -0800 Subject: Improvements to the SAT solver. --- src/proof/cec/cecSatG2.c | 6 +++--- src/sat/glucose2/Glucose2.cpp | 15 +++++++++++---- src/sat/glucose2/Solver.h | 2 +- 3 files changed, 15 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 45f56cf0..80a4b853 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1196,7 +1196,7 @@ int Cec4_ManCandIterNext( Cec4_Man_t * p ) while ( Vec_IntSize(p->vCands) > 0 ) { int fStop, iCand = Vec_IntEntry( p->vCands, p->iPosRead ); - if ( fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID) ) + if ( (fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID)) ) Vec_IntWriteEntry( p->vCands, p->iPosWrite++, iCand ); if ( ++p->iPosRead == Vec_IntSize(p->vCands) ) { @@ -1273,7 +1273,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p ) int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose ) { abctime clk; - int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit; + int nBTLimit = (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit; int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2]; int UnsatConflicts[3] = {0}; if ( iObj1 < iObj0 ) @@ -1385,7 +1385,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords ); //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i ) // Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) ); - pCex = NULL;//sat_solver_read_cex( p->pSat ); + pCex = sat_solver_read_cex( p->pSat ); Vec_IntClear( p->vPat ); if ( pCex == NULL ) { diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp index f32d1210..aa3d361f 100644 --- a/src/sat/glucose2/Glucose2.cpp +++ b/src/sat/glucose2/Glucose2.cpp @@ -1153,6 +1153,13 @@ lbool Solver::search(int nof_conflicts) for (;;){ CRef confl = propagate(); + + // exact conflict limit + if ( !withinBudget() && confl != CRef_Undef ) { + lbdQueue.fastclear(); + cancelUntil(0); + return l_Undef; } + if (confl != CRef_Undef){ // CONFLICT @@ -1395,15 +1402,15 @@ printf("c ==================================[ Search Statistics (every %6d confl if (status == l_True){ - if( justUsage() && false ){ + if( justUsage() ){ assert(jheap.empty()); //JustModel.growTo(nVars()); - int i = 0; + int i = 0, j = 0; JustModel.push(toLit(0)); for (; i < trail.size(); i++) if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) ) - JustModel.push(trail[i]); - JustModel[0] = toLit(i); + JustModel.push(trail[i]), j++; + JustModel[0] = toLit(j); } else { // Extend & copy model: model.growTo(nVars()); diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h index ab73dbc5..26b3bdcb 100644 --- a/src/sat/glucose2/Solver.h +++ b/src/sat/glucose2/Solver.h @@ -546,7 +546,7 @@ inline int Solver::nClauses () const { return clauses.size(); } inline int Solver::nLearnts () const { return learnts.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } -inline int * Solver::getCex () const { return NULL; } +inline int * Solver::getCex () const { return (int*) &JustModel[0]; } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } inline void Solver::setDecisionVar(Var v, bool b) { -- cgit v1.2.3