diff options
Diffstat (limited to 'src/sat/bsat/satSolver2.c')
-rw-r--r-- | src/sat/bsat/satSolver2.c | 294 |
1 files changed, 98 insertions, 196 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 37ae7354..25ba35c3 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START -#define SAT_USE_ANALYZE_FINAL #define SAT_USE_PROOF_LOGGING //================================================================================================= @@ -150,7 +149,9 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 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 clause_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]); 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 @@ -501,13 +502,8 @@ static void solver2_canceluntil(sat_solver2* s, int level) { int bound; int lastLev; int c, x; - - if ( level == 0 ) - { - int ss = 0; - } - if (solver2_dlevel(s) <= level) + if (solver2_dlevel(s) < level) return; trail = s->trail; @@ -532,7 +528,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) { } -static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit) +static void solver2_record(sat_solver2* s, veci* cls, int proof_id) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); @@ -540,7 +536,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUni assert(veci_size(cls) > 0); if ( veci_size(cls) == 1 ) { - if ( s->fProofLogging && !fSkipUnit) + if ( s->fProofLogging ) var_set_unit_clause(s, lit_var(begin[0]), Cid); Cid = 0; } @@ -610,14 +606,12 @@ void Solver::analyzeFinal(satset* confl, bool skip_first) } */ -#ifdef SAT_USE_ANALYZE_FINAL - static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) { int i, j, x;//, start; veci_resize(&s->conf_final,0); if ( s->root_level == 0 ) - return -1; + return s->hProofLast; proof_chain_start( s, conf ); assert( veci_size(&s->tagged) == 0 ); satset_foreach_var( conf, x, i, skip_first ){ @@ -650,9 +644,6 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) return proof_chain_stop( s ); } -#endif - - static int solver2_lit_removable_rec(sat_solver2* s, int v) { // tag[0]: True if original conflict clause literal. @@ -916,8 +907,6 @@ satset* solver2_propagate(sat_solver2* s) end = begin + veci_size(ws); s->stats.propagations++; - s->simpdb_props--; - for (i = j = begin; i < end; ){ c = clause_read(s,*i); lits = c->pEnts; @@ -968,7 +957,8 @@ satset* solver2_propagate(sat_solver2* s) proof_chain_start( s, clause_read(s,Cid) ); proof_chain_resolve( s, NULL, Var ); proof_id = proof_chain_stop( s ); - clause_create_new( s, &Lit, &Lit, 1, proof_id ); + s->hProofLast = proof_id; +// clause_create_new( s, &Lit, &Lit, 1, proof_id ); } } @@ -990,71 +980,10 @@ WatchFound: i++; return confl; } - -/* -static void clause_remove(sat_solver2* s, satset* c) -{ - assert(lit_neg(c->pEnts[0]) < s->size*2); - assert(lit_neg(c->pEnts[1]) < s->size*2); - - veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c)); - veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c)); - - if (c->learnt){ - s->stats.learnts--; - s->stats.learnts_literals -= c->nEnts; - }else{ - s->stats.clauses--; - s->stats.clauses_literals -= c->nEnts; - } -} -*/ - -static lbool clause_simplify(sat_solver2* s, satset* c) -{ - int i, x; - assert(solver2_dlevel(s) == 0); - satset_foreach_var( c, x, i, 0 ) - if (var_value(s, x) == lit_sign(c->pEnts[i])) - return l_True; - return l_False; -} - int sat_solver2_simplify(sat_solver2* s) { - int TailOld = s->qtail; -// int type; - int Counter = 0; assert(solver2_dlevel(s) == 0); - // reset the head - s->qhead = 0; - if (solver2_propagate(s) != 0) - return false; -// printf( "Tail moved from %d to %d.\n", TailOld, s->qtail ); - - if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return true; -/* - for (type = 0; type < 2; type++){ - veci* cs = type ? &s->learnts : &s->clauses; - int* cls = (int*)veci_begin(cs); - int i, j; - for (j = i = 0; i < veci_size(cs); i++){ - satset* c = clause_read(s,cls[i]); - if (lit_reason(s,c->pEnts[0]) != cls[i] && - clause_simplify(s,c) == l_True) - clause_remove(s,c), Counter++; - else - cls[j++] = cls[i]; - } - veci_resize(cs,j); - } -*/ -//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses ); - s->simpdb_assigns = s->qhead; - // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); - return true; + return (solver2_propagate(s) == NULL); } /* @@ -1123,11 +1052,10 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) #endif s->stats.conflicts++; conflictC++; if (solver2_dlevel(s) <= s->root_level){ -#ifdef SAT_USE_ANALYZE_FINAL proof_id = solver2_analyze_final(s, confl, 0); assert( proof_id > 0 ); - solver2_record(s,&s->conf_final, proof_id, 0); -#endif +// solver2_record(s,&s->conf_final, proof_id); + s->hProofLast = proof_id; veci_delete(&learnt_clause); return l_False; } @@ -1137,13 +1065,11 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level; blevel = s->root_level > blevel ? s->root_level : blevel; solver2_canceluntil(s,blevel); - solver2_record(s,&learnt_clause, proof_id, 0); -#ifdef SAT_USE_ANALYZE_FINAL + solver2_record(s,&learnt_clause, proof_id); // 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 ) var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 ); -#endif act_var_decay(s); act_clause_decay(s); @@ -1169,9 +1095,9 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) return l_Undef; } - if (solver2_dlevel(s) == 0 && !s->fSkipSimplify) +// if (solver2_dlevel(s) == 0 && !s->fSkipSimplify) // Simplify the set of problem clauses: - sat_solver2_simplify(s); +// sat_solver2_simplify(s); // New variable decision: s->stats.decisions++; @@ -1267,9 +1193,12 @@ sat_solver2* sat_solver2_new(void) veci_push(&s->proofs, -1); } // initialize clause pointers - s->hClausePivot = 1; - s->hLearntPivot = 1; s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + s->hClausePivot = 1; // the pivot among clauses + s->hLearntPivot = 1; // the pivot moang learned clauses + s->iVarPivot = 0; // the pivot among the variables + s->iSimpPivot = 0; // marker of unit-clauses return s; } @@ -1381,17 +1310,13 @@ void sat_solver2_delete(sat_solver2* s) } -int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) +int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) { - lit *i,*j; - int maxvar; - lit last; - - if (begin == end) - { - assert( 0 ); - return false; - } + cla Cid; + lit *i,*j,*iFree = NULL; + int maxvar, count, temp; + assert( solver2_dlevel(s) == 0 ); + assert( begin < end ); // copy clause into storage veci_resize( &s->temp_clause, 0 ); @@ -1400,7 +1325,6 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) begin = veci_begin( &s->temp_clause ); end = begin + veci_size( &s->temp_clause ); - //printlits(begin,end); printf("\n"); // insertion sort maxvar = lit_var(*begin); for (i = begin + 1; i < end; i++){ @@ -1412,67 +1336,58 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) } sat_solver2_setnvars(s,maxvar+1); - // delete duplicates - last = lit_Undef; - for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i)))); - if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) - return true; // tautology - else if (*i != last && var_value(s, lit_var(*i)) == varX) - last = *j++ = *i; - } - //printf("final: "); printlits(begin,j); printf("\n"); - if (j == begin) // empty clause + // coount the number of 0-literals + count = 0; + for ( i = begin; i < end; i++ ) { - assert( 0 ); - return false; + // make sure all literals are unique + assert( i == begin || lit_var(*(i-1)) != lit_var(*i) ); + // consider the value of this literal + if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true + return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count + if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal + iFree = i; + else + count++; // literal is 0 } + assert( count < end-begin ); // the clause cannot be UNSAT - if (j - begin == 1) // unit clause - return solver2_enqueue(s,*begin,0); - - // create new clause - return clause_create_new(s,begin,j,0,0); -} - -int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) -{ - cla Cid; - lit *i,*j; - int maxvar; - assert( begin < end ); - - // copy clause into storage - veci_resize( &s->temp_clause, 0 ); - for ( i = begin; i < end; i++ ) - veci_push( &s->temp_clause, *i ); - begin = veci_begin( &s->temp_clause ); - end = begin + veci_size( &s->temp_clause ); - - // insertion sort - maxvar = lit_var(*begin); - for (i = begin + 1; i < end; i++){ - lit l = *i; - maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; - for (j = i; j > begin && *(j-1) > l; j--) - *j = *(j-1); - *j = l; - } - sat_solver2_setnvars(s,maxvar+1); + // swap variables to make sure the clause is watched using unassigned variable + temp = *iFree; + *iFree = *begin; + *begin = temp; // create a new clause Cid = clause_create_new( s, begin, end, 0, 0 ); + // handle unit clause - if ( begin + 1 == end ) + if ( count+1 == end-begin ) { -// printf( "Adding unit clause %d\n", begin[0] ); -// solver2_canceluntil(s, 0); if ( s->fProofLogging ) - var_set_unit_clause( s, lit_var(begin[0]), Cid ); - if ( !solver2_enqueue(s,begin[0],0) ) - assert( 0 ); + { + if ( count == 0 ) // original learned clause + { + var_set_unit_clause( s, lit_var(begin[0]), Cid ); + if ( !solver2_enqueue(s,begin[0],0) ) + assert( 0 ); + } + else + { + // Log production of top-level unit clause: + int x, k, proof_id, CidNew; + satset* c = clause_read(s, Cid); + proof_chain_start( s, c ); + satset_foreach_var( c, x, k, 1 ) + proof_chain_resolve( s, NULL, x ); + proof_id = proof_chain_stop( s ); + // generate a new clause + CidNew = clause_create_new( s, begin, begin+1, 1, proof_id ); + var_set_unit_clause( s, lit_var(begin[0]), CidNew ); + if ( !solver2_enqueue(s,begin[0],Cid) ) + assert( 0 ); + } + } } -//satset_print( clause_read(s, Cid) ); return Cid; } @@ -1571,6 +1486,7 @@ void solver2_reducedb(sat_solver2* s) void sat_solver2_rollback( sat_solver2* s ) { int i, k, j; + assert( s->qhead == s->qtail ); assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) ); assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); @@ -1596,34 +1512,37 @@ void sat_solver2_rollback( sat_solver2* s ) veci_resize(&s->wlists[i],j); } // compact units - if ( s->fProofLogging ) - for ( i = 0; i < s->size; i++ ) - if ( s->units[i] && !clause_is_used(s, s->units[i]) ) - s->units[i] = 0; + if ( s->fProofLogging ) { + for ( i = 0; i < s->size; i++ ) + if ( s->units[i] && !clause_is_used(s, s->units[i]) ) + { + var_set_value(s, i, varX); + s->reasons[i] = 0; + s->units[i] = 0; + } + } } // reset implication queue - assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns ); - assert( s->simpdb_assigns >= s->iSimpPivot ); + assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot ); (&s->trail_lim)->ptr[0] = s->iSimpPivot; - s->simpdb_assigns = s->iSimpPivot; solver2_canceluntil( s, 0 ); // reset problem clauses if ( s->hClausePivot < veci_size(&s->clauses) ) { satset* first = satset_read(&s->clauses, s->hClausePivot); - s->stats.clauses = first->Id; + 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+1); + veci_resize(&s->claActs, first->Id); if ( s->fProofLogging ) { - veci_resize(&s->claProofs, first->Id+1); + veci_resize(&s->claProofs, first->Id); Sat_ProofReduce( s ); } - s->stats.learnts = first->Id; + s->stats.learnts = first->Id-1; veci_resize(&s->learnts, s->hLearntPivot); } // reset watcher lists @@ -1647,8 +1566,6 @@ void sat_solver2_rollback( sat_solver2* s ) s->cla_inc = (1 << 11); #endif s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; s->random_seed = 91648253; s->progress_estimate = 0; s->verbosity = 0; @@ -1664,9 +1581,12 @@ void sat_solver2_rollback( sat_solver2* s ) s->stats.learnts_literals = 0; s->stats.tot_literals = 0; // initialize clause pointers - s->hClausePivot = 1; - s->hLearntPivot = 1; s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + s->hClausePivot = 1; // the pivot among clauses + s->hLearntPivot = 1; // the pivot moang learned clauses + s->iVarPivot = 0; // the pivot among the variables + s->iSimpPivot = 0; // marker of unit-clauses } } @@ -1717,10 +1637,10 @@ void sat_solver2_verify( sat_solver2* s ) Counter++; } } - if ( Counter == 0 ) - printf( "Verification passed.\n" ); - else + if ( Counter != 0 ) printf( "Verification failed!\n" ); +// else +// printf( "Verification passed.\n" ); } @@ -1734,6 +1654,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim lit * i; s->hLearntLast = -1; + s->hProofLast = -1; // set the external limits // s->nCalls++; @@ -1750,27 +1671,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim 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 (var_value(s, *i)) { - case var1: // l_True: - break; - case varX: // l_Undef - solver2_assume(s, *i); - if (solver2_propagate(s) == NULL) - break; - // fallthrough - case var0: // l_False - solver2_canceluntil(s, 0); - return l_False; - } - } - s->root_level = solver2_dlevel(s); - -#endif - /* // Perform assumptions: root_level = assumps.size(); @@ -1803,7 +1703,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim assert(root_level == decisionLevel()); */ -#ifdef SAT_USE_ANALYZE_FINAL // Perform assumptions: s->root_level = end - begin; for ( i = begin; i < end; i++ ) @@ -1822,6 +1721,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { + assert( 0 ); proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions) veci_resize(&s->conf_final,0); veci_push(&s->conf_final, lit_neg(p)); @@ -1829,7 +1729,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (var_level(s, lit_var(p)) > 0) veci_push(&s->conf_final, p); } - solver2_record(s, &s->conf_final, proof_id, 1); +// solver2_record(s, &s->conf_final, proof_id, 1); + s->hProofLast = proof_id; solver2_canceluntil(s, 0); return l_False; } @@ -1839,14 +1740,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (confl != NULL){ proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); +// solver2_record(s,&s->conf_final, proof_id, 1); + s->hProofLast = proof_id; solver2_canceluntil(s, 0); - solver2_record(s,&s->conf_final, proof_id, 1); return l_False; } } } assert(s->root_level == solver2_dlevel(s)); -#endif if (s->verbosity >= 1){ printf("==================================[MINISAT]===================================\n"); @@ -1891,6 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim printf("==============================================================================\n"); solver2_canceluntil(s,0); + assert( s->qhead == s->qtail ); // if ( status == l_True ) // sat_solver2_verify( s ); return status; |