From 06416a981f73b61581f399e9c7c205366fa23edf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 26 Nov 2011 11:33:37 -0800 Subject: Started experiments with a new solver. --- src/sat/bsat/satSolver2.c | 438 ++++++++++++++++++++++++++++++++++++++-------- src/sat/bsat/satSolver2.h | 1 + src/sat/bsat/satUtil.c | 4 +- 3 files changed, 371 insertions(+), 72 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 81e26cb8..6f292e64 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -28,9 +28,9 @@ 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_SYSTEM_MEMORY_MANAGEMENT +#define SAT_USE_ANALYZE_FINAL +//#define SAT_USE_WATCH_ARRAYS //================================================================================================= // Debug: @@ -79,6 +79,7 @@ struct clause_t { int size_learnt; unsigned act; + clause * pNext[2]; lit lits[0]; }; @@ -203,11 +204,10 @@ static inline void act_var_rescale(sat_solver2* s) { int i, clk = clock(); static int Total = 0; for (i = 0; i < s->size; i++) - activity[i] >>= 20; - s->var_inc >>= 20; + activity[i] >>= 19; + s->var_inc >>= 19; // assert( s->var_inc > 15 ); - - s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<4) ); + 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 ); @@ -233,7 +233,6 @@ static inline void act_clause_rescale(sat_solver2* s) { for (i = 0; i < vecp_size(&s->learnts); i++) cs[i]->act >>= 14; s->cla_inc >>= 14; - // assert( s->cla_inc > (1<<10)-1 ); s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); @@ -254,24 +253,113 @@ static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc //================================================================================================= // Clause functions: +static inline void clause_watch_( sat_solver2* s, clause* c, lit Lit ) +{ + if ( c->lits[0] == Lit ) + c->pNext[0] = s->pWatches[lit_neg(Lit)]; + else + { + assert( c->lits[1] == Lit ); + c->pNext[1] = s->pWatches[lit_neg(Lit)]; + } + s->pWatches[lit_neg(Lit)] = c; +} -/* pre: size > 1 && no variable occurs twice - */ -static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) +static inline void clause_watch__( sat_solver2* s, clause* c, lit Lit ) { - int size; - clause* c; - int i; + clause* pLast = s->pWatches[lit_neg(Lit)]; + if ( c->lits[0] == Lit ) + c->pNext[0] = NULL; + else + { + assert( c->lits[1] == Lit ); + c->pNext[1] = NULL; + } + // add at the tail + if ( pLast == NULL ) + { + s->pWatches[lit_neg(Lit)] = c; + return; + } + // find the last one + while ( 1 ) + { + if ( pLast->lits[0] == Lit ) + { + if ( pLast->pNext[0] == NULL ) + { + pLast->pNext[0] = c; + return; + } + pLast = pLast->pNext[0]; + } + else + { + assert( pLast->lits[1] == Lit ); + if ( pLast->pNext[1] == NULL ) + { + pLast->pNext[1] = c; + return; + } + pLast = pLast->pNext[1]; + } + } +} - assert(end - begin > 1); - assert(learnt >= 0 && learnt < 2); - size = end - begin; +static inline void clause_watch33( sat_solver2* s, clause* c, lit Lit ) +{ + clause** ppList = s->pWatches + lit_neg(Lit),** ppNext; + if ( c->lits[0] == Lit ) + ppNext = &c->pNext[0]; + else + { + assert( c->lits[1] == Lit ); + ppNext = &c->pNext[1]; + } + if ( *ppList == NULL ) + { + *ppList = c; + *ppNext = c; + return; + } + // add at the tail + if ( (*ppList)->lits[0] == Lit ) + { + assert( (*ppList)->pNext[0] != NULL ); + *ppNext = (*ppList)->pNext[0]; + (*ppList)->pNext[0] = c; + } + else + { + assert( (*ppList)->lits[1] == Lit ); + assert( (*ppList)->pNext[1] != NULL ); + *ppNext = (*ppList)->pNext[1]; + (*ppList)->pNext[1] = c; + } + *ppList = c; +} - // c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size); -#else -// c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); +static inline void clause_watch( sat_solver2* s, clause* c, lit Lit ) +{ + clause * pList = s->pWatches[lit_neg(Lit)]; + assert( c->lits[0] == Lit || c->lits[1] == Lit ); + if ( pList == NULL ) + c->pNext[c->lits[1] == Lit] = c; + else + { + assert( pList->lits[0] == Lit || pList->lits[1] == Lit ); + c->pNext[c->lits[1] == Lit] = pList->pNext[pList->lits[1] == Lit]; + pList->pNext[pList->lits[1] == Lit] = c; + } + s->pWatches[lit_neg(Lit)] = c; +} + +static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) +{ + clause* c; + int i, size = end - begin; + assert(size > 1); + // add memory if needed if ( s->nMemSize + (int)sizeof(clause)/4 + size > s->nMemAlloc ) { int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24); @@ -281,16 +369,14 @@ static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) s->nMemAlloc = nMemAlloc; s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); } + // create clause c = (clause*)(s->pMemArray + s->nMemSize); s->nMemSize += sizeof(clause)/4 + size; if ( s->nMemSize > s->nMemAlloc ) printf( "Out of memory!!!\n" ); assert( s->nMemSize <= s->nMemAlloc ); -#endif - c->size_learnt = (size << 1) | learnt; assert(((ABC_PTRUINT_T)c & 1) == 0); - c->act = 0; for (i = 0; i < size; i++) c->lits[i] = begin[i]; @@ -303,8 +389,13 @@ static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) assert(lit_neg(begin[0]) < s->size*2); assert(lit_neg(begin[1]) < s->size*2); +#ifdef SAT_USE_WATCH_ARRAYS vecp_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),(void*)c); vecp_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),(void*)c); +#else + clause_watch( s, c, begin[0] ); + clause_watch( s, c, begin[1] ); +#endif return c; } @@ -315,8 +406,10 @@ static void clause_remove(sat_solver2* s, clause* c) assert(lit_neg(lits[0]) < s->size*2); assert(lit_neg(lits[1]) < s->size*2); +#ifdef SAT_USE_WATCH_ARRAYS vecp_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),(void*)c); vecp_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),(void*)c); +#endif if (clause_learnt(c)){ s->stats.learnts--; @@ -325,12 +418,6 @@ static void clause_remove(sat_solver2* s, clause* c) s->stats.clauses--; s->stats.clauses_literals -= clause_size(c); } - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - ABC_FREE(c); -#else -// Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); -#endif } @@ -358,13 +445,15 @@ void sat_solver2_setnvars(sat_solver2* s,int n) int var; if (s->cap < n){ - + while (s->cap < n) s->cap = s->cap*2+1; +#ifdef SAT_USE_WATCH_ARRAYS s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); -// s->activity = ABC_REALLOC(double, s->activity, s->cap); +#else + s->pWatches = ABC_REALLOC(clause*,s->pWatches, s->cap*2); +#endif s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); -// s->factors = ABC_REALLOC(double, s->factors, s->cap); s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap); s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap); @@ -372,13 +461,18 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->tags = ABC_REALLOC(lbool, s->tags, s->cap); s->trail = ABC_REALLOC(lit, s->trail, s->cap); s->polarity = ABC_REALLOC(char, s->polarity, s->cap); + } for (var = s->size; var < n; var++){ +#ifdef SAT_USE_WATCH_ARRAYS vecp_new(&s->wlists[2*var]); vecp_new(&s->wlists[2*var+1]); +#else + s->pWatches[2*var] = NULL; + s->pWatches[2*var+1] = NULL; +#endif s->activity [var] = (1<<10); -// s->factors [var] = 0; s->assigns [var] = l_Undef; s->orderpos [var] = veci_size(&s->order); s->reasons [var] = (clause*)0; @@ -762,13 +856,241 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) } +static inline clause* clause_propagate__( sat_solver2* s, lit Lit ) +{ + clause ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i, sig, Counter = 0; + s->stats.propagations++; + if ( s->pWatches[Lit] == NULL ) + return NULL; + // iterate through the literals + ppPrev = s->pWatches + Lit; + for ( pCur = *ppPrev; pCur; pCur = *ppPrev ) + { + Counter++; + // make sure the false literal is in the second literal of the clause + if ( pCur->lits[0] == LitF ) + { + pCur->lits[0] = pCur->lits[1]; + pCur->lits[1] = LitF; + pTemp = pCur->pNext[0]; + pCur->pNext[0] = pCur->pNext[1]; + pCur->pNext[1] = pTemp; + } + assert( pCur->lits[1] == LitF ); + + // if the first literal is true, the clause is satisfied +// if ( pCur->lits[0] == s->pAssigns[lit_var(pCur->lits[0])] ) + sig = !lit_sign(pCur->lits[0]); sig += sig - 1; + if (s->assigns[lit_var(pCur->lits[0])] == sig) + { + ppPrev = &pCur->pNext[1]; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < clause_size(pCur); i++ ) + { + // skip the case when the literal is false +// if ( lit_neg(pCur->lits[i]) == p->pAssigns[lit_var(pCur->lits[i])] ) + sig = lit_sign(pCur->lits[i]); sig += sig - 1; + if (s->assigns[lit_var(pCur->lits[i])] == sig) + continue; + // the literal is either true or unassigned - watch it + pCur->lits[1] = pCur->lits[i]; + pCur->lits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext[1]; + // add this clause to the watch list of pCur->lits[i] (now it is pCur->lits[1]) + clause_watch( s, pCur, pCur->lits[1] ); + break; + } + if ( i < clause_size(pCur) ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( enqueue(s, pCur->lits[0], pCur) ) + { + ppPrev = &pCur->pNext[1]; + continue; + } + + // conflict detected - return the conflict clause +// printf( "%d ", Counter ); + return pCur; + } +// printf( "%d ", Counter ); + return NULL; +} +clause* sat_solver2_propagate_new__( sat_solver2* s ) +{ + clause* pClause; + int Lit; + while ( s->qtail - s->qhead > 0 ) + { + Lit = s->trail[s->qhead++]; + pClause = clause_propagate__( s, Lit ); + if ( pClause ) + return pClause; + } + return NULL; +} + + +static inline clause* clause_propagate( sat_solver2* s, lit Lit, clause** ppHead, clause** ppTail ) +{ + clause ** ppPrev = ppHead; + clause * pCur, * pTemp, * pPrev = NULL; + lit LitF = lit_neg(Lit); + int i, sig, Counter = 0; + // iterate through the clauses in the linked list + for ( pCur = *ppPrev; pCur; pCur = *ppPrev ) + { + Counter++; + // make sure the false literal is in the second literal of the clause + if ( pCur->lits[0] == LitF ) + { + pCur->lits[0] = pCur->lits[1]; + pCur->lits[1] = LitF; + pTemp = pCur->pNext[0]; + pCur->pNext[0] = pCur->pNext[1]; + pCur->pNext[1] = pTemp; + } + assert( pCur->lits[1] == LitF ); + + // if the first literal is true, the clause is satisfied +// if ( pCur->lits[0] == s->pAssigns[lit_var(pCur->lits[0])] ) + sig = !lit_sign(pCur->lits[0]); sig += sig - 1; + if (s->assigns[lit_var(pCur->lits[0])] == sig) + { + pPrev = pCur; + ppPrev = &pCur->pNext[1]; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < clause_size(pCur); i++ ) + { + // skip the case when the literal is false +// if ( lit_neg(pCur->lits[i]) == p->pAssigns[lit_var(pCur->lits[i])] ) + sig = lit_sign(pCur->lits[i]); sig += sig - 1; + if (s->assigns[lit_var(pCur->lits[i])] == sig) + continue; + // the literal is either true or unassigned - watch it + pCur->lits[1] = pCur->lits[i]; + pCur->lits[i] = LitF; + // remove this clause from the watch list of Lit + if ( pCur->pNext[1] == NULL ) + { + assert( *ppTail == pCur ); + *ppTail = pPrev; + } + *ppPrev = pCur->pNext[1]; + // add this clause to the watch list of pCur->lits[i] (now it is pCur->lits[1]) + clause_watch( s, pCur, pCur->lits[1] ); + break; + } + if ( i < clause_size(pCur) ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( enqueue(s, pCur->lits[0], pCur) ) + { + pPrev = pCur; + ppPrev = &pCur->pNext[1]; + continue; + } + + // conflict detected - return the conflict clause +// printf( "%d ", Counter ); + return pCur; + } +// printf( "%d ", Counter ); + return NULL; +} +clause* sat_solver2_propagate_new( sat_solver2* s ) +{ + clause* pClause,* pHead,* pTail; + int Lit, Flag; + while ( s->qtail - s->qhead > 0 ) + { + s->stats.propagations++; + Lit = s->trail[s->qhead++]; + if ( s->pWatches[Lit] == NULL ) + continue; + // get head and tail + pTail = s->pWatches[Lit]; +/* + if ( pTail->lits[0] == lit_neg(Lit) ) + { + pHead = pTail->pNext[0]; + pTail->pNext[0] = NULL; + } + else + { + assert( pTail->lits[1] == lit_neg(Lit) ); + pHead = pTail->pNext[1]; + pTail->pNext[1] = NULL; + } +*/ +/* + Flag = pTail->lits[1] == lit_neg(Lit); + assert( pTail->lits[0] == lit_neg(Lit) || Flag ); + pHead = pTail->pNext[Flag]; + pTail->pNext[Flag] = NULL; +*/ + assert( pTail->lits[0] == lit_neg(Lit) || pTail->lits[1] == lit_neg(Lit) ); + pHead = pTail->pNext[pTail->lits[1] == lit_neg(Lit)]; + pTail->pNext[pTail->lits[1] == lit_neg(Lit)] = NULL; + + // propagate + pClause = clause_propagate( s, Lit, &pHead, &pTail ); + assert( (pHead == NULL) == (pTail == NULL) ); + // create new list + s->pWatches[Lit] = pTail; +/* + if ( pTail ) + { + if ( pTail->lits[0] == lit_neg(Lit) ) + pTail->pNext[0] = pHead; + else + { + assert( pTail->lits[1] == lit_neg(Lit) ); + pTail->pNext[1] = pHead; + } + } +*/ +/* + if ( pTail ) + { + Flag = pTail->lits[1] == lit_neg(Lit); + assert( pTail->lits[0] == lit_neg(Lit) || Flag ); + pTail->pNext[Flag] = pHead; + } +*/ + if ( pTail ) + { + assert( pTail->lits[0] == lit_neg(Lit) || pTail->lits[1] == lit_neg(Lit) ); + pTail->pNext[pTail->lits[1] == lit_neg(Lit)] = pHead; + } + if ( pClause ) + return pClause; + } + return NULL; +} + + clause* sat_solver2_propagate(sat_solver2* s) { lbool* values = s->assigns; - clause* confl = (clause*)0; + clause* confl = NULL; lit* lits; - //printf("sat_solver2_propagate\n"); +#ifndef SAT_USE_WATCH_ARRAYS + return sat_solver2_propagate_new( s ); +#endif + while (confl == 0 && s->qtail - s->qhead > 0){ lit p = s->trail[s->qhead++]; vecp* ws = sat_solver2_read_wlist(s,p); @@ -835,6 +1157,7 @@ clause* sat_solver2_propagate(sat_solver2* s) return confl; } + static int clause_cmp (const void* x, const void* y) { // return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || ((clause*)x)->act < ((clause*)y)->act) ? -1 : 1; } @@ -873,8 +1196,6 @@ void sat_solver2_reducedb(sat_solver2* s) printf( "Reduction removed %10d clauses (out of %10d)... Value = %d\n", Counter, vecp_size(&s->learnts), extra_lim ); //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); - - vecp_resize(&s->learnts,j); } @@ -956,8 +1277,8 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I if (*nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= *nof_learnts) { // Reduce the set of learnt clauses: - sat_solver2_reducedb(s); - *nof_learnts = *nof_learnts * 12 / 10; //*= 1.1; +// sat_solver2_reducedb(s); +// *nof_learnts = *nof_learnts * 12 / 10; //*= 1.1; } // New variable decision: @@ -1015,18 +1336,6 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->temp_clause); veci_new(&s->conf_final); - // initialize arrays - s->wlists = 0; - s->activity = 0; -// s->factors = 0; - s->assigns = 0; - s->orderpos = 0; - s->reasons = 0; - s->levels = 0; - s->tags = 0; - s->trail = 0; - - // initialize other vars s->size = 0; s->cap = 0; @@ -1056,21 +1365,12 @@ sat_solver2* sat_solver2_new(void) s->stats.learnts_literals = 0; s->stats.max_literals = 0; s->stats.tot_literals = 0; - return s; } void sat_solver2_delete(sat_solver2* s) { - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - int i; - for (i = 0; i < vecp_size(&s->clauses); i++) - ABC_FREE(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - ABC_FREE(vecp_begin(&s->learnts)[i]); -#endif ABC_FREE(s->pMemArray); // delete vectors @@ -1081,21 +1381,19 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->tagged); veci_delete(&s->stack); veci_delete(&s->model); -// veci_delete(&s->act_vars); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); ABC_FREE(s->binary); // delete arrays - if (s->wlists != 0){ + if (s->assigns != 0){ int i; - for (i = 0; i < s->size*2; i++) - vecp_delete(&s->wlists[i]); - - // if one is different from null, all are + if ( s->wlists ) + for (i = 0; i < s->size*2; i++) + vecp_delete(&s->wlists[i]); ABC_FREE(s->wlists ); + ABC_FREE(s->pWatches ); ABC_FREE(s->activity ); -// ABC_FREE(s->factors ); ABC_FREE(s->assigns ); ABC_FREE(s->orderpos ); ABC_FREE(s->reasons ); @@ -1104,8 +1402,6 @@ void sat_solver2_delete(sat_solver2* s) ABC_FREE(s->tags ); ABC_FREE(s->polarity ); } - -// sat_solver2_store_free(s); ABC_FREE(s); } @@ -1189,6 +1485,7 @@ int sat_solver2_simplify(sat_solver2* s) return true; reasons = s->reasons; +/* for (type = 0; type < 2; type++){ vecp* cs = type ? &s->learnts : &s->clauses; clause** cls = (clause**)vecp_begin(cs); @@ -1203,6 +1500,7 @@ int sat_solver2_simplify(sat_solver2* s) } vecp_resize(cs,j); } +*/ //printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses ); s->simpdb_assigns = s->qhead; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 94cf0d63..3ccf96aa 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -98,6 +98,7 @@ struct sat_solver2_t int cla_inc; // Amount to bump next clause with. // float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + clause** pWatches; // watcher lists (for each literal) vecp* wlists; // // double* activity; // A heuristic measurement of the activity of a variable. unsigned*activity; // A heuristic measurement of the activity of a variable. diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index c8569606..ab9641bb 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -154,7 +154,7 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) 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( "inspects : %10d\n", (int)p->stats.inspects ); // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); } @@ -176,7 +176,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ) 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( "inspects : %10d\n", (int)p->stats.inspects ); // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); printf( "memory : %10d\n", p->nMemSize ); } -- cgit v1.2.3