diff options
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 4 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 637 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 31 | ||||
| -rw-r--r-- | src/sat/bsat/satUtil.c | 17 | ||||
| -rw-r--r-- | src/sat/bsat/satVec.h | 8 |
5 files changed, 481 insertions, 216 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index ff5e6e3d..f500b46b 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -113,8 +113,8 @@ extern void * sat_solver_store_release( sat_solver * s ); //================================================================================================= // Solver representation: -//struct clause_t; -//typedef struct clause_t clause; +struct clause_t; +typedef struct clause_t clause; struct sat_solver_t { diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 5cb62cf6..405e4367 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -38,7 +38,7 @@ ABC_NAMESPACE_IMPL_START // For derivation output (verbosity level 2) #define L_IND "%-*d" -#define L_ind sat_solver2_dlevel(s)*3+3,sat_solver2_dlevel(s) +#define L_ind solver2_dlevel(s)*3+3,solver2_dlevel(s) #define L_LIT "%sx%d" #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) static void printlits(lit* begin, lit* end) @@ -65,6 +65,8 @@ static inline double drand(double* seed) { static inline int irand(double* seed, int size) { return (int)(drand(seed) * size); } +static inline int sat_float2int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } +static inline float sat_int2float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } //================================================================================================= // Predeclarations: @@ -80,46 +82,88 @@ static const int varX = 3; struct varinfo_t { - unsigned val : 2; - unsigned pol : 1; - unsigned mark : 1; - unsigned tag : 3; - unsigned lev : 25; + unsigned val : 2; // variable value + unsigned pol : 1; // last polarity + unsigned tag : 3; // conflict analysis tags + unsigned lev : 26; // variable level }; -static inline int var_value (sat_solver2 * s, int v) { return s->vi[v].val; } -static inline int var_polar (sat_solver2 * s, int v) { return s->vi[v].pol; } -static inline int var_tag (sat_solver2 * s, int v) { return s->vi[v].tag; } -static inline int var_mark (sat_solver2 * s, int v) { return s->vi[v].mark; } -static inline int var_level (sat_solver2 * s, int v) { return s->vi[v].lev; } +static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } +static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } +static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; } + +static inline void var_set_value (sat_solver2* s, int v, int val ) { s->vi[v].val = val; } +static inline void var_set_polar (sat_solver2* s, int v, int pol ) { s->vi[v].pol = pol; } +static inline void var_set_level (sat_solver2* s, int v, int lev ) { s->vi[v].lev = lev; } + +// variable tags +static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; } +static inline void var_set_tag (sat_solver2* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->vi[v].tag == 0 ) + veci_push( &s->tagged, v ); + s->vi[v].tag = tag; +} +static inline void var_add_tag (sat_solver2* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->vi[v].tag == 0 ) + veci_push( &s->tagged, v ); + s->vi[v].tag |= tag; +} +static inline void solver2_clear_tags(sat_solver2* s, int start) { + int i, * tagged = veci_begin(&s->tagged); + for (i = start; i < veci_size(&s->tagged); i++) + s->vi[tagged[i]].tag = 0; + veci_resize(&s->tagged,start); +} -static inline void var_set_value (sat_solver2 * s, int v, int val ) { s->vi[v].val = val; } -static inline void var_set_polar (sat_solver2 * s, int v, int pol ) { s->vi[v].pol = pol; } -static inline void var_set_tag (sat_solver2 * s, int v, int tag ) { s->vi[v].tag = tag; } -static inline void var_set_mark (sat_solver2 * s, int v, int mark) { s->vi[v].mark = mark; } -static inline void var_set_level (sat_solver2 * s, int v, int lev ) { s->vi[v].lev = lev; } +// level marks +static inline int var_lev_mark (sat_solver2* s, int v) { + return (veci_begin(&s->trail_lim)[var_level(s,v)] & 0x80000000) > 0; +} +static inline void var_lev_set_mark (sat_solver2* s, int v) { + int level = var_level(s,v); + assert( level < veci_size(&s->trail_lim) ); + veci_begin(&s->trail_lim)[level] |= 0x80000000; + veci_push(&s->mark_levels, level); +} +static inline void solver2_clear_marks(sat_solver2* s) { + int i, * mark_levels = veci_begin(&s->mark_levels); + for (i = 0; i < veci_size(&s->mark_levels); i++) + veci_begin(&s->trail_lim)[mark_levels[i]] &= 0x7FFFFFFF; + veci_resize(&s->mark_levels,0); +} + +// other inlines +//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v]; } +//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)]; } +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)]; } //================================================================================================= // Clause datatype + minor functions: -struct clause_t // should have even number of entries! +typedef struct satset_t satset; +struct satset_t // should have even number of entries! { unsigned learnt : 1; - unsigned fMark : 1; - unsigned fPartA : 1; - unsigned fRefed : 1; - unsigned nLits : 28; + unsigned mark : 1; + unsigned partA : 1; + unsigned nLits : 29; int Id; - lit lits[0]; + lit pLits[0]; }; -static inline lit* clause_begin (clause* c) { return c->lits; } -static inline int clause_learnt (clause* c) { return c->learnt; } -static inline int clause_nlits (clause* c) { return c->nLits; } -static inline int clause_size (int nLits) { return sizeof(clause)/4 + nLits + (nLits & 1); } +static inline lit* clause_begin (satset* c) { return c->pLits; } +static inline int clause_learnt (satset* c) { return c->learnt; } +static inline int clause_nlits (satset* c) { return c->nLits; } +static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits + (nLits & 1); } -static inline clause* get_clause (sat_solver2* s, int c) { return (clause *)(s->pMemArray + c); } -static inline cla clause_id (sat_solver2* s, clause* c) { return (cla)((int *)c - s->pMemArray); } +static inline satset* get_clause (sat_solver2* s, int c) { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL; } +static inline cla clause_id (sat_solver2* s, satset* c) { return (cla)((int *)c - veci_begin(&s->clauses)); } + +static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? get_clause(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; } #define sat_solver_foreach_clause( s, c, i ) \ for ( i = 16; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) @@ -127,17 +171,55 @@ static inline cla clause_id (sat_solver2* s, clause* c) { return (cla)( for ( i = s->iLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) //================================================================================================= +// Proof logging: + +static inline void proof_chain_start( sat_solver2* s, satset* c ) +{ + if ( s->fProofLogging ) + { + s->iStartChain = veci_size(&s->proof_clas); + veci_push(&s->proof_clas, 0); + veci_push(&s->proof_clas, 0); + veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 ); + veci_push(&s->proof_vars, 0); + veci_push(&s->proof_vars, 0); + veci_push(&s->proof_vars, 0); + } +} + +static inline void proof_chain_resolve( sat_solver2* s, satset* c, int Var ) +{ + if ( s->fProofLogging && c ) + { + veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 ); + veci_push(&s->proof_vars, Var); + } +} + +static inline void proof_chain_stop( sat_solver2* s ) +{ + if ( s->fProofLogging ) + { + satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain); + assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) ); + c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2; + s->iStartChain = 0; +// printf( "%d ", c->nLits ); + } +} + +//================================================================================================= // Simple helpers: -static inline int sat_solver2_dlevel(sat_solver2* s) { return veci_size(&s->trail_lim); } -static inline veci* sat_solver2_read_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; } +static inline int solver2_dlevel(sat_solver2* s) { return veci_size(&s->trail_lim); } +static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; } //================================================================================================= // Clause functions: static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) { - clause* c; + satset* c; int i, Cid, nLits = end - begin; assert(nLits > 1); assert(begin[0] >= 0); @@ -145,44 +227,43 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) assert(lit_var(begin[0]) < s->size); assert(lit_var(begin[1]) < s->size); // add memory if needed - if ( s->nMemSize + clause_size(nLits) > s->nMemAlloc ) + if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap ) { - int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24); - s->pMemArray = ABC_REALLOC( int, s->pMemArray, nMemAlloc ); - memset( s->pMemArray + s->nMemAlloc, 0, sizeof(int) * (nMemAlloc - s->nMemAlloc) ); - printf( "Reallocing from %d to %d...\n", s->nMemAlloc, nMemAlloc ); - s->nMemAlloc = nMemAlloc; - s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); + int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); + s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); + memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); +// printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); + s->clauses.cap = nMemAlloc; + s->clauses.size = Abc_MaxInt( veci_size(&s->clauses), 2 ); } // create clause - c = (clause*)(s->pMemArray + s->nMemSize); + c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); c->learnt = learnt; c->nLits = nLits; for (i = 0; i < nLits; i++) - c->lits[i] = begin[i]; + c->pLits[i] = begin[i]; // assign clause ID if ( learnt ) { c->Id = s->stats.learnts + 1; assert( c->Id == veci_size(&s->claActs) ); veci_push(&s->claActs, 0); + //veci_push(&s->claProof, 0); } else - { - c->Id = -(s->stats.clauses + 1); - } + c->Id = s->stats.clauses + 1; // extend storage - Cid = s->nMemSize; - s->nMemSize += clause_size(nLits); - if ( s->nMemSize > s->nMemAlloc ) + Cid = veci_size(&s->clauses); + s->clauses.size += clause_size(nLits); + if ( veci_size(&s->clauses) > s->clauses.cap ) printf( "Out of memory!!!\n" ); - assert( s->nMemSize <= s->nMemAlloc ); + assert( veci_size(&s->clauses) <= s->clauses.cap ); assert(((ABC_PTRUINT_T)c & 7) == 0); // watch the clause - veci_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),clause_id(s,c)); - veci_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),clause_id(s,c)); + veci_push(solver2_wlist(s,lit_neg(begin[0])),clause_id(s,c)); + veci_push(solver2_wlist(s,lit_neg(begin[1])),clause_id(s,c)); // remember the last one and first learnt s->iLast = Cid; @@ -284,56 +365,85 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select //================================================================================================= // Activity functions: -static inline void act_var_rescale(sat_solver2* s) { - unsigned* activity = s->activity; - int i, clk = clock(); - static int Total = 0; +#ifdef USE_FLOAT_ACTIVITY + +static inline void act_var_rescale(sat_solver2* s) { + double* activity = s->activity; + int i; for (i = 0; i < s->size; i++) - activity[i] >>= 19; - s->var_inc >>= 19; -// assert( s->var_inc > 15 ); - s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); -// printf( "Rescaling... Var inc = %5d Conf = %10d ", s->var_inc, s->stats.conflicts ); - Total += clock() - clk; -// Abc_PrintTime( 1, "Time", Total ); + activity[i] *= 1e-100; + s->var_inc *= 1e-100; } +static inline void act_clause_rescale(sat_solver2* s) { + static int Total = 0; + float * claActs = (float *)veci_begin(&s->claActs); + int i, clk = clock(); + for (i = 0; i < veci_size(&s->claActs); i++) + claActs[i] *= (float)1e-20; + s->cla_inc *= (float)1e-20; + printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts ); + Total += clock() - clk; + Abc_PrintTime( 1, "Time", Total ); +} static inline void act_var_bump(sat_solver2* s, int v) { - static int Counter = 0; s->activity[v] += s->var_inc; - if (s->activity[v] & 0x80000000) + if (s->activity[v] > 1e100) act_var_rescale(s); if (s->orderpos[v] != -1) order_update(s,v); } +static inline void act_clause_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) + act_clause_rescale(s); +} +static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; } +static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; } -//static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; } -static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); } +#else +static inline void act_var_rescale(sat_solver2* s) { + unsigned* activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] >>= 19; + s->var_inc >>= 19; + s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); +} static inline void act_clause_rescale(sat_solver2* s) { static int Total = 0; int i, clk = clock(); - unsigned * tagged = (unsigned *)veci_begin(&s->claActs); + unsigned * claActs = (unsigned *)veci_begin(&s->claActs); for (i = 1; i < veci_size(&s->claActs); i++) - tagged[i] >>= 14; + claActs[i] >>= 14; s->cla_inc >>= 14; -// assert( s->cla_inc > (1<<10)-1 ); s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); - printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); + + printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); Total += clock() - clk; Abc_PrintTime( 1, "Time", Total ); } - -static inline void act_clause_bump(sat_solver2* s, clause *c) { +static inline void act_var_bump(sat_solver2* s, int v) { + s->activity[v] += s->var_inc; + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); +} +static inline void act_clause_bump(sat_solver2* s, satset*c) { + unsigned * claActs = (unsigned *)veci_begin(&s->claActs); assert( c->Id > 0 && c->Id < veci_size(&s->claActs) ); - ((unsigned *)veci_begin(&s->claActs))[c->Id] += s->cla_inc; - if (((unsigned *)veci_begin(&s->claActs))[c->Id] & 0x80000000) + claActs[c->Id] += s->cla_inc; + if (claActs[c->Id] & 0x80000000) act_clause_rescale(s); } - -//static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; } +static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); } static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); } +#endif //================================================================================================= // Minor (solver) functions: @@ -352,7 +462,7 @@ static inline int enqueue(sat_solver2* s, lit l, int from) printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); #endif var_set_value( s, v, lit_sign(l) ); - var_set_level( s, v, sat_solver2_dlevel(s) ); + var_set_level( s, v, solver2_dlevel(s) ); s->reasons[v] = from; s->trail[s->qtail++] = l; order_assigned(s, v); @@ -377,7 +487,7 @@ static void sat_solver2_canceluntil(sat_solver2* s, int level) { int lastLev; int c, x; - if (sat_solver2_dlevel(s) <= level) + if (solver2_dlevel(s) <= level) return; trail = s->trail; @@ -440,7 +550,7 @@ static double sat_solver2_progress(sat_solver2* s) | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ /* -void Solver::analyzeFinal(Clause* confl, bool skip_first) +void Solver::analyzeFinal(satset* confl, bool skip_first) { // -- NOTE! This code is relatively untested. Please report bugs! conflict.clear(); @@ -481,102 +591,166 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first) #ifdef SAT_USE_ANALYZE_FINAL -static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first) +static void sat_solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) { - int* tagged; - int i, j, start; + int i, j, start, x; veci_resize(&s->conf_final,0); if ( s->root_level == 0 ) return; assert( veci_size(&s->tagged) == 0 ); for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++) { - int x = lit_var(clause_begin(conf)[i]); + x = lit_var(clause_begin(conf)[i]); if ( var_level(s,x) ) - { var_set_tag(s, x, 1); - veci_push(&s->tagged,x); - } } - start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ - int x = lit_var(s->trail[i]); - if (s->vi[x].tag == 1){ - if (s->reasons[x] == 0){ - assert( var_level(s,x) ); - veci_push(&s->conf_final,lit_neg(s->trail[i])); - }else{ - clause* c = get_clause(s, s->reasons[x]); + x = lit_var(s->trail[i]); + if (var_tag(s,x)){ + satset* c = get_clause(s, var_reason(s,x)); + if (c){ int* lits = clause_begin(c); for (j = 1; j < clause_nlits(c); j++) if ( var_level(s,lit_var(lits[j])) ) - { var_set_tag(s, lit_var(lits[j]), 1); - veci_push(&s->tagged,lit_var(lits[j])); - } + }else { + assert( var_level(s,x) ); + veci_push(&s->conf_final,lit_neg(s->trail[i])); } } } - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - var_set_tag(s, tagged[i], 0); - veci_resize(&s->tagged,0); + solver2_clear_tags(s,0); } #endif -static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl) +static int sat_solver2_lit_removable_rec(sat_solver2* s, int v) { - clause* c; - lit* lits; - int i, j, v, top = veci_size(&s->tagged); - assert(lit_var(l) >= 0 && lit_var(l) < s->size); - assert(s->reasons[lit_var(l)] != 0); + // tag[0]: True if original conflict clause literal. + // tag[1]: Processed by this procedure + // tag[2]: 0=non-removable, 1=removable + + satset* c; + int i, x; + + // skip visited + if (var_tag(s,v) & 2) + return (var_tag(s,v) & 4) > 0; + + // skip decisions on a wrong level + c = get_clause(s, var_reason(s,v)); + if ( c == NULL ){ + var_add_tag(s,v,2); + return 0; + } + + for ( i = 1; i < (int)c->nLits; i++ ){ + x = lit_var(c->pLits[i]); + if (var_tag(s,x) & 1) + sat_solver2_lit_removable_rec(s, x); + else{ + if (var_level(s,x) == 0 || var_tag(s,x) == 6) continue; // -- 'x' checked before, found to be removable (or belongs to the toplevel) + if (var_tag(s,x) == 2 || !var_lev_mark(s,x) || !sat_solver2_lit_removable_rec(s, x)) + { // -- 'x' checked before, found NOT to be removable, or it belongs to a wrong level, or cannot be removed + var_add_tag(s,v,2); + return 0; + } + } + } +// if (pfl && visit[p0] & 1){ +// result.push(p0); } + var_add_tag(s,v,6); + return 1; +} + +static int sat_solver2_lit_removable(sat_solver2* s, int x) +{ + satset* c; + int i, top; + if ( !var_reason(s,x) ) + return 0; + if ( var_tag(s,x) & 2 ) + { + assert( var_tag(s,x) & 1 ); + return 1; + } + top = veci_size(&s->tagged); veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - while (veci_size(&s->stack) > 0) + veci_push(&s->stack, x << 1); + while (veci_size(&s->stack)) { - v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; - assert(v >= 0 && v < s->size); - veci_resize(&s->stack,veci_size(&s->stack)-1); - assert(s->reasons[v] != 0); - c = get_clause(s, s->reasons[v]); - lits = clause_begin(c); - for (i = 1; i < clause_nlits(c); i++){ - int v = lit_var(lits[i]); - if (s->vi[v].tag == 0 && var_level(s,v)){ - if (s->reasons[v] != 0 && ((1 << (var_level(s,v) & 31)) & minl)){ - veci_push(&s->stack,lit_var(lits[i])); - var_set_tag(s, v, 1); - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - for (j = top; j < veci_size(&s->tagged); j++) - var_set_tag(s, tagged[j], 0); - veci_resize(&s->tagged,top); - return false; - } + x = veci_pop(&s->stack); + if ( s->fProofLogging ){ + if ( x & 1 ){ + if ( var_tag(s,x >> 1) & 1 ) + veci_push(&s->min_lit_order, x >> 1 ); + continue; } + veci_push(&s->stack, x ^ 1 ); + } + x >>= 1; + c = get_clause(s, var_reason(s,x)); + for (i = 1; i < (int)c->nLits; i++){ + x = lit_var(c->pLits[i]); + if (var_tag(s,x) || !var_level(s,x)) + continue; + if (!var_reason(s,x) || !var_lev_mark(s,x)){ + solver2_clear_tags(s, top); + return 0; + } + veci_push(&s->stack, x << 1); + var_set_tag(s, x, 2); } } - return true; + return 1; } -static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) +static void sat_solver2_logging_order(sat_solver2* s, int x) { - lit* trail = s->trail; - int cnt = 0; - lit p = lit_Undef; - int ind = s->qtail-1; - lit* lits; - int i, j, minl; - int* tagged; - assert( veci_size(&s->tagged) == 0 ); + satset* c; + int i; + if ( (var_tag(s,x) & 4) ) + return; + var_add_tag(s, x, 4); + veci_resize(&s->stack,0); + veci_push(&s->stack,x << 1); + while (veci_size(&s->stack)) + { + x = veci_pop(&s->stack); + if ( x & 1 ){ + veci_push(&s->min_step_order, x >> 1 ); + continue; + } + veci_push(&s->stack, x ^ 1 ); + x >>= 1; + c = get_clause(s, var_reason(s,x)); +// if ( !c ) +// printf( "sat_solver2_logging_order(): Error in conflict analysis!!!\n" ); + for (i = 1; i < (int)c->nLits; i++){ + x = lit_var(c->pLits[i]); + if ( !var_level(s,x) || (var_tag(s,x) & 1) ) + continue; + veci_push(&s->stack, x << 1); + var_add_tag(s, x, 4); + } + } +} +static void sat_solver2_analyze(sat_solver2* s, satset* c, veci* learnt) +{ + int cnt = 0; + lit p = lit_Undef; + int x, ind = s->qtail-1; + lit* lits,* vars, i, j, k; + assert( veci_size(&s->tagged) == 0 ); + // tag[0] - visited by conflict analysis (afterwards: literals of the learned clause) + // tag[1] - visited by sat_solver2_lit_removable() with success + // tag[2] - visited by sat_solver2_logging_order() +/* + proof_chain_start( s, c ); veci_push(learnt,lit_Undef); - do{ assert(c != 0); if (clause_learnt(c)) @@ -588,46 +762,107 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) assert(lit_var(q) >= 0 && lit_var(q) < s->size); if (!var_tag(s, lit_var(q)) && var_level(s,lit_var(q))){ var_set_tag(s, lit_var(q), 1); - veci_push(&s->tagged,lit_var(q)); act_var_bump(s,lit_var(q)); - if (var_level(s,lit_var(q)) == sat_solver2_dlevel(s)) + if (var_level(s,lit_var(q)) == solver2_dlevel(s)) cnt++; else veci_push(learnt,q); } } - while (!var_tag(s, lit_var(trail[ind--]))); + while (!var_tag(s, lit_var(s->trail[ind--]))); - p = trail[ind+1]; - c = get_clause(s, s->reasons[lit_var(p)]); + p = s->trail[ind+1]; + c = get_clause(s, lit_reason(s,p)); cnt--; }while (cnt > 0); + *veci_begin(learnt) = lit_neg(p); +*/ + proof_chain_start( s, c ); + veci_push(learnt,lit_Undef); + while ( 1 ){ + assert(c != 0); + if (clause_learnt(c)) + act_clause_bump(s,c); + for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){ + x = lit_var(c->pLits[j]); + assert(x >= 0 && x < s->size); + if ( var_tag(s, x) ) + continue; + if ( var_level(s,x) == 0 ) + { + proof_chain_resolve( s, var_unit_clause(s, x), x ); + continue; + } + var_set_tag(s, x, 1); + act_var_bump(s,x); + if (var_level(s,x) == solver2_dlevel(s)) + cnt++; + else + veci_push(learnt,c->pLits[j]); + } + + while (!var_tag(s, lit_var(s->trail[ind--]))); + + p = s->trail[ind+1]; + c = get_clause(s, lit_reason(s,p)); + cnt--; + if ( cnt == 0 ) + break; + proof_chain_resolve( s, c, lit_var(p) ); + } *veci_begin(learnt) = lit_neg(p); + // mark levels + assert( veci_size(&s->mark_levels) == 0 ); lits = veci_begin(learnt); - minl = 0; for (i = 1; i < veci_size(learnt); i++) - minl |= 1 << (var_level(s,lit_var(lits[i])) & 31); + var_lev_set_mark(s, lit_var(lits[i])); // simplify (full) + veci_resize(&s->min_lit_order, 0); for (i = j = 1; i < veci_size(learnt); i++){ - if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver2_lit_removable(s,lits[i],minl)) +// if (!sat_solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!! + if (!sat_solver2_lit_removable( s,lit_var(lits[i])) ) lits[j++] = lits[i]; + } + + // record the proof + if ( s->fProofLogging ) + { + // collect additional clauses to resolve + veci_resize(&s->min_step_order, 0); + vars = veci_begin(&s->min_lit_order); + for (i = 0; i < veci_size(&s->min_lit_order); i++) + sat_solver2_logging_order( s, vars[i] ); + + // add them in the reverse order + vars = veci_begin(&s->min_step_order); + for (i = veci_size(&s->min_step_order); i > 0; ) { i--; + c = get_clause(s, var_reason(s,vars[i])); + proof_chain_resolve( s, c, vars[i] ); + for ( k = 1; k < (int)c->nLits; k++ ) + { + x = lit_var(c->pLits[k]); + if ( var_level(s,x) == 0 ) + proof_chain_resolve( s, var_unit_clause(s, x), x ); + } + } + proof_chain_stop( s ); } + // unmark levels + solver2_clear_marks( s ); + // update size of learnt + statistics s->stats.max_literals += veci_size(learnt); veci_resize(learnt,j); s->stats.tot_literals += j; // clear tags - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - var_set_tag(s, tagged[i], 0); - veci_resize(&s->tagged,0); + solver2_clear_tags(s,0); #ifdef DEBUG for (i = 0; i < s->size; i++) @@ -660,16 +895,16 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) #endif } -clause* sat_solver2_propagate(sat_solver2* s) +satset* sat_solver2_propagate(sat_solver2* s) { - clause * c, * confl = NULL; + satset* c, * confl = NULL; veci* ws; lit* lits, false_lit, p, * stop, * k; cla* begin,* end, *i, *j; while (confl == 0 && s->qtail - s->qhead > 0){ p = s->trail[s->qhead++]; - ws = sat_solver2_read_wlist(s,p); + ws = solver2_wlist(s,p); begin = (cla*)veci_begin(ws); end = begin + veci_size(ws); @@ -703,7 +938,7 @@ clause* sat_solver2_propagate(sat_solver2* s) if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ lits[1] = *k; *k = false_lit; - veci_push(sat_solver2_read_wlist(s,lit_neg(lits[1])),*i); + veci_push(solver2_wlist(s,lit_neg(lits[1])),*i); goto next; } } @@ -729,14 +964,14 @@ next: i++; -static void clause_remove(sat_solver2* s, clause* c) +static void clause_remove(sat_solver2* s, satset* c) { lit* lits = clause_begin(c); assert(lit_neg(lits[0]) < s->size*2); assert(lit_neg(lits[1]) < s->size*2); - veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),clause_id(s,c)); - veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),clause_id(s,c)); + veci_remove(solver2_wlist(s,lit_neg(lits[0])),clause_id(s,c)); + veci_remove(solver2_wlist(s,lit_neg(lits[1])),clause_id(s,c)); if (clause_learnt(c)){ s->stats.learnts--; @@ -748,11 +983,11 @@ static void clause_remove(sat_solver2* s, clause* c) } -static lbool clause_simplify(sat_solver2* s, clause* c) +static lbool clause_simplify(sat_solver2* s, satset* c) { lit* lits = clause_begin(c); int i; - assert(sat_solver2_dlevel(s) == 0); + assert(solver2_dlevel(s) == 0); for (i = 0; i < clause_nlits(c); i++){ if (var_value(s, lit_var(lits[i])) == lit_sign(lits[i])) return l_True; @@ -764,7 +999,7 @@ int sat_solver2_simplify(sat_solver2* s) { // int type; int Counter = 0; - assert(sat_solver2_dlevel(s) == 0); + assert(solver2_dlevel(s) == 0); if (sat_solver2_propagate(s) != 0) return false; if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) @@ -775,8 +1010,8 @@ int sat_solver2_simplify(sat_solver2* s) int* cls = (int*)veci_begin(cs); int i, j; for (j = i = 0; i < veci_size(cs); i++){ - clause * c = get_clause(s,cls[i]); - if (s->reasons[lit_var(*clause_begin(c))] != cls[i] && + satset* c = get_clause(s,cls[i]); + if (lit_reason(s,*clause_begin(c)) != cls[i] && clause_simplify(s,c) == l_True) clause_remove(s,c), Counter++; else @@ -794,7 +1029,8 @@ int sat_solver2_simplify(sat_solver2* s) void sat_solver2_reducedb(sat_solver2* s) { - clause * c; +/* + satset* c; cla Cid; int clk = clock(); @@ -814,10 +1050,10 @@ void sat_solver2_reducedb(sat_solver2* s) sat_solver_foreach_learnt( s, c, Cid ) { assert( c->Id == k ); - c->fMark = 0; - if ( clause_nlits(c) > 2 && s->reasons[lit_var(*clause_begin(c))] != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) + c->mark = 0; + if ( clause_nlits(c) > 2 && lit_reason(s,*clause_begin(c)) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) { - c->fMark = 1; + c->mark = 1; Counter++; } k++; @@ -826,28 +1062,25 @@ printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d ", Counter Abc_PrintTime( 1, "Time", clock() - clk ); } ABC_FREE( pPerm ); +*/ } static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts) { - double var_decay = 0.95; - double clause_decay = 0.999; double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; -// s->var_decay = (float)(1 / var_decay ); -// s->cla_decay = (float)(1 / clause_decay); ABC_INT64_T conflictC = 0; veci learnt_clause; - assert(s->root_level == sat_solver2_dlevel(s)); + assert(s->root_level == solver2_dlevel(s)); s->stats.starts++; veci_resize(&s->model,0); veci_new(&learnt_clause); for (;;){ - clause* confl = sat_solver2_propagate(s); + satset* confl = sat_solver2_propagate(s); if (confl != 0){ // CONFLICT int blevel; @@ -856,7 +1089,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I printf(L_IND"**CONFLICT**\n", L_ind); #endif s->stats.conflicts++; conflictC++; - if (sat_solver2_dlevel(s) == s->root_level){ + if (solver2_dlevel(s) == s->root_level){ #ifdef SAT_USE_ANALYZE_FINAL sat_solver2_analyze_final(s, confl, 0); #endif @@ -901,7 +1134,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I return l_Undef; } -// if (sat_solver2_dlevel(s) == 0 && !s->fSkipSimplify) +// if (solver2_dlevel(s) == 0 && !s->fSkipSimplify) // Simplify the set of problem clauses: // sat_solver2_simplify(s); @@ -951,7 +1184,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I sat_solver2* sat_solver2_new(void) { - sat_solver2 * s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) ); + sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) ); // initialize vectors veci_new(&s->order); @@ -961,20 +1194,32 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->model); veci_new(&s->temp_clause); veci_new(&s->conf_final); - veci_new(&s->claActs); - veci_new(&s->claProofs); - veci_push(&s->claActs, -1); - veci_push(&s->claProofs, -1); + veci_new(&s->mark_levels); + veci_new(&s->min_lit_order); + veci_new(&s->min_step_order); + veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1); + veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1); + veci_new(&s->claActs); veci_push(&s->claActs, -1); + veci_new(&s->claProofs); veci_push(&s->claProofs, -1); // initialize other s->iLearnt = -1; // the first learnt clause s->iLast = -1; // the last learnt clause +#ifdef USE_FLOAT_ACTIVITY + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999 ); +#else + s->var_inc = (1 << 5); s->cla_inc = (1 << 11); - s->var_inc = (1 << 5); +#endif s->random_seed = 91648253; + s->fProofLogging = 1; return s; } + void sat_solver2_setnvars(sat_solver2* s,int n) { int var; @@ -985,10 +1230,14 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2); s->vi = ABC_REALLOC(varinfo, s->vi, s->cap); - s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); s->reasons = ABC_REALLOC(cla, s->reasons, s->cap); s->trail = ABC_REALLOC(lit, s->trail, s->cap); +#ifdef USE_FLOAT_ACTIVITY + s->activity = ABC_REALLOC(double, s->activity, s->cap); +#else + s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); +#endif } for (var = s->size; var < n; var++){ @@ -1008,7 +1257,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { - ABC_FREE(s->pMemArray); + // report statistics + assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) ); + printf( "Used %6.2f Mb for proof-logging.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20) ); // delete vectors veci_delete(&s->order); @@ -1018,8 +1269,14 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->model); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); + veci_delete(&s->mark_levels); + veci_delete(&s->min_lit_order); + veci_delete(&s->min_step_order); + veci_delete(&s->proof_clas); + veci_delete(&s->proof_vars); veci_delete(&s->claActs); veci_delete(&s->claProofs); + veci_delete(&s->clauses); // delete arrays if (s->vi != 0){ @@ -1029,10 +1286,10 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->wlists[i]); ABC_FREE(s->wlists ); ABC_FREE(s->vi ); - ABC_FREE(s->activity ); ABC_FREE(s->orderpos ); ABC_FREE(s->reasons ); ABC_FREE(s->trail ); + ABC_FREE(s->activity ); } ABC_FREE(s); } @@ -1162,7 +1419,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim return l_False; } } - s->root_level = sat_solver2_dlevel(s); + s->root_level = solver2_dlevel(s); #endif @@ -1175,7 +1432,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (!assume(p)){ GClause r = reason[var(p)]; if (r != GClause_NULL){ - Clause* confl; + satset* confl; if (r.isLit()){ confl = propagate_tmpbin; (*confl)[1] = ~p; @@ -1189,7 +1446,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim conflict.push(~p); cancelUntil(0); return false; } - Clause* confl = propagate(); + satset* confl = propagate(); if (confl != NULL){ analyzeFinal(confl), assert(conflict.size() > 0); cancelUntil(0); @@ -1208,10 +1465,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim veci_push(&s->trail_lim,s->qtail); if (!enqueue(s,p,0)) { - clause * r = get_clause(s, s->reasons[lit_var(p)]); + satset* r = get_clause(s, lit_reason(s,p)); if (r != NULL) { - clause* confl = r; + satset* confl = r; sat_solver2_analyze_final(s, confl, 1); veci_push(&s->conf_final, lit_neg(p)); } @@ -1225,7 +1482,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { - clause* confl = sat_solver2_propagate(s); + satset* confl = sat_solver2_propagate(s); if (confl != NULL){ sat_solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); @@ -1233,7 +1490,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim return l_False; } } } - assert(s->root_level == sat_solver2_dlevel(s)); + assert(s->root_level == solver2_dlevel(s)); #endif // s->nCalls2++; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index a5ed85b3..937972a6 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START - +//#define USE_FLOAT_ACTIVITY //================================================================================================= // Public interface: @@ -70,9 +70,6 @@ extern void * sat_solver2_store_release( sat_solver2 * s ); //================================================================================================= // Solver representation: -//struct clause_t; -//typedef struct clause_t clause; - struct varinfo_t; typedef struct varinfo_t varinfo; @@ -91,21 +88,26 @@ struct sat_solver2_t int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything int fNotUseRandom; // do not allow random decisions with a fixed probability // int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging // clauses + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) int iLearnt; // the first learnt clause int iLast; // the last learnt clause - veci* wlists; // watcher lists (for each literal) - - // clause memory - int * pMemArray; - int nMemAlloc; - int nMemSize; // activities +#ifdef USE_FLOAT_ACTIVITY + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. +#else int var_inc; // Amount to bump next variable with. int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable. +#endif veci claActs; // clause activities veci claProofs; // clause proofs @@ -123,6 +125,15 @@ struct sat_solver2_t veci model; // If problem is solved, this vector contains the model (contains: lbool). veci conf_final; // If problem is unsatisfiable (possibly under assumptions), // this vector represent the final conflict clause expressed in the assumptions. + veci mark_levels; // temporary storage for labeled levels + veci min_lit_order; // ordering of removable literals + veci min_step_order;// ordering of resolution steps + + // proof logging + veci proof_clas; // sequence of proof clauses + veci proof_vars; // sequence of proof variables + int iStartChain; // beginning of the chain + // statistics stats_t stats; ABC_INT64_T nConfLimit; // external limit on the number of conflicts diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index ab9641bb..99a09081 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -169,16 +169,15 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) SeeAlso [] ***********************************************************************/ -void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ) +void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s ) { -// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); - printf( "starts : %10d\n", (int)p->stats.starts ); - printf( "conflicts : %10d\n", (int)p->stats.conflicts ); - printf( "decisions : %10d\n", (int)p->stats.decisions ); - printf( "propagations : %10d\n", (int)p->stats.propagations ); -// printf( "inspects : %10d\n", (int)p->stats.inspects ); -// printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); - printf( "memory : %10d\n", p->nMemSize ); + printf( "starts : %10d\n", (int)s->stats.starts ); + printf( "conflicts : %10d\n", (int)s->stats.conflicts ); + printf( "decisions : %10d\n", (int)s->stats.decisions ); + printf( "propagations : %10d\n", (int)s->stats.propagations ); +// printf( "inspects : %10d\n", (int)s->stats.inspects ); +// printf( "inspects2 : %10d\n", (int)s->stats.inspects2 ); + printf( "memory : %10d\n", veci_size(&s->clauses) ); } /**Function************************************************************* diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index aeca3059..1f63ba1e 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -44,7 +44,8 @@ static inline void veci_new (veci* v) { static inline void veci_delete (veci* v) { ABC_FREE(v->ptr); } static inline int* veci_begin (veci* v) { return v->ptr; } static inline int veci_size (veci* v) { return v->size; } -static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! +static inline void veci_resize (veci* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !! +static inline int veci_pop (veci* v) { assert(v->size); return v->ptr[--v->size]; } static inline void veci_push (veci* v, int e) { if (v->size == v->cap) { @@ -82,7 +83,7 @@ static inline void vecp_new (vecp* v) { static inline void vecp_delete (vecp* v) { ABC_FREE(v->ptr); } static inline void** vecp_begin (vecp* v) { return v->ptr; } static inline int vecp_size (vecp* v) { return v->size; } -static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !! +static inline void vecp_resize (vecp* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !! static inline void vecp_push (vecp* v, void* e) { if (v->size == v->cap) { @@ -143,9 +144,6 @@ struct stats_t }; typedef struct stats_t stats_t; -struct clause_t; -typedef struct clause_t clause; - ABC_NAMESPACE_HEADER_END #endif |