From 9be1b076934b0410689c857cd71ef7d21a714b5f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 6 Sep 2007 08:01:00 -0700 Subject: Version abc70906 --- src/sat/bsat/satSolver.c | 202 ++++++----------------------------------------- 1 file changed, 25 insertions(+), 177 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 19ff6f8b..512c5751 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -27,7 +27,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satSolver.h" //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT -#define WATCHFLAG 1 //================================================================================================= // Debug: @@ -91,11 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ //================================================================================================= // Encode literals in clause pointers: -static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } +static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } -static clause* clause_from_lit2(lit l) { return (clause*)(unsigned long)l; } -static lit clause_read_lit2(clause* c) { return (lit)(unsigned long)c; } //================================================================================================= // Simple helpers: @@ -111,15 +108,6 @@ static inline void vecp_remove(vecp* v, void* e) for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; vecp_resize(v,vecp_size(v)-1); } -static inline void vecp_remove2(vecp* v, void* e) -{ - void** ws = vecp_begin(v); - int j = 0; - for (; ws[j] != e ; j++); - assert(j < vecp_size(v)); - for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2]; - vecp_resize(v,vecp_size(v)-2); -} //================================================================================================= // Variable order functions: @@ -316,26 +304,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - if ( WATCHFLAG ) - { - if ( size == 2 ) - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit(begin[1])); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit(begin[0])); - } - else - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1])); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0])); - } - } - else - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); - } + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); return c; } @@ -351,24 +321,8 @@ static void clause_remove(sat_solver* s, clause* c) //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); assert(lits[0] < s->size*2); - if ( WATCHFLAG ) - { - if ( clause_size(c) == 2 ) - { - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1])); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0])); - } - else - { - vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); - vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); - } - } - else - { - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); - } + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); if (clause_learnt(c)){ s->stats.learnts--; @@ -749,31 +703,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) } -void sat_solver_check(sat_solver* s) -{ - int j, k; - lit Lit, First, *lits; - vecp* ws; - clause **begin, **end, **i; - for ( j = 0; j < s->size; j++ ) - for ( k = 0; k < 2; k++ ) - { - Lit = toLitCond( j, k ); - ws = sat_solver_read_wlist(s,Lit); - begin = (clause**)vecp_begin(ws); - end = begin + vecp_size(ws); - for (i = begin; i < end; i++) - { - if (clause_is_lit(*i)) - continue; - lits = clause_begin(*i); - First = clause_read_lit2(*(i+1)); - assert( First == lits[0] || First == lits[1] ); - i++; - } - } -} - clause* sat_solver_propagate(sat_solver* s) { lbool* values = s->assigns; @@ -787,19 +716,15 @@ clause* sat_solver_propagate(sat_solver* s) clause **begin = (clause**)vecp_begin(ws); clause **end = begin + vecp_size(ws); clause **i, **j; -// sat_solver_check(s); s->stats.propagations++; s->simpdb_props--; - + //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); - for (i = j = begin; i < end; i++) - { - if (clause_is_lit(*i)) - { + for (i = j = begin; i < end; ){ + if (clause_is_lit(*i)){ *j++ = *i; - if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))) - { + if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ confl = s->binary; (clause_begin(confl))[1] = lit_neg(p); (clause_begin(confl))[0] = clause_read_lit(*i++); @@ -808,27 +733,13 @@ clause* sat_solver_propagate(sat_solver* s) while (i < end) *j++ = *i++; } - } - else - { - lit false_lit, first; + }else{ + lit false_lit; lbool sig; - if ( WATCHFLAG ) - { - first = clause_read_lit2(*(i+1)); - sig = !lit_sign(first); sig += sig - 1; - if (values[lit_var(first)] == sig) - { - *j++ = *i++; - *j++ = *i; - continue; - } - } - lits = clause_begin(*i); - // Make sure the false literal is in data[1]: + // Make sure the false literal is data[1]: false_lit = lit_neg(p); if (lits[0] == false_lit){ lits[0] = lits[1]; @@ -837,95 +748,35 @@ clause* sat_solver_propagate(sat_solver* s) assert(lits[1] == false_lit); //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); - if ( WATCHFLAG ) - { -/* - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig) - { - *j++ = *i++; - *j++ = *i; - continue; - } - else -*/ - { + // If 0th watch is true, then clause is already satisfied. + sig = !lit_sign(lits[0]); sig += sig - 1; + if (values[lit_var(lits[0])] == sig){ + *j++ = *i; + }else{ // Look for new watch: lit* stop = lits + clause_size(*i); lit* k; -// assert( lits[0] == first ); - for (k = lits + 2; k < stop; k++) - { + for (k = lits + 2; k < stop; k++){ lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig) - { + if (values[lit_var(*k)] != sig){ lits[1] = *k; *k = false_lit; -// vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++); - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0])); - break; - } + vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } } - if ( k < stop ) - continue; *j++ = *i; // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)) - { + if (!enqueue(s,lits[0], *i)){ confl = *i++; - *j++ = clause_from_lit2(lits[0]); i++; // // Copy the remaining watches: while (i < end) *j++ = *i++; } - else - { - *j++ = clause_from_lit2(lits[0]); i++; // - } - } - } - else - { - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig) - { - *j++ = *i; - } - else - { - // Look for new watch: - lit* stop = lits + clause_size(*i); - lit* k; - for (k = lits + 2; k < stop; k++) - { - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig) - { - lits[1] = *k; - *k = false_lit; - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); - break; - } - } - if ( k < stop ) - continue; - - *j++ = *i; - // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)) - { - confl = *i++; - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - } } } + next: + i++; } s->stats.inspects += j - (clause**)vecp_begin(ws); @@ -944,7 +795,7 @@ void sat_solver_reducedb(sat_solver* s) double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity clause** learnts = (clause**)vecp_begin(&s->learnts); clause** reasons = s->reasons; -//printf( "Trying to reduce DB\n" ); + sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ @@ -1037,10 +888,8 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l } if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify) - { // Simplify the set of problem clauses: sat_solver_simplify(s); - } if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) // Reduce the set of learnt clauses: @@ -1271,7 +1120,6 @@ bool sat_solver_simplify(sat_solver* s) if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) return true; -//printf( "Trying to simplify\n" ); reasons = s->reasons; for (type = 0; type < 2; type++){ -- cgit v1.2.3