diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 12:45:46 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 12:45:46 -0700 |
commit | b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4 (patch) | |
tree | 9e5e3e6aebf36d28cf3c7726ac7f5f7bcdd8a843 /src/sat/bsat/satSolver2.c | |
parent | 5f3ba152e5729824f78fd03e3d164de81a452d22 (diff) | |
download | abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.gz abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.bz2 abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.zip |
Improvements in the proof-logging SAT solver.
Diffstat (limited to 'src/sat/bsat/satSolver2.c')
-rw-r--r-- | src/sat/bsat/satSolver2.c | 609 |
1 files changed, 302 insertions, 307 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 58ea531c..0bca05ed 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -30,9 +30,11 @@ ABC_NAMESPACE_IMPL_START #define SAT_USE_PROOF_LOGGING +static int Time = 0; + //================================================================================================= // Debug: - + //#define VERBOSEDEBUG // For derivation output (verbosity level 2) @@ -136,28 +138,19 @@ static inline void solver2_clear_marks(sat_solver2* s) { //================================================================================================= // Clause datatype + minor functions: -static inline satset* clause2_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); } -static inline cla clause2_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; } -static inline int clause2_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); } -static inline int clause2_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; } -static inline int clause2_is_used(sat_solver2* s, cla h) { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot); } - //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; } //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } -//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL; } +//static inline clause* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL; } //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; } static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } -static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause2_read(s, s->units[v]); } +static inline clause* var_unit_clause(sat_solver2* s, int v) { return clause2_read(s, s->units[v]); } static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } -//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } -// these two only work after creating a clause before the solver is called -int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; } -void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; } -int clause2_id(sat_solver2* s, int h) { return clause2_read(s, h)->Id; } +#define clause_foreach_var( p, var, i, start ) \ + for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ ) //================================================================================================= // Simple helpers: @@ -168,7 +161,7 @@ static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l //================================================================================================= // Proof logging: -static inline void proof_chain_start( sat_solver2* s, satset* c ) +static inline void proof_chain_start( sat_solver2* s, clause* c ) { if ( s->fProofLogging ) { @@ -181,11 +174,11 @@ static inline void proof_chain_start( sat_solver2* s, satset* c ) } } -static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) +static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { if ( s->fProofLogging ) { - satset* c = cls ? cls : var_unit_clause( s, Var ); + clause* c = cls ? cls : var_unit_clause( s, Var ); int ProofId = clause2_proofid(s, c, var_is_partA(s,Var)); assert( ProofId > 0 ); veci_push( &s->temp_proof, ProofId ); @@ -196,9 +189,9 @@ static inline int proof_chain_stop( sat_solver2* s ) { if ( s->fProofLogging ) { + 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) ); - satset * c = (satset *)Vec_SetEntry( &s->Proofs, h ); - c->nEnts = veci_size(&s->temp_proof) - 2; + Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 ); return h; } return 0; @@ -292,12 +285,12 @@ static inline void act_var_rescale(sat_solver2* s) { s->var_inc *= 1e-100; } static inline void act_clause2_rescale(sat_solver2* s) { - static int Total = 0; - float * claActs = (float *)veci_begin(&s->claActs); + static clock_t Total = 0; + float * act_clas = (float *)veci_begin(&s->act_clas); int i; clock_t clk = clock(); - for (i = 0; i < veci_size(&s->claActs); i++) - claActs[i] *= (float)1e-20; + for (i = 0; i < veci_size(&s->act_clas); i++) + act_clas[i] *= (float)1e-20; s->cla_inc *= (float)1e-20; Total += clock() - clk; @@ -311,11 +304,11 @@ static inline void act_var_bump(sat_solver2* s, int v) { if (s->orderpos[v] != -1) order_update(s,v); } -static inline void act_clause2_bump(sat_solver2* s, satset*c) { - float * claActs = (float *)veci_begin(&s->claActs); - assert( c->Id < veci_size(&s->claActs) ); - claActs[c->Id] += s->cla_inc; - if (claActs[c->Id] > (float)1e20) +static inline void act_clause2_bump(sat_solver2* s, clause*c) { + float * act_clas = (float *)veci_begin(&s->act_clas); + assert( c->Id < veci_size(&s->act_clas) ); + act_clas[c->Id] += s->cla_inc; + if (act_clas[c->Id] > (float)1e20) act_clause2_rescale(s); } static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; } @@ -332,14 +325,14 @@ static inline void act_var_rescale(sat_solver2* s) { s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); } static inline void act_clause2_rescale(sat_solver2* s) { -// static int Total = 0; - int i;//, clk = clock(); - unsigned * claActs = (unsigned *)veci_begin(&s->claActs); - for (i = 1; i < veci_size(&s->claActs); i++) - claActs[i] >>= 14; +// static clock_t Total = 0; +// clock_t clk = clock(); + int i; + unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas); + for (i = 0; i < veci_size(&s->act_clas); i++) + act_clas[i] >>= 14; s->cla_inc >>= 14; s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); - // Total += clock() - clk; // Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); // Abc_PrintTime( 1, "Time", Total ); @@ -351,11 +344,12 @@ static inline void act_var_bump(sat_solver2* s, int v) { if (s->orderpos[v] != -1) order_update(s,v); } -static inline void act_clause2_bump(sat_solver2* s, satset*c) { - unsigned * claActs = (unsigned *)veci_begin(&s->claActs); - assert( c->Id > 0 && c->Id < veci_size(&s->claActs) ); - claActs[c->Id] += s->cla_inc; - if (claActs[c->Id] & 0x80000000) +static inline void act_clause2_bump(sat_solver2* s, clause*c) { + unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas); + int Id = clause_id(c); + assert( Id >= 0 && Id < veci_size(&s->act_clas) ); + act_clas[Id] += s->cla_inc; + if (act_clas[Id] & 0x80000000) act_clause2_rescale(s); } static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); } @@ -366,89 +360,61 @@ static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc //================================================================================================= // Clause functions: +static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c ) +{ + int i, lev, minl = 0, lbd = 0; + for (i = 0; i < (int)c->size; i++) { + lev = var_level(s, lit_var(c->lits[i])); + if ( !(minl & (1 << (lev & 31))) ) { + minl |= 1 << (lev & 31); + lbd++; + } + } + return lbd; +} + static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id) { - satset* c; - int i, Cid, nLits = end - begin; - assert(nLits < 1 || begin[0] >= 0); - assert(nLits < 2 || begin[1] >= 0); - assert(nLits < 1 || lit_var(begin[0]) < s->size); - assert(nLits < 2 || lit_var(begin[1]) < s->size); - // add memory if needed - - // assign clause ID - if ( learnt ) + clause* c; + int h, size = end - begin; + assert(size < 1 || begin[0] >= 0); + assert(size < 2 || begin[1] >= 0); + assert(size < 1 || lit_var(begin[0]) < s->size); + assert(size < 2 || lit_var(begin[1]) < s->size); + // create new clause + h = Sat_MemAppend( &s->Mem, begin, size, learnt, 1 ); + assert( !(h & 1) ); + c = clause2_read( s, h ); + if (learnt) { - if ( veci_size(&s->learnts) + satset_size(nLits) > s->learnts.cap ) - { - int nMemAlloc = s->learnts.cap ? 2 * s->learnts.cap : (1 << 20); - s->learnts.ptr = ABC_REALLOC( int, veci_begin(&s->learnts), nMemAlloc ); - // Abc_Print(1, "Reallocing from %d to %d...\n", s->learnts.cap, nMemAlloc ); - s->learnts.cap = nMemAlloc; - if ( veci_size(&s->learnts) == 0 ) - veci_push( &s->learnts, -1 ); - } - // create clause - c = (satset*)(veci_begin(&s->learnts) + veci_size(&s->learnts)); - ((int*)c)[0] = 0; - c->learnt = learnt; - c->nEnts = nLits; - for (i = 0; i < nLits; i++) - c->pEnts[i] = begin[i]; - // count the clause - s->stats.learnts++; - s->stats.learnts_literals += nLits; - c->Id = s->stats.learnts; - assert( c->Id == veci_size(&s->claActs) ); - veci_push(&s->claActs, 0); + if ( s->fProofLogging ) + assert( proof_id ); + c->lbd = sat_clause_compute_lbd( s, c ); + assert( clause_id(c) == veci_size(&s->act_clas) ); if ( proof_id ) veci_push(&s->claProofs, proof_id); - if ( nLits > 2 ) +// veci_push(&s->act_clas, (1<<10)); + veci_push(&s->act_clas, 0); + if ( size > 2 ) act_clause2_bump( s,c ); - // extend storage - Cid = (veci_size(&s->learnts) << 1) | 1; - s->learnts.size += satset_size(nLits); - assert( veci_size(&s->learnts) <= s->learnts.cap ); - assert(((ABC_PTRUINT_T)c & 3) == 0); -// Abc_Print(1, "Clause for proof %d: ", proof_id ); -// satset_print( c ); + s->stats.learnts++; + s->stats.learnts_literals += size; // remember the last one - s->hLearntLast = Cid; + s->hLearntLast = h; } else { - if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap ) - { - int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); - s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); - // Abc_Print(1, "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); - s->clauses.cap = nMemAlloc; - if ( veci_size(&s->clauses) == 0 ) - veci_push( &s->clauses, -1 ); - } - // create clause - c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); - ((int*)c)[0] = 0; - c->learnt = learnt; - c->nEnts = nLits; - for (i = 0; i < nLits; i++) - c->pEnts[i] = begin[i]; - // count the clause + assert( clause_id(c) == (int)s->stats.clauses ); s->stats.clauses++; - s->stats.clauses_literals += nLits; - c->Id = s->stats.clauses; - // extend storage - Cid = (veci_size(&s->clauses) << 1); - s->clauses.size += satset_size(nLits); - assert( veci_size(&s->clauses) <= s->clauses.cap ); - assert(((ABC_PTRUINT_T)c & 3) == 0); + s->stats.clauses_literals += size; } // watch the clause - if ( nLits > 1 ){ - veci_push(solver2_wlist(s,lit_neg(begin[0])),Cid); - veci_push(solver2_wlist(s,lit_neg(begin[1])),Cid); + if ( size > 1 ) + { + veci_push(solver2_wlist(s,lit_neg(begin[0])),h); + veci_push(solver2_wlist(s,lit_neg(begin[1])),h); } - return Cid; + return h; } //================================================================================================= @@ -472,17 +438,6 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from) s->reasons[v] = from; // = from << 1; s->trail[s->qtail++] = l; order_assigned(s, v); -/* - if ( solver2_dlevel(s) == 0 ) - { - satset * c = from ? clause2_read( s, from ) : NULL; - Abc_Print(1, "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) ); - if ( c ) - satset_print( c ); - else - Abc_Print(1, "<none>\n" ); - } -*/ return true; } } @@ -589,7 +544,7 @@ static double solver2_progress(sat_solver2* s) | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ /* -void Solver::analyzeFinal(satset* confl, bool skip_first) +void Solver::analyzeFinal(clause* confl, bool skip_first) { // -- NOTE! This code is relatively untested. Please report bugs! conflict.clear(); @@ -628,7 +583,7 @@ void Solver::analyzeFinal(satset* confl, bool skip_first) } */ -static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) +static int solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first) { int i, j, x;//, start; veci_resize(&s->conf_final,0); @@ -636,7 +591,7 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) return s->hProofLast; proof_chain_start( s, conf ); assert( veci_size(&s->tagged) == 0 ); - satset_foreach_var( conf, x, i, skip_first ){ + clause_foreach_var( conf, x, i, skip_first ){ if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -647,10 +602,10 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ x = lit_var(s->trail[i]); if (var_tag(s,x)){ - satset* c = clause2_read(s, var_reason(s,x)); + clause* c = clause2_read(s, var_reason(s,x)); if (c){ proof_chain_resolve( s, c, x ); - satset_foreach_var( c, x, j, 1 ){ + clause_foreach_var( c, x, j, 1 ){ if ( var_level(s,x) ) var_set_tag(s, x, 1); else @@ -672,7 +627,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) // tag[1]: Processed by this procedure // tag[2]: 0=non-removable, 1=removable - satset* c; + clause* c; int i, x; // skip visited @@ -686,7 +641,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) return 0; } - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if (var_tag(s,x) & 1) solver2_lit_removable_rec(s, x); else{ @@ -706,7 +661,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) static int solver2_lit_removable(sat_solver2* s, int x) { - satset* c; + clause* c; int i, top; if ( !var_reason(s,x) ) return 0; @@ -731,7 +686,7 @@ static int solver2_lit_removable(sat_solver2* s, int x) } x >>= 1; c = clause2_read(s, var_reason(s,x)); - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if (var_tag(s,x) || !var_level(s,x)) continue; if (!var_reason(s,x) || !var_lev_mark(s,x)){ @@ -747,7 +702,7 @@ static int solver2_lit_removable(sat_solver2* s, int x) static void solver2_logging_order(sat_solver2* s, int x) { - satset* c; + clause* c; int i; if ( (var_tag(s,x) & 4) ) return; @@ -766,7 +721,7 @@ static void solver2_logging_order(sat_solver2* s, int x) c = clause2_read(s, var_reason(s,x)); // if ( !c ) // Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" ); - satset_foreach_var( c, x, i, 1 ){ + clause_foreach_var( c, x, i, 1 ){ if ( !var_level(s,x) || (var_tag(s,x) & 1) ) continue; veci_push(&s->stack, x << 1); @@ -777,19 +732,19 @@ static void solver2_logging_order(sat_solver2* s, int x) static void solver2_logging_order_rec(sat_solver2* s, int x) { - satset* c; + clause* c; int i, y; if ( (var_tag(s,x) & 8) ) return; c = clause2_read(s, var_reason(s,x)); - satset_foreach_var( c, y, i, 1 ) + clause_foreach_var( c, y, i, 1 ) if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 ) solver2_logging_order_rec(s, y); var_add_tag(s, x, 8); veci_push(&s->min_step_order, x); } -static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) +static int solver2_analyze(sat_solver2* s, clause* c, veci* learnt) { int cnt = 0; lit p = 0; @@ -805,9 +760,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) veci_push(learnt,lit_Undef); while ( 1 ){ assert(c != 0); - if (c->learnt) + if (c->lrn) act_clause2_bump(s,c); - satset_foreach_var( c, x, j, (int)(p > 0) ){ + clause_foreach_var( c, x, j, (int)(p > 0) ){ assert(x >= 0 && x < s->size); if ( var_tag(s, x) ) continue; @@ -821,7 +776,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) if (var_level(s,x) == solver2_dlevel(s)) cnt++; else - veci_push(learnt,c->pEnts[j]); + veci_push(learnt,c->lits[j]); } while (!var_tag(s, lit_var(s->trail[ind--]))); @@ -864,7 +819,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) for (i = veci_size(&s->min_step_order); i > 0; ) { i--; c = clause2_read(s, var_reason(s,vars[i])); proof_chain_resolve( s, c, vars[i] ); - satset_foreach_var(c, x, k, 1) + clause_foreach_var(c, x, k, 1) if ( var_level(s,x) == 0 ) proof_chain_resolve( s, NULL, x ); } @@ -913,9 +868,9 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) return proof_id; } -satset* solver2_propagate(sat_solver2* s) +clause* solver2_propagate(sat_solver2* s) { - satset* c, * confl = NULL; + clause* c, * confl = NULL; veci* ws; lit* lits, false_lit, p, * stop, * k; cla* begin,* end, *i, *j; @@ -931,7 +886,7 @@ satset* solver2_propagate(sat_solver2* s) s->stats.propagations++; for (i = j = begin; i < end; ){ c = clause2_read(s,*i); - lits = c->pEnts; + lits = c->lits; // Make sure the false literal is data[1]: false_lit = lit_neg(p); @@ -946,7 +901,7 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; else{ // Look for new watch: - stop = lits + c->nEnts; + stop = lits + c->size; for (k = lits + 2; k < stop; k++){ if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ lits[1] = *k; @@ -962,7 +917,7 @@ satset* solver2_propagate(sat_solver2* s) int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit)); // Log production of top-level unit clause: proof_chain_start( s, c ); - satset_foreach_var( c, x, k, 1 ){ + clause_foreach_var( c, x, k, 1 ){ assert( var_level(s, x) == 0 ); proof_chain_resolve( s, NULL, x ); } @@ -986,6 +941,8 @@ satset* solver2_propagate(sat_solver2* s) *j++ = *i; // Clause is unit under assignment: + if ( c->lrn ) + c->lbd = sat_clause_compute_lbd(s, c); if (!solver2_enqueue(s,Lit, *i)){ confl = clause2_read(s,*i++); // Copy the remaining watches: @@ -1024,7 +981,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) veci_new(&learnt_clause); for (;;){ - satset* confl = solver2_propagate(s); + clause* confl = solver2_propagate(s); if (confl != 0){ // CONFLICT int blevel; @@ -1138,9 +1095,13 @@ sat_solver2* sat_solver2_new(void) #endif s->fSkipSimplify = 1; s->fNotUseRandom = 0; - s->nLearntMax = 0; s->fVerbose = 0; + 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); veci_new(&s->trail_lim); @@ -1152,32 +1113,20 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->mark_levels); veci_new(&s->min_lit_order); veci_new(&s->min_step_order); - veci_new(&s->learnt_live); - veci_new(&s->claActs); veci_push(&s->claActs, -1); - veci_new(&s->claProofs); veci_push(&s->claProofs, -1); +// veci_new(&s->learnt_live); + + Sat_MemAlloc_( &s->Mem, 14 ); + veci_new(&s->act_clas); + veci_new(&s->claProofs); if ( s->fProofLogging ) Vec_SetAlloc_( &s->Proofs, 20 ); - // prealloc clause - assert( !s->clauses.ptr ); - s->clauses.cap = (1 << 20); - s->clauses.ptr = ABC_ALLOC( int, s->clauses.cap ); - veci_push(&s->clauses, -1); - // prealloc learnt - assert( !s->learnts.ptr ); - s->learnts.cap = (1 << 20); - s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap ); - veci_push(&s->learnts, -1); - // initialize clause pointers s->hLearntLast = -1; // the last learnt clause s->hProofLast = -1; // the last proof ID // initialize rollback s->iVarPivot = 0; // the pivot for variables s->iTrailPivot = 0; // the pivot for trail - s->iProofPivot = 0; // the pivot for proof records - s->hClausePivot = 1; // the pivot for problem clause - s->hLearntPivot = 1; // the pivot for learned clause s->hProofPivot = 1; // the pivot for proof records return s; } @@ -1243,11 +1192,11 @@ void sat_solver2_delete(sat_solver2* s) if ( fVerify ) { veci * pCore = (veci *)Sat_ProofCore( s ); - Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); +// Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); veci_delete( pCore ); ABC_FREE( pCore ); - if ( s->fProofLogging ) - Sat_ProofCheck( s ); +// if ( s->fProofLogging ) +// Sat_ProofCheck( s ); } // report statistics @@ -1264,11 +1213,12 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->mark_levels); veci_delete(&s->min_lit_order); veci_delete(&s->min_step_order); - veci_delete(&s->learnt_live); - veci_delete(&s->claActs); +// veci_delete(&s->learnt_live); + veci_delete(&s->act_clas); veci_delete(&s->claProofs); - veci_delete(&s->clauses); - veci_delete(&s->learnts); +// veci_delete(&s->clauses); +// veci_delete(&s->lrns); + Sat_MemFree_( &s->Mem ); // veci_delete(&s->proofs); Vec_SetFree_( &s->Proofs ); @@ -1290,6 +1240,8 @@ void sat_solver2_delete(sat_solver2* s) ABC_FREE(s->model ); } ABC_FREE(s); + +// Abc_PrintTime( 1, "Time", Time ); } @@ -1358,9 +1310,9 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) { // Log production of top-level unit clause: int x, k, proof_id, CidNew; - satset* c = clause2_read(s, Cid); + clause* c = clause2_read(s, Cid); proof_chain_start( s, c ); - satset_foreach_var( c, x, k, 1 ) + clause_foreach_var( c, x, k, 1 ) proof_chain_resolve( s, NULL, x ); proof_id = proof_chain_stop( s ); // generate a new clause @@ -1400,127 +1352,178 @@ void luby2_test() void sat_solver2_reducedb(sat_solver2* s) { static clock_t TimeTotal = 0; - satset * c, * pivot; - cla h,* pArray,* pArray2; - int * pPerm, * pClaAct, nClaAct, ActCutOff; - int i, j, k, hTemp, hHandle, LastSize = 0; + Sat_Mem_t * pMem = &s->Mem; + clause * c; + int nLearnedOld = veci_size(&s->act_clas); + int * act_clas = veci_begin(&s->act_clas); + int * pPerm, * pSortValues, nCutoffValue, * pClaProofs; + int i, j, k, Id, nSelected, LastSize = 0; int Counter, CounterStart; clock_t clk = clock(); + static int Count = 0; + Count++; + assert( s->nLearntMax ); + s->nDBreduces++; +// printf( "Calling reduceDB with %d clause limit and parameters (%d %d %d).\n", s->nLearntMax, s->nLearntStart, s->nLearntDelta, s->nLearntRatio ); - // check if it is time to reduce - if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax ) - return; +/* + // find the new limit s->nLearntMax = s->nLearntMax * 11 / 10; - // preserve 1/10 of last clauses CounterStart = s->stats.learnts - (s->nLearntMax / 10); - // preserve 1/10 of most active clauses - pClaAct = veci_begin(&s->claActs) + 1; - nClaAct = veci_size(&s->claActs) - 1; - pPerm = Abc_MergeSortCost( pClaAct, nClaAct ); - assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] ); - ActCutOff = pClaAct[pPerm[nClaAct*9/10]]; + pSortValues = veci_begin(&s->act_clas); + pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld ); + assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] ); + nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]]; + ABC_FREE( pPerm ); +// nCutoffValue = ABC_INFINITY; +*/ + + + // find the new limit + s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; + // preserve 1/20 of last clauses + CounterStart = nLearnedOld - (s->nLearntMax / 20); + // preserve 3/4 of most active clauses + nSelected = nLearnedOld*s->nLearntRatio/100; + // create sorting values + pSortValues = ABC_ALLOC( int, nLearnedOld ); + Sat_MemForEachLearned( pMem, c, i, k ) + { + Id = clause_id(c); + pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4)); +// pSortValues[Id] = act_clas[Id]; + assert( pSortValues[Id] >= 0 ); + } + // find non-decreasing permutation + pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld ); + assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] ); + nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]]; ABC_FREE( pPerm ); -// ActCutOff = ABC_INFINITY; +// nCutoffValue = ABC_INFINITY; - // mark learned clauses to remove - Counter = 0; - veci_resize( &s->learnt_live, 0 ); - sat_solver_foreach_learnt( s, c, h ) + // count how many clauses satisfy the condition + Counter = j = 0; + Sat_MemForEachLearned( pMem, c, i, k ) { - if ( Counter++ > CounterStart || c->nEnts < 3 || pClaAct[c->Id-1] >= ActCutOff || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 ) - veci_push( &s->learnt_live, h ); + assert( c->mark == 0 ); + if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) + { + } else - c->mark = 1; + j++; + if ( j >= nLearnedOld / 6 ) + break; } - // report the results - if ( s->fVerbose ) - Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", - veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts ); - - // remap clause proofs and clauses - hHandle = 1; - pArray = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; - pArray2 = veci_begin(&s->claActs); - satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) + if ( j < nLearnedOld / 6 ) + return; + + // mark learned clauses to remove + Counter = j = 0; + pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; + Sat_MemForEachLearned( pMem, c, i, k ) { - if ( pArray ) - pArray[i+1] = pArray[c->Id]; - pArray2[i+1] = pArray2[c->Id]; - c->Id = hHandle; hHandle += satset_size(c->nEnts); + assert( c->mark == 0 ); + if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) + { + pSortValues[j] = pSortValues[clause_id(c)]; + if ( pClaProofs ) + pClaProofs[j] = pClaProofs[clause_id(c)]; + j++; + } + else // delete + { + c->mark = 1; + s->stats.learnts_literals -= clause_size(c); + s->stats.learnts--; + } } +// if ( j == nLearnedOld ) +// return; + + assert( s->stats.learnts == (unsigned)j ); + assert( Counter == nLearnedOld ); + veci_resize(&s->act_clas,j); if ( s->fProofLogging ) - veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1); - veci_resize(&s->claActs,veci_size(&s->learnt_live)+1); + veci_resize(&s->claProofs,j); + + // update ID of each clause to be its new handle + Counter = Sat_MemCompactLearned( pMem, 0 ); + assert( Counter == (int)s->stats.learnts ); - // update reason clauses + // update reasons for ( i = 0; i < s->size; i++ ) - if ( s->reasons[i] && (s->reasons[i] & 1) ) - { - c = clause2_read( s, s->reasons[i] ); - assert( c->mark == 0 ); - s->reasons[i] = (c->Id << 1) | 1; - } + { + if ( !s->reasons[i] ) // no reason + continue; + if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause + continue; + if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause + continue; + c = clause2_read( s, s->reasons[i] ); + assert( c->mark == 0 ); + s->reasons[i] = clause_id(c); // updating handle here!!! + } - // compact watches + // update watches for ( i = 0; i < s->size*2; i++ ) { - pArray = veci_begin(&s->wlists[i]); + int * pArray = veci_begin(&s->wlists[i]); for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( !(pArray[k] & 1) ) // problem clause + { + if ( clause_is_lit(pArray[k]) ) // 2-lit clause pArray[j++] = pArray[k]; - else if ( !(c = clause2_read(s, pArray[k]))->mark ) // useful learned clause - pArray[j++] = (c->Id << 1) | 1; + else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause + pArray[j++] = pArray[k]; + else + { + c = clause2_read(s, pArray[k]); + if ( !c->mark ) // useful learned clause + pArray[j++] = clause_id(c); // updating handle here!!! + } + } veci_resize(&s->wlists[i],j); } + // compact units if ( s->fProofLogging ) - for ( i = 0; i < s->size; i++ ) - if ( s->units[i] && (s->units[i] & 1) ) - { - c = clause2_read( s, s->units[i] ); - assert( c->mark == 0 ); - s->units[i] = (c->Id << 1) | 1; - } - // compact clauses - pivot = satset_read( &s->learnts, s->hLearntPivot ); - s->hLearntPivot = hTemp = hHandle; - satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) - { - hTemp = c->Id; c->Id = i + 1; - LastSize = satset_size(c->nEnts); - memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*LastSize ); - if ( pivot && pivot <= c ) - { - s->hLearntPivot = hTemp; - pivot = NULL; - } - } - assert( hHandle == hTemp + LastSize ); - veci_resize(&s->learnts,hHandle); - s->stats.learnts = veci_size(&s->learnt_live); - assert( s->hLearntPivot <= veci_size(&s->learnts) ); - assert( s->hClausePivot <= veci_size(&s->clauses) ); + for ( i = 0; i < s->size; i++ ) + if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) ) + { + c = clause2_read( s, s->units[i] ); + assert( c->mark == 0 ); + s->units[i] = clause_id(c); + } + + // perform final move of the clauses + Counter = Sat_MemCompactLearned( pMem, 1 ); + assert( Counter == (int)s->stats.learnts ); // compact proof (compacts 'proofs' and update 'claProofs') if ( s->fProofLogging ) - Sat_ProofReduce( s ); + s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + + // report the results TimeTotal += clock() - clk; if ( s->fVerbose ) - Abc_PrintTime( 1, "Time", TimeTotal ); + { + Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", + s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld ); + Abc_PrintTime( 1, "Time", TimeTotal ); + } } // reverses to the previously bookmarked point void sat_solver2_rollback( sat_solver2* s ) { + Sat_Mem_t * pMem = &s->Mem; int i, k, j; + static int Count = 0; + Count++; assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); - assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) ); - assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); - assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) ); assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) ); // reset implication queue solver2_canceluntil_rollback( s, s->iTrailPivot ); @@ -1538,42 +1541,32 @@ void sat_solver2_rollback( sat_solver2* s ) } } // compact watches - if ( s->hClausePivot > 1 || s->hLearntPivot > 1 ) - { - for ( i = 0; i < s->size*2; i++ ) - { - cla* pArray = veci_begin(&s->wlists[i]); - for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( clause2_is_used(s, pArray[k]) ) - pArray[j++] = pArray[k]; - veci_resize(&s->wlists[i],j); - } - } - // reset problem clauses - if ( s->hClausePivot < veci_size(&s->clauses) ) + for ( i = 0; i < s->iVarPivot*2; i++ ) { - satset* first = satset_read(&s->clauses, s->hClausePivot); - s->stats.clauses = first->Id-1; - veci_resize(&s->clauses, s->hClausePivot); - } - // resetn learned clauses - if ( s->hLearntPivot < veci_size(&s->learnts) ) - { - satset* first = satset_read(&s->learnts, s->hLearntPivot); - veci_resize(&s->claActs, first->Id); - if ( s->fProofLogging ) { - veci_resize(&s->claProofs, first->Id); -// Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot); // <- some bug here -// Vec_SetShrink(&s->Proofs, s->hProofPivot); - Sat_ProofReduce( s ); - } - s->stats.learnts = first->Id-1; - veci_resize(&s->learnts, s->hLearntPivot); + cla* pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + if ( Sat_MemClauseUsed(pMem, pArray[k]) ) + pArray[j++] = pArray[k]; + veci_resize(&s->wlists[i],j); } // reset watcher lists for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) s->wlists[i].size = 0; + // reset clause counts + s->stats.clauses = pMem->BookMarkE[0]; + s->stats.learnts = pMem->BookMarkE[1]; + // rollback clauses + Sat_MemRollBack( pMem ); + + // resize learned arrays + veci_resize(&s->act_clas, s->stats.learnts); + if ( s->fProofLogging ) + { + veci_resize(&s->claProofs, s->stats.learnts); + Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here +// Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); + } // initialize other vars s->size = s->iVarPivot; @@ -1614,9 +1607,6 @@ void sat_solver2_rollback( sat_solver2* s ) // initialize rollback s->iVarPivot = 0; // the pivot for variables s->iTrailPivot = 0; // the pivot for trail - s->iProofPivot = 0; // the pivot for proof records - s->hClausePivot = 1; // the pivot for problem clause - s->hLearntPivot = 1; // the pivot for learned clause s->hProofPivot = 1; // the pivot for proof records } } @@ -1630,9 +1620,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) for (i = 0; i < s->cap*2; i++) Mem += s->wlists[i].cap * sizeof(int); Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); - Mem += s->clauses.cap * sizeof(int); - Mem += s->learnts.cap * sizeof(int); - Mem += s->claActs.cap * sizeof(int); + Mem += s->act_clas.cap * sizeof(int); Mem += s->claProofs.cap * sizeof(int); // Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); // Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); @@ -1651,7 +1639,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); Mem += s->cap * sizeof(int); // ABC_FREE(s->units ); Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); - Mem += s->tagged.cap * sizeof(int); Mem += s->stack.cap * sizeof(int); Mem += s->order.cap * sizeof(int); @@ -1661,9 +1648,9 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->mark_levels.cap * sizeof(int); Mem += s->min_lit_order.cap * sizeof(int); Mem += s->min_step_order.cap * sizeof(int); - Mem += s->learnt_live.cap * sizeof(int); Mem += s->temp_proof.cap * sizeof(int); -// Mem += Vec_ReportMemory( &s->Mem ); + Mem += Sat_MemMemoryAll( &s->Mem ); +// Mem += Vec_ReportMemory( &s->Proofs ); return Mem; } double sat_solver2_memory_proof( sat_solver2* s ) @@ -1673,6 +1660,7 @@ double sat_solver2_memory_proof( sat_solver2* s ) // find the clause in the watcher lists +/* int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) { int i, k, Found = 0; @@ -1697,25 +1685,26 @@ int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) } return Found; } - +*/ +/* // verify that all problem clauses are satisfied void sat_solver2_verify( sat_solver2* s ) { - satset * c; + clause * c; int i, k, v, Counter = 0; - satset_foreach_entry( &s->clauses, c, i, 1 ) + clause_foreach_entry( &s->clauses, c, i, 1 ) { - for ( k = 0; k < (int)c->nEnts; k++ ) + for ( k = 0; k < (int)c->size; k++ ) { - v = lit_var(c->pEnts[k]); - if ( sat_solver2_var_value(s, v) ^ lit_sign(c->pEnts[k]) ) + v = lit_var(c->lits[k]); + if ( sat_solver2_var_value(s, v) ^ lit_sign(c->lits[k]) ) break; } - if ( k == (int)c->nEnts ) + if ( k == (int)c->size ) { Abc_Print(1, "Clause %d is not satisfied. ", c->Id ); - satset_print( c ); - sat_solver2_find_clause( s, satset_handle(&s->clauses, c), 1 ); + clause_print( c ); + sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 ); Counter++; } } @@ -1724,7 +1713,7 @@ void sat_solver2_verify( sat_solver2* s ) // else // Abc_Print(1, "Verification passed.\n" ); } - +*/ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { @@ -1761,7 +1750,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (!solver2_assume(p)){ GClause r = reason[var(p)]; if (r != Gclause2_NULL){ - satset* confl; + clause* confl; if (r.isLit()){ confl = propagate_tmpbin; (*confl)[1] = ~p; @@ -1775,7 +1764,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim conflict.push(~p); cancelUntil(0); return false; } - satset* confl = propagate(); + clause* confl = propagate(); if (confl != NULL){ analyzeFinal(confl), assert(conflict.size() > 0); cancelUntil(0); @@ -1793,10 +1782,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim veci_push(&s->trail_lim,s->qtail); if (!solver2_enqueue(s,p,0)) { - satset* r = clause2_read(s, lit_reason(s,p)); + clause* r = clause2_read(s, lit_reason(s,p)); if (r != NULL) { - satset* confl = r; + clause* confl = r; proof_id = solver2_analyze_final(s, confl, 1); veci_push(&s->conf_final, lit_neg(p)); } @@ -1816,7 +1805,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { - satset* confl = solver2_propagate(s); + clause* confl = solver2_propagate(s); if (confl != NULL){ proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); @@ -1851,8 +1840,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; - // reduce the set of learnt clauses: - sat_solver2_reducedb(s); + // reduce the set of learnt clauses + if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax ) + sat_solver2_reducedb(s); // perform next run nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) ); status = solver2_search(s, nof_conflicts); @@ -1872,5 +1862,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim return status; } +void * Sat_ProofCore( sat_solver2 * s ) +{ + extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot ); + return Proof_DeriveCore( &s->Proofs, s->hProofLast ); +} ABC_NAMESPACE_IMPL_END |