diff options
Diffstat (limited to 'src/sat/bsat/satSolver.c')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 189 |
1 files changed, 152 insertions, 37 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 1f02adec..1ad903c1 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -28,6 +28,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satStore.h" ABC_NAMESPACE_IMPL_START + +#define SAT_USE_ANALYZE_FINAL + /* extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); @@ -40,8 +43,10 @@ extern int Sto_ManChangeLastClause( void * p ); extern void Sto_ManMarkRoots( void * p ); extern void Sto_ManMarkClausesA( void * p ); */ + //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT + //================================================================================================= // Debug: @@ -457,14 +462,14 @@ static inline int enqueue(sat_solver* s, lit l, clause* from) } -static inline void assume(sat_solver* s, lit l){ +static inline int assume(sat_solver* s, lit l){ assert(s->qtail == s->qhead); assert(s->assigns[lit_var(l)] == l_Undef); #ifdef VERBOSEDEBUG printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); #endif veci_push(&s->trail_lim,s->qtail); - enqueue(s,l,(clause*)0); + return enqueue(s,l,(clause*)0); } @@ -624,52 +629,73 @@ static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ /* -void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) +void Solver::analyzeFinal(Clause* confl, bool skip_first) { - out_conflict.clear(); - out_conflict.push(p); - - if (decisionLevel() == 0) - return; - - seen[var(p)] = 1; + // -- NOTE! This code is relatively untested. Please report bugs! + conflict.clear(); + if (root_level == 0) return; + + vec<char>& seen = analyze_seen; + for (int i = skip_first ? 1 : 0; i < confl->size(); i++){ + Var x = var((*confl)[i]); + if (level[x] > 0) + seen[x] = 1; + } - for (int i = trail.size()-1; i >= trail_lim[0]; i--){ - Var x = var(trail[i]); + int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level]; + for (int i = start; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); if (seen[x]){ - if (reason(x) == GClause_NULL){ - assert(level(x) > 0); - out_conflict.push(~trail[i]); + GClause r = reason[x]; + if (r == GClause_NULL){ + assert(level[x] > 0); + conflict.push(~trail[i]); }else{ - Clause& c = ca.deref(smartReason(x)); - for (int j = 1; j < c.size(); j++) - if (level(var(c[j])) > 0) - seen[var(c[j])] = 1; + if (r.isLit()){ + Lit p = r.lit(); + if (level[var(p)] > 0) + seen[var(p)] = 1; + }else{ + Clause& c = *r.clause(); + for (int j = 1; j < c.size(); j++) + if (level[var(c[j])] > 0) + seen[var(c[j])] = 1; + } } seen[x] = 0; } } - - seen[var(p)] = 0; } */ -static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) +#ifdef SAT_USE_ANALYZE_FINAL + +static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first) { - int i, j; - veci_resize(out_conflict,0); -// veci_push(out_conflict,p); // do not write conflict literal - if ( sat_solver_dlevel(s) == 0 ) + int i, j, start; + veci_resize(&s->conf_final,0); + if ( s->root_level == 0 ) return; assert( veci_size(&s->tagged) == 0 ); - assert( s->tags[lit_var(p)] == l_Undef ); - s->tags[lit_var(p)] = l_True; - for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ +// assert( s->tags[lit_var(p)] == l_Undef ); +// s->tags[lit_var(p)] = l_True; + for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) + { + int x = lit_var(clause_begin(conf)[i]); + if (s->levels[x] > 0) + { + s->tags[x] = l_True; + 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->tags[x] == l_True){ if (s->reasons[x] == NULL){ assert(s->levels[x] > 0); - veci_push(out_conflict,lit_neg(s->trail[i])); + veci_push(&s->conf_final,lit_neg(s->trail[i])); }else{ clause* c = s->reasons[x]; if (clause_is_lit(c)){ @@ -698,6 +724,8 @@ static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict) veci_resize(&s->tagged,0); } +#endif + static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) { @@ -976,8 +1004,9 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT #endif s->stats.conflicts++; conflictC++; if (sat_solver_dlevel(s) == s->root_level){ - lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; -// sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); +#ifdef SAT_USE_ANALYZE_FINAL + sat_solver_analyze_final(s, confl, 0); +#endif veci_delete(&learnt_clause); return l_False; } @@ -988,6 +1017,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT blevel = s->root_level > blevel ? s->root_level : blevel; sat_solver_canceluntil(s,blevel); sat_solver_record(s,&learnt_clause); +#ifdef SAT_USE_ANALYZE_FINAL +// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) + if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0; +#endif act_var_decay(s); act_clause_decay(s); @@ -1340,25 +1373,107 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) s->nInsLimit = nInsLimitGlobal; +#ifndef SAT_USE_ANALYZE_FINAL + //printf("solve: "); printlits(begin, end); printf("\n"); for (i = begin; i < end; i++){ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ - case 1: /* l_True: */ + case 1: // l_True: break; - case 0: /* l_Undef */ + case 0: // l_Undef assume(s, *i); if (sat_solver_propagate(s) == NULL) break; // fallthrough - case -1: /* l_False */ + case -1: // l_False sat_solver_canceluntil(s, 0); return l_False; } } - s->nCalls2++; - s->root_level = sat_solver_dlevel(s); +#endif + +/* + // Perform assumptions: + root_level = assumps.size(); + for (int i = 0; i < assumps.size(); i++){ + Lit p = assumps[i]; + assert(var(p) < nVars()); + if (!assume(p)){ + GClause r = reason[var(p)]; + if (r != GClause_NULL){ + Clause* confl; + if (r.isLit()){ + confl = propagate_tmpbin; + (*confl)[1] = ~p; + (*confl)[0] = r.lit(); + }else + confl = r.clause(); + analyzeFinal(confl, true); + conflict.push(~p); + }else + conflict.clear(), + conflict.push(~p); + cancelUntil(0); + return false; } + Clause* confl = propagate(); + if (confl != NULL){ + analyzeFinal(confl), assert(conflict.size() > 0); + cancelUntil(0); + return false; } + } + assert(root_level == decisionLevel()); +*/ + +#ifdef SAT_USE_ANALYZE_FINAL + // Perform assumptions: + s->root_level = end - begin; + for ( i = begin; i < end; i++ ) + { + lit p = *i; + assert(lit_var(p) < s->size); + veci_push(&s->trail_lim,s->qtail); + if (!enqueue(s,p,(clause*)0)) + { + clause * r = s->reasons[lit_var(p)]; + if (r != NULL) + { + clause* confl; + if (clause_is_lit(r)) + { + confl = s->binary; + (clause_begin(confl))[1] = lit_neg(p); + (clause_begin(confl))[0] = clause_read_lit(r); + } + else + confl = r; + sat_solver_analyze_final(s, confl, 1); + veci_push(&s->conf_final, lit_neg(p)); + } + else + { + veci_resize(&s->conf_final,0); + veci_push(&s->conf_final, lit_neg(p)); + } + sat_solver_canceluntil(s, 0); + return l_False; + } + else + { + clause* confl = sat_solver_propagate(s); + if (confl != NULL){ + sat_solver_analyze_final(s, confl, 0); + assert(s->conf_final.size > 0); + sat_solver_canceluntil(s, 0); + return l_False; } + } + } + assert(s->root_level == sat_solver_dlevel(s)); +#endif + + s->nCalls2++; + if (s->verbosity >= 1){ printf("==================================[MINISAT]===================================\n"); printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); |