From 8982bf58cb8c801bdd6e204d73ac6ed36d98adaa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Jul 2012 22:31:00 -0700 Subject: Reducing memory usage in proof-based abstraction. --- src/sat/bsat/satProof2.h | 326 ++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bsat/satSolver2.c | 89 +++++++++---- src/sat/bsat/satSolver2.h | 8 +- 3 files changed, 393 insertions(+), 30 deletions(-) create mode 100644 src/sat/bsat/satProof2.h (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h new file mode 100644 index 00000000..82ed9264 --- /dev/null +++ b/src/sat/bsat/satProof2.h @@ -0,0 +1,326 @@ +/**CFile**************************************************************** + + FileName [satProof2.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver.] + + Synopsis [Proof logging.] + + Author [Alan Mishchenko ] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__sat__bsat__satProof2_h +#define ABC__sat__bsat__satProof2_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "misc/vec/vec.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Prf_Man_t_ Prf_Man_t; +struct Prf_Man_t_ +{ + int iFirst; // first learned clause with proof + int iFirst2; // first learned clause with proof + int nWords; // the number of proof words + word * pInfo; // pointer to the current proof + Vec_Wrd_t * vInfo; // proof information + Vec_Int_t * vSaved; // IDs of saved clauses + Vec_Int_t * vId2Pr; // mapping proof IDs of problem clauses into bitshifts (user's array) +}; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Prf_BitWordNum( int nWidth ) { return (nWidth >> 6) + ((nWidth & 63) > 0); } +static inline int Prf_ManSize( Prf_Man_t * p ) { return Vec_WrdSize( p->vInfo ) / p->nWords; } +static inline void Prf_ManClearNewInfo( Prf_Man_t * p ) { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); } +static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Prf_Man_t * Prf_ManAlloc() +{ + Prf_Man_t * p; + p = ABC_CALLOC( Prf_Man_t, 1 ); + p->iFirst = -1; + p->iFirst2 = -1; + p->vInfo = Vec_WrdAlloc( 1000 ); + p->vSaved = Vec_IntAlloc( 1000 ); + return p; +} +static inline void Prf_ManStop( Prf_Man_t * p ) +{ + if ( p == NULL ) + return; + Vec_IntFree( p->vSaved ); + Vec_WrdFree( p->vInfo ); + ABC_FREE( p ); +} +static inline void Prf_ManStopP( Prf_Man_t ** p ) +{ + Prf_ManStop( *p ); + *p = NULL; +} +static inline double Prf_ManMemory( Prf_Man_t * p ) +{ + return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth ) +{ + assert( p->iFirst == -1 ); + p->iFirst = iFirst; + p->nWords = Prf_BitWordNum( nWidth ); + p->vId2Pr = vId2Pr; + p->pInfo = NULL; + Vec_WrdClear( p->vInfo ); +} +static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth ) +{ + Vec_Wrd_t * vInfoNew; + int i, w, nSize, nWordsNew; + assert( p->iFirst >= 0 ); + assert( p->pInfo == NULL ); + if ( nWidth < 64 * p->nWords ) + return; + // get word count after resizing + nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords ); + // remap the entries + nSize = Prf_ManSize( p ); + vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew ); + for ( i = 0; i < nSize; i++ ) + { + p->pInfo = Prf_ManClauseInfo( p, i ); + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( vInfoNew, p->pInfo[w] ); + for ( ; w < nWordsNew; w++ ) + Vec_WrdPush( vInfoNew, 0 ); + } + Vec_WrdFree( p->vInfo ); + p->vInfo = vInfoNew; + p->nWords = nWordsNew; + p->pInfo = NULL; + +} +static inline void Prf_ManShrink( Prf_Man_t * p, int iClause ) +{ + assert( p->iFirst >= 0 ); + assert( iClause - p->iFirst >= 0 ); + assert( iClause - p->iFirst < Prf_ManSize(p) ); + Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew ) +{ + assert( p->iFirst >= 0 ); + if ( i < p->iFirst ) + return; + if ( Vec_IntSize(p->vSaved) == 0 ) + { + assert( p->iFirst2 == -1 ); + p->iFirst2 = iNew; + } + Vec_IntPush( p->vSaved, i ); +} +static inline void Prf_ManCompact( Prf_Man_t * p, int iNew ) +{ + int i, w, k = 0, Entry, nSize; + assert( p->iFirst >= 0 ); + assert( p->pInfo == NULL ); + nSize = Prf_ManSize( p ); + Vec_IntForEachEntry( p->vSaved, Entry, i ) + { + assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize ); + p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst ); + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] ); + } + Vec_WrdShrink( p->vInfo, k ); + Vec_IntClear( p->vSaved ); + p->pInfo = NULL; + // update first + if ( p->iFirst2 == -1 ) + p->iFirst = iNew; + else + p->iFirst = p->iFirst2; + p->iFirst2 = -1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c ) +{ + assert( p->iFirst >= 0 ); + assert( p->pInfo != NULL ); + // add to proof info + if ( c->lrn ) // learned clause + { + if ( clause_id(c) >= p->iFirst ) + { + word * pProofStart; + int w; + assert( clause_id(c) - p->iFirst >= 0 ); + assert( clause_id(c) - p->iFirst < Prf_ManSize(p) ); + pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst ); + for ( w = 0; w < p->nWords; w++ ) + p->pInfo[w] |= pProofStart[w]; + } + } + else // problem clause + { + if ( clause_id(c) ) // has proof ID + { + int Entry; + if ( p->vId2Pr == NULL ) + Entry = clause_id(c); + else + Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) ); + if ( Entry >= 0 ) + { + assert( Entry < 64 * p->nWords ); + Abc_InfoSetBit( (unsigned *)p->pInfo, Entry ); + } + } + } +} +static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c ) +{ + assert( p->iFirst >= 0 ); + // prepare info for new clause + Prf_ManClearNewInfo( p ); + // get pointer to the proof + assert( p->pInfo == NULL ); + p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 ); + // add to proof info + Prf_ManChainResolve( p, c ); +} +static inline int Prf_ManChainStop( Prf_Man_t * p ) +{ + assert( p->pInfo != NULL ); + p->pInfo = NULL; + return 0; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p ) +{ + Vec_Int_t * vCore; + int i, Entry; + assert( p->iFirst >= 0 ); + assert( p->pInfo == NULL ); + vCore = Vec_IntAlloc( 64 * p->nWords ); + p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 ); + if ( p->vId2Pr == NULL ) + { + for ( i = 0; i < 64 * p->nWords; i++ ) + if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) ) + Vec_IntPush( vCore, i ); + } + else + { + Vec_IntForEachEntry( p->vId2Pr, Entry, i ) + { + if ( Entry < 0 ) + continue; + assert( Entry < 64 * p->nWords ); + if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) ) + Vec_IntPush( vCore, i ); + } + } + p->pInfo = NULL; + Vec_IntSort( vCore, 1 ); + return vCore; +} + + + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index b84f5a5f..6662eca5 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -161,7 +161,11 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l static inline void proof_chain_start( sat_solver2* s, clause* c ) { - if ( s->fProofLogging ) + if ( !s->fProofLogging ) + return; + if ( s->pPrf2 ) + Prf_ManChainStart( s->pPrf2, c ); + if ( s->pPrf1 ) { int ProofId = clause2_proofid(s, c, 0); assert( (ProofId >> 2) > 0 ); @@ -174,7 +178,14 @@ static inline void proof_chain_start( sat_solver2* s, clause* c ) static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { - if ( s->fProofLogging ) + if ( !s->fProofLogging ) + return; + if ( s->pPrf2 ) + { + clause* c = cls ? cls : var_unit_clause( s, Var ); + Prf_ManChainResolve( s->pPrf2, c ); + } + if ( s->pPrf1 ) { clause* c = cls ? cls : var_unit_clause( s, Var ); int ProofId = clause2_proofid(s, c, var_is_partA(s,Var)); @@ -185,11 +196,15 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) static inline int proof_chain_stop( sat_solver2* s ) { - if ( s->fProofLogging ) + if ( !s->fProofLogging ) + return 0; + if ( s->pPrf2 ) + Prf_ManChainStop( s->pPrf2 ); + if ( s->pPrf1 ) { extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ); - int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) ); - Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 ); + int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) ); + Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 ); return h; } return 0; @@ -371,7 +386,7 @@ static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c ) return lbd; } -static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id) +static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id ) { clause* c; int h, size = end - begin; @@ -385,11 +400,11 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, c = clause2_read( s, h ); if (learnt) { - if ( s->fProofLogging ) + if ( s->pPrf1 ) assert( proof_id ); c->lbd = sat_clause_compute_lbd( s, c ); assert( clause_id(c) == veci_size(&s->act_clas) ); - if ( proof_id ) + if ( s->pPrf1 ) veci_push(&s->claProofs, proof_id); // veci_push(&s->act_clas, (1<<10)); veci_push(&s->act_clas, 0); @@ -674,7 +689,8 @@ static int solver2_lit_removable(sat_solver2* s, int x) while (veci_size(&s->stack)) { x = veci_pop(&s->stack); - if ( s->fProofLogging ){ + if ( s->fProofLogging ) + { if ( x & 1 ){ if ( var_tag(s,x >> 1) & 1 ) veci_push(&s->min_lit_order, x >> 1 ); @@ -910,7 +926,8 @@ clause* solver2_propagate(sat_solver2* s) // Did not find watch -- clause is unit under assignment: Lit = lits[0]; - if (s->fProofLogging && solver2_dlevel(s) == 0){ + if ( s->fProofLogging && solver2_dlevel(s) == 0 ) + { int k, x, proof_id, Cid, Var = lit_var(Lit); int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit)); // Log production of top-level unit clause: @@ -990,7 +1007,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) s->stats.conflicts++; conflictC++; if (solver2_dlevel(s) <= s->root_level){ proof_id = solver2_analyze_final(s, confl, 0); - assert( proof_id > 0 ); + if ( s->pPrf1 ) + assert( proof_id > 0 ); s->hProofLast = proof_id; veci_delete(&learnt_clause); return l_False; @@ -1112,12 +1130,11 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->min_lit_order); veci_new(&s->min_step_order); // veci_new(&s->learnt_live); - Sat_MemAlloc_( &s->Mem, 14 ); veci_new(&s->act_clas); + // proof-logging veci_new(&s->claProofs); - if ( s->fProofLogging ) - Vec_SetAlloc_( &s->Proofs, 20 ); +// s->pPrf1 = Vec_SetAlloc( 20 ); // initialize clause pointers s->hLearntLast = -1; // the last learnt clause @@ -1218,7 +1235,8 @@ void sat_solver2_delete(sat_solver2* s) // veci_delete(&s->lrns); Sat_MemFree_( &s->Mem ); // veci_delete(&s->proofs); - Vec_SetFree_( &s->Proofs ); + Vec_SetFree( s->pPrf1 ); + Prf_ManStop( s->pPrf2 ); // delete arrays if (s->vi != 0){ @@ -1424,7 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s) // mark learned clauses to remove Counter = j = 0; - pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; + pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL; Sat_MemForEachLearned( pMem, c, i, k ) { assert( c->mark == 0 ); @@ -1432,7 +1450,9 @@ void sat_solver2_reducedb(sat_solver2* s) { pSortValues[j] = pSortValues[clause_id(c)]; if ( pClaProofs ) - pClaProofs[j] = pClaProofs[clause_id(c)]; + pClaProofs[j] = pClaProofs[clause_id(c)]; + if ( s->pPrf2 ) + Prf_ManAddSaved( s->pPrf2, clause_id(c), j ); j++; } else // delete @@ -1443,13 +1463,15 @@ void sat_solver2_reducedb(sat_solver2* s) } } ABC_FREE( pSortValues ); + if ( s->pPrf2 ) + Prf_ManCompact( s->pPrf2, j ); // if ( j == nLearnedOld ) // return; assert( s->stats.learnts == (unsigned)j ); assert( Counter == nLearnedOld ); veci_resize(&s->act_clas,j); - if ( s->fProofLogging ) + if ( veci_size(&s->claProofs) ) veci_resize(&s->claProofs,j); // update ID of each clause to be its new handle @@ -1508,8 +1530,8 @@ void sat_solver2_reducedb(sat_solver2* s) assert( Counter == (int)s->stats.learnts ); // compact proof (compacts 'proofs' and update 'claProofs') - if ( s->fProofLogging ) - s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + if ( s->pPrf1 ) + s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot ); // report the results @@ -1531,7 +1553,7 @@ void sat_solver2_rollback( sat_solver2* s ) Count++; assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); - assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) ); + assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) ); // reset implication queue solver2_canceluntil_rollback( s, s->iTrailPivot ); // update order @@ -1568,14 +1590,17 @@ void sat_solver2_rollback( sat_solver2* s ) // resize learned arrays veci_resize(&s->act_clas, s->stats.learnts); - if ( s->fProofLogging ) + if ( s->pPrf1 ) { veci_resize(&s->claProofs, s->stats.learnts); // Vec_SetShrink(&s->Proofs, s->hProofPivot); // some weird bug here, which shows only on 64-bits! // temporarily, perform more general proof reduction - Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot ); } + assert( s->pPrf2 == NULL ); +// if ( s->pPrf2 ) +// Prf_ManShrink( s->pPrf2, s->stats.learnts ); // initialize other vars s->size = s->iVarPivot; @@ -1641,8 +1666,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) #else Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity ); #endif -// if ( s->factors ) -// Mem += s->cap * sizeof(double); // ABC_FREE(s->factors ); Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail ); Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos ); Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); @@ -1659,12 +1682,15 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->min_step_order.cap * sizeof(int); Mem += s->temp_proof.cap * sizeof(int); Mem += Sat_MemMemoryAll( &s->Mem ); -// Mem += Vec_ReportMemory( &s->Proofs ); +// Mem += Vec_ReportMemory( s->pPrf1 ); return Mem; } double sat_solver2_memory_proof( sat_solver2* s ) { - return Vec_ReportMemory( &s->Proofs ); + double Mem = s->dPrfMemory; + if ( s->pPrf1 ) + Mem += Vec_ReportMemory( s->pPrf1 ); + return Mem; } @@ -1911,7 +1937,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim void * Sat_ProofCore( sat_solver2 * s ) { extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot ); - return Proof_DeriveCore( &s->Proofs, s->hProofLast ); + if ( s->pPrf1 ) + return Proof_DeriveCore( s->pPrf1, s->hProofLast ); + if ( s->pPrf2 ) + { + s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) ); + return Prf_ManUnsatCore( s->pPrf2 ); + } + return NULL; } ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 81ecea76..1682ab6e 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satVec.h" #include "satClause.h" #include "misc/vec/vecSet.h" +#include "satProof2.h" ABC_NAMESPACE_HEADER_START @@ -147,10 +148,12 @@ struct sat_solver2_t veci learnt_live; // remaining clauses after reduce DB // proof logging - Vec_Set_t Proofs; // sequence of proof records + Vec_Set_t * pPrf1; // sequence of proof records veci temp_proof; // temporary place to store proofs int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + Prf_Man_t * pPrf2; // another proof manager + double dPrfMemory; // memory used by the proof-logger // statistics stats_t stats; @@ -234,7 +237,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s) assert( s->qhead == s->qtail ); s->iVarPivot = s->size; s->iTrailPivot = s->qhead; - s->hProofPivot = Vec_SetHandCurrent(&s->Proofs); + if ( s->pPrf1 ) + s->hProofPivot = Vec_SetHandCurrent(s->pPrf1); Sat_MemBookMark( &s->Mem ); } -- cgit v1.2.3