From 1c16c45679252be03fb2be840fc497a1150b0d2a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 27 Nov 2011 16:28:57 -0800 Subject: Started experiments with a new solver. --- src/sat/bsat/satSolver2.c | 892 +++++++++++++--------------------------------- src/sat/bsat/satSolver2.h | 32 +- 2 files changed, 272 insertions(+), 652 deletions(-) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 60ae1bf6..5cb62cf6 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START #define SAT_USE_ANALYZE_FINAL -//#define SAT_USE_WATCH_ARRAYS //================================================================================================= // Debug: @@ -103,28 +102,24 @@ static inline void var_set_level (sat_solver2 * s, int v, int lev ) { s->vi[ //================================================================================================= // Clause datatype + minor functions: -struct clause_t // should have odd number of entries! +struct clause_t // should have even number of entries! { unsigned learnt : 1; unsigned fMark : 1; unsigned fPartA : 1; unsigned fRefed : 1; unsigned nLits : 28; - unsigned act; - unsigned proof; -#ifndef SAT_USE_WATCH_ARRAYS - int pNext[2]; -#endif + int Id; lit lits[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 int clause_size (int nLits) { return sizeof(clause)/4 + nLits + (nLits & 1); } static inline clause* get_clause (sat_solver2* s, int c) { return (clause *)(s->pMemArray + c); } -static inline int clause_id (sat_solver2* s, clause* c) { return ((int *)c - s->pMemArray); } +static inline cla clause_id (sat_solver2* s, clause* c) { return (cla)((int *)c - s->pMemArray); } #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) ) @@ -137,6 +132,65 @@ static inline int clause_id (sat_solver2* s, clause* c) { return ((int 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]; } +//================================================================================================= +// Clause functions: + +static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) +{ + clause* c; + int i, Cid, nLits = end - begin; + assert(nLits > 1); + assert(begin[0] >= 0); + assert(begin[1] >= 0); + 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 ) + { + 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 ); + } + // create clause + c = (clause*)(s->pMemArray + s->nMemSize); + c->learnt = learnt; + c->nLits = nLits; + for (i = 0; i < nLits; i++) + c->lits[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); + } + else + { + c->Id = -(s->stats.clauses + 1); + } + + // extend storage + Cid = s->nMemSize; + s->nMemSize += clause_size(nLits); + if ( s->nMemSize > s->nMemAlloc ) + printf( "Out of memory!!!\n" ); + assert( s->nMemSize <= s->nMemAlloc ); + 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)); + + // remember the last one and first learnt + s->iLast = Cid; + if ( learnt && s->iLearnt == -1 ) + s->iLearnt = Cid; + return Cid; +} + //================================================================================================= // Variable order functions: @@ -178,13 +232,11 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select { int* heap = veci_begin(&s->order); int* orderpos = s->orderpos; -// lbool* values = s->assigns; // Random decision: if (drand(&s->random_seed) < random_var_freq){ int next = irand(&s->random_seed,s->size); assert(next >= 0 && next < s->size); -// if (values[next] == l_Undef) if (var_value(s, next) == varX) return next; } @@ -222,15 +274,13 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select orderpos[heap[i]] = i; } -//printf( "-%d ", next ); -// if (values[next] == l_Undef) if (var_value(s, next) == varX) return next; } - return var_Undef; } + //================================================================================================= // Activity functions: @@ -261,11 +311,11 @@ static inline void act_var_bump(sat_solver2* s, int v) { static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); } static inline void act_clause_rescale(sat_solver2* s) { - clause * c; - int i, clk = clock(); static int Total = 0; - sat_solver_foreach_learnt( s, c, i ) - c->act >>= 14; + int i, clk = clock(); + unsigned * tagged = (unsigned *)veci_begin(&s->claActs); + for (i = 1; i < veci_size(&s->claActs); i++) + tagged[i] >>= 14; s->cla_inc >>= 14; // assert( s->cla_inc > (1<<10)-1 ); s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); @@ -274,219 +324,20 @@ static inline void act_clause_rescale(sat_solver2* s) { Abc_PrintTime( 1, "Time", Total ); } - static inline void act_clause_bump(sat_solver2* s, clause *c) { - c->act += s->cla_inc; - if (c->act & 0x80000000) + 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) act_clause_rescale(s); } //static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; } static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); } -//================================================================================================= -// Clause functions: -#ifndef SAT_USE_WATCH_ARRAYS - -static inline void clause_watch_front( 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)] = clause_id(s, c); -} -static inline void clause_watch( sat_solver2* s, clause* c, lit Lit ) -{ - clause * pList; - cla * 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 == 0 ) - { - *ppList = clause_id(s, c); - *ppNext = clause_id(s, c); - return; - } - // add at the tail - pList = get_clause( s, *ppList ); - if ( pList->lits[0] == Lit ) - { - assert( pList->pNext[0] != 0 ); - *ppNext = pList->pNext[0]; - pList->pNext[0] = clause_id(s, c); - } - else - { - assert( pList->lits[1] == Lit ); - assert( pList->pNext[1] != 0 ); - *ppNext = pList->pNext[1]; - pList->pNext[1] = clause_id(s, c); - } - *ppList = clause_id(s, c); -} -/* -static inline void clause_watch( sat_solver2* s, clause* c, lit Lit ) -{ - int * ppList = s->pWatches[lit_neg(Lit)]; - assert( c->lits[0] == Lit || c->lits[1] == Lit ); - if ( *ppList == NULL ) - c->pNext[c->lits[1] == Lit] = clause_id(s, c); - else - { - clause * pList = get_clause( s, *ppList ); - 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] = clause_id(s, c); - } - s->pWatches[lit_neg(Lit)] = clause_id(s, c); -} -*/ -#endif - -static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt) -{ - clause* c; - int i, Cid, nLits = end - begin; - assert(nLits > 1); - assert(begin[0] >= 0); - assert(begin[1] >= 0); - 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 ) - { - 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 ); - } - // create clause - c = (clause*)(s->pMemArray + s->nMemSize); - c->learnt = learnt; - c->nLits = nLits; - for (i = 0; i < nLits; i++) - c->lits[i] = begin[i]; - - // extend storage - Cid = s->nMemSize; - s->nMemSize += clause_size(nLits); - if ( s->nMemSize > s->nMemAlloc ) - printf( "Out of memory!!!\n" ); - assert( s->nMemSize <= s->nMemAlloc ); - assert(((ABC_PTRUINT_T)c & 7) == 0); - - -#ifdef SAT_USE_WATCH_ARRAYS - 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)); -#else - clause_watch( s, c, begin[0] ); - clause_watch( s, c, begin[1] ); -#endif - - // remember the last one and first learnt - s->iLast = Cid; - if ( learnt && s->iLearnt == -1 ) - s->iLearnt = Cid; - return Cid; -} - - -static void clause_remove(sat_solver2* s, clause* c) -{ - lit* lits = clause_begin(c); - assert(lit_neg(lits[0]) < s->size*2); - assert(lit_neg(lits[1]) < s->size*2); - -#ifdef SAT_USE_WATCH_ARRAYS - 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)); -#endif - - if (clause_learnt(c)){ - s->stats.learnts--; - s->stats.learnts_literals -= clause_nlits(c); - }else{ - s->stats.clauses--; - s->stats.clauses_literals -= clause_nlits(c); - } -} - - -static lbool clause_simplify(sat_solver2* s, clause* c) -{ - lit* lits = clause_begin(c); -// lbool* values = s->assigns; - int i; - - assert(sat_solver2_dlevel(s) == 0); - - for (i = 0; i < clause_nlits(c); i++){ -// lbool sig = !lit_sign(lits[i]); sig += sig - 1; -// if (values[lit_var(lits[i])] == sig) - if (var_value(s, lit_var(lits[i])) == lit_sign(lits[i])) - return l_True; - } - return l_False; -} //================================================================================================= // Minor (solver) functions: -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(veci, s->wlists, s->cap*2); -#else - s->pWatches = ABC_REALLOC(cla, s->pWatches, s->cap*2); -#endif - 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); - } - - for (var = s->size; var < n; var++){ -#ifdef SAT_USE_WATCH_ARRAYS - veci_new(&s->wlists[2*var]); - veci_new(&s->wlists[2*var+1]); -#else - s->pWatches[2*var] = 0; - s->pWatches[2*var+1] = 0; -#endif - *((int*)s->vi + var) = 0; s->vi[var].val = varX; - s->activity [var] = (1<<10); - s->orderpos [var] = veci_size(&s->order); - s->reasons [var] = 0; - - // does not hold because variables enqueued at top level will not be reinserted in the heap - // assert(veci_size(&s->order) == var); - veci_push(&s->order,var); - order_update(s, var); - } - - s->size = n > s->size ? n : s->size; -} - - static inline int enqueue(sat_solver2* s, lit l, int from) { int v = lit_var(l); @@ -579,44 +430,6 @@ static double sat_solver2_progress(sat_solver2* s) //================================================================================================= // Major methods: -static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl) -{ - 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); - veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - while (veci_size(&s->stack) > 0) - { - 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; - } - } - } - } - return true; -} - - /*_________________________________________________________________________________________________ | | analyzeFinal : (p : Lit) -> [void] @@ -705,15 +518,52 @@ static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_fir } } } - 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); + 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); +} + +#endif + + +static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl) +{ + 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); + veci_resize(&s->stack,0); + veci_push(&s->stack,lit_var(l)); + while (veci_size(&s->stack) > 0) + { + 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; + } + } + } + } + return true; } -#endif - - static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) { lit* trail = s->trail; @@ -810,236 +660,6 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) #endif } -#ifndef SAT_USE_WATCH_ARRAYS - -static inline clause* clause_propagate__front( sat_solver2* s, lit Lit ) -{ - clause * pCur; - cla * ppPrev, pThis, pTemp; - lit LitF = lit_neg(Lit); - int i, Counter = 0; - s->stats.propagations++; - if ( s->pWatches[Lit] == 0 ) - return NULL; - // iterate through the literals - ppPrev = s->pWatches + Lit; - for ( pThis = *ppPrev; pThis; pThis = *ppPrev ) - { - Counter++; - // make sure the false literal is in the second literal of the clause - pCur = get_clause( s, pThis ); - 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) - if (var_value(s, lit_var(pCur->lits[0])) == lit_sign(pCur->lits[0])) - { - ppPrev = &pCur->pNext[1]; - continue; - } - - // look for a new literal to watch - for ( i = 2; i < clause_nlits(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) - if (var_value(s, lit_var(pCur->lits[i])) == !lit_sign(pCur->lits[i])) - 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_nlits(pCur) ) // found new watch - continue; - - // clause is unit - enqueue new implication - if ( enqueue(s, pCur->lits[0], clause_id(s,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__front( sat_solver2* s ) -{ - clause* pClause; - lit Lit; - while ( s->qtail - s->qhead > 0 ) - { - Lit = s->trail[s->qhead++]; - pClause = clause_propagate__front( s, Lit ); - if ( pClause ) - return pClause; - } - return NULL; -} - -static inline clause* clause_propagate( sat_solver2* s, lit Lit, int * ppHead, int * ppTail ) -{ - clause * pCur; - cla * ppPrev = ppHead, pThis, pTemp, pPrev = 0; - lit LitF = lit_neg(Lit); - int i, Counter = 0; - // iterate through the literals - for ( pThis = *ppPrev; pThis; pThis = *ppPrev ) - { - Counter++; - // make sure the false literal is in the second literal of the clause - pCur = get_clause( s, pThis ); - 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 ) - if (var_value(s, lit_var(pCur->lits[0])) == lit_sign(pCur->lits[0])) - { - pPrev = pThis; - ppPrev = &pCur->pNext[1]; - continue; - } - - // look for a new literal to watch - for ( i = 2; i < clause_nlits(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 ) - if (var_value(s, lit_var(pCur->lits[i])) == !lit_sign(pCur->lits[i])) - 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] == 0 ) - { - assert( *ppTail == pThis ); - *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_nlits(pCur) ) // found new watch - continue; - - // clause is unit - enqueue new implication - if ( enqueue(s, pCur->lits[0], clause_id(s,pCur)) ) - { - pPrev = pThis; - 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, * pTailC; - cla pHead, pTail; - lit Lit; - while ( s->qtail - s->qhead > 0 ) - { - s->stats.propagations++; - Lit = s->trail[s->qhead++]; - if ( s->pWatches[Lit] == 0 ) - continue; - // get head and tail - pTail = s->pWatches[Lit]; - pTailC = get_clause( s, pTail ); -/* - if ( pTailC->lits[0] == lit_neg(Lit) ) - { - pHead = pTailC->pNext[0]; - pTailC->pNext[0] = NULL; - } - else - { - assert( pTailC->lits[1] == lit_neg(Lit) ); - pHead = pTailC->pNext[1]; - pTailC->pNext[1] = NULL; - } -*/ - if ( s->stats.propagations == 10 ) - { - int s = 0; - } - assert( pTailC->lits[0] == lit_neg(Lit) || pTailC->lits[1] == lit_neg(Lit) ); - pHead = pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)]; - pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)] = 0; - - // propagate - pClause = clause_propagate( s, Lit, &pHead, &pTail ); - assert( (pHead == 0) == (pTail == 0) ); - - // create new list - s->pWatches[Lit] = pTail; -/* - if ( pTail ) - { - pTailC = get_clause( s, pTail ); - if ( pTailC->lits[0] == lit_neg(Lit) ) - pTailC->pNext[0] = pHead; - else - { - assert( pTailC->lits[1] == lit_neg(Lit) ); - pTailC->pNext[1] = pHead; - } - } -*/ - if ( pTail ) - { - pTailC = get_clause( s, pTail ); - assert( pTailC->lits[0] == lit_neg(Lit) || pTailC->lits[1] == lit_neg(Lit) ); - pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)] = pHead; - } - if ( pClause ) - return pClause; - } - return NULL; -} - -#endif - clause* sat_solver2_propagate(sat_solver2* s) { clause * c, * confl = NULL; @@ -1047,11 +667,6 @@ clause* sat_solver2_propagate(sat_solver2* s) lit* lits, false_lit, p, * stop, * k; cla* begin,* end, *i, *j; - -#ifndef SAT_USE_WATCH_ARRAYS - return sat_solver2_propagate_new( s ); -#endif - while (confl == 0 && s->qtail - s->qhead > 0){ p = s->trail[s->qhead++]; ws = sat_solver2_read_wlist(s,p); @@ -1113,44 +728,107 @@ next: i++; } -static int clause_cmp (const void* x, const void* y) { -// return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } - return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || ((clause*)x)->act < ((clause*)y)->act) ? -1 : 1; } + +static void clause_remove(sat_solver2* s, clause* 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)); + + if (clause_learnt(c)){ + s->stats.learnts--; + s->stats.learnts_literals -= clause_nlits(c); + }else{ + s->stats.clauses--; + s->stats.clauses_literals -= clause_nlits(c); + } +} + + +static lbool clause_simplify(sat_solver2* s, clause* c) +{ + lit* lits = clause_begin(c); + int i; + assert(sat_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; + } + return l_False; +} + +int sat_solver2_simplify(sat_solver2* s) +{ +// int type; + int Counter = 0; + assert(sat_solver2_dlevel(s) == 0); + if (sat_solver2_propagate(s) != 0) + return false; + 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++){ + clause * c = get_clause(s,cls[i]); + if (s->reasons[lit_var(*clause_begin(c))] != 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; +} void sat_solver2_reducedb(sat_solver2* s) { -/* - vecp Vec, * pVec = &Vec; - double extra_limD = (double)s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity - unsigned extra_lim = (extra_limD < 1.0) ? 1 : (int)extra_limD; - int i, j, * pBeg, * pEnd; - - // move clauses into vector - vecp_new( pVec ); - pBeg = (int*)veci_begin(&s->learnts); - pEnd = pBeg + veci_size(&s->learnts); - while ( pBeg < pEnd ) - vecp_push( pVec, get_clause(s,*pBeg++) ); - sat_solver2_sort( vecp_begin(pVec), vecp_size(pVec), &clause_cmp ); - vecp_delete( pVec ); - - // compact clauses - pBeg = (int*)veci_begin(&s->learnts); - for (i = j = 0; i < vecp_size(pVec); i++) + clause * c; + cla Cid; + int clk = clock(); + + // sort the clauses by activity + int nLearnts = veci_size(&s->claActs) - 1; + extern int * Abc_SortCost( int * pCosts, int nSize ); + int * pPerm, * pCosts = veci_begin(&s->claActs); + pPerm = Abc_SortCost( pCosts, veci_size(&s->claActs) ); + assert( pCosts[pPerm[1]] <= pCosts[pPerm[veci_size(&s->claActs)-1]] ); + + // mark clauses to be removed { - clause * c = ((clause**)vecp_begin(pVec))[i]; - int Cid = clause_id(s,c); -// printf( "%d ", c->act ); - if (clause_nlits(c) > 2 && s->reasons[lit_var(*clause_begin(c))] != Cid && (i < vecp_size(pVec)/2 || c->act < extra_lim) ) - clause_remove(s,c); - else - pBeg[j++] = Cid; + double extra_limD = (double)s->cla_inc / nLearnts; // Remove any clause below this activity + unsigned extra_lim = (extra_limD < 1.0) ? 1 : (int)extra_limD; + unsigned * pActs = (unsigned *)veci_begin(&s->claActs); + int k = 1, Counter = 0; + 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->fMark = 1; + Counter++; + } + k++; + } +printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d ", Counter, nLearnts, extra_lim ); +Abc_PrintTime( 1, "Time", clock() - clk ); } -printf( "Reduction removed %10d clauses (out of %10d)... Value = %d\n", veci_size(&s->learnts) - j, veci_size(&s->learnts), extra_lim ); - veci_resize(&s->learnts,j); -*/ + 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; @@ -1230,8 +908,8 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I if (*nof_learnts >= 0 && s->stats.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 * 11 / 10; //*= 1.1; } // New variable decision: @@ -1273,8 +951,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; - 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); @@ -1284,6 +961,10 @@ 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); // initialize other s->iLearnt = -1; // the first learnt clause @@ -1294,6 +975,36 @@ sat_solver2* sat_solver2_new(void) return s; } +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; + + 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); + } + + for (var = s->size; var < n; var++){ + veci_new(&s->wlists[2*var]); + veci_new(&s->wlists[2*var+1]); + *((int*)s->vi + var) = 0; s->vi[var].val = varX; + s->activity [var] = (1<<10); + s->orderpos [var] = veci_size(&s->order); + s->reasons [var] = 0; + // does not hold because variables enqueued at top level will not be reinserted in the heap + // assert(veci_size(&s->order) == var); + veci_push(&s->order,var); + order_update(s, var); + } + s->size = n > s->size ? n : s->size; +} void sat_solver2_delete(sat_solver2* s) { @@ -1307,6 +1018,8 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->model); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); + veci_delete(&s->claActs); + veci_delete(&s->claProofs); // delete arrays if (s->vi != 0){ @@ -1315,7 +1028,6 @@ void sat_solver2_delete(sat_solver2* s) for (i = 0; i < s->size*2; i++) veci_delete(&s->wlists[i]); ABC_FREE(s->wlists ); - ABC_FREE(s->pWatches ); ABC_FREE(s->vi ); ABC_FREE(s->activity ); ABC_FREE(s->orderpos ); @@ -1388,45 +1100,6 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) } -int sat_solver2_simplify(sat_solver2* s) -{ -// int type; - int Counter = 0; - - assert(sat_solver2_dlevel(s) == 0); - - if (sat_solver2_propagate(s) != 0) - return false; - - 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++){ - clause * c = get_clause(s,cls[i]); - if (s->reasons[lit_var(*clause_begin(c))] != 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; -} - double luby2(double y, int x) { int size, seq; @@ -1625,74 +1298,5 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } -int sat_solver2_nvars(sat_solver2* s) -{ - return s->size; -} - - -int sat_solver2_nclauses(sat_solver2* s) -{ - return (int)s->stats.clauses; -} - - -int sat_solver2_nconflicts(sat_solver2* s) -{ - return (int)s->stats.conflicts; -} - -//================================================================================================= -// Sorting functions (sigh): - -static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) -{ - int i, j, best_i; - void* tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (comp(array[j], array[best_i]) < 0) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - - -static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) -{ - if (size <= 15) - selectionsort(array, size, comp); - - else{ - void* pivot = array[irand(seed, size)]; - void* tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(comp(array[i], pivot)<0); - do j--; while(comp(pivot, array[j])<0); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sortrnd(array , i , comp, seed); - sortrnd(&array[i], size-i, comp, seed); - } -} - -void sat_solver2_sort(void** array, int size, int(*comp)(const void *, const void *)) -{ -// int i; - double seed = 91648253; - sortrnd(array,size,comp,&seed); -// for ( i = 1; i < size; i++ ) -// assert(comp(array[i-1], array[i])<0); -} ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 2725c92b..5ccb2c33 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -100,7 +100,6 @@ struct sat_solver2_t int iLearnt; // the first learnt clause int iLast; // the last learnt clause veci* wlists; // watcher lists (for each literal) - cla* pWatches; // watcher lists (for each literal) // clause memory int * pMemArray; @@ -111,6 +110,8 @@ struct sat_solver2_t 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. + veci claActs; // clause activities + veci claProofs; // clause proofs // internal state varinfo * vi; // variable information @@ -134,24 +135,39 @@ struct sat_solver2_t }; -static int sat_solver2_var_value( sat_solver2* s, int v ) +static inline int sat_solver2_nvars(sat_solver2* s) +{ + return s->size; +} + +static inline int sat_solver2_nclauses(sat_solver2* s) +{ + return (int)s->stats.clauses; +} + +static inline int sat_solver2_nconflicts(sat_solver2* s) +{ + return (int)s->stats.conflicts; +} + +static inline int sat_solver2_var_value( sat_solver2* s, int v ) { assert( s->model.ptr != NULL && v < s->size ); return (int)(s->model.ptr[v] == l_True); } -static int sat_solver2_var_literal( sat_solver2* s, int v ) +static inline int sat_solver2_var_literal( sat_solver2* s, int v ) { assert( s->model.ptr != NULL && v < s->size ); return toLitCond( v, s->model.ptr[v] != l_True ); } -static void sat_solver2_act_var_clear(sat_solver2* s) +static inline void sat_solver2_act_var_clear(sat_solver2* s) { int i; for (i = 0; i < s->size; i++) s->activity[i] = 0;//.0; s->var_inc = 1.0; } -static void sat_solver2_compress(sat_solver2* s) +static inline void sat_solver2_compress(sat_solver2* s) { if ( s->qtail != s->qhead ) { @@ -160,20 +176,20 @@ static void sat_solver2_compress(sat_solver2* s) } } -static int sat_solver2_final(sat_solver2* s, int ** ppArray) +static inline int sat_solver2_final(sat_solver2* s, int ** ppArray) { *ppArray = s->conf_final.ptr; return s->conf_final.size; } -static int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit) +static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit) { int nRuntimeLimit = s->nRuntimeLimit; s->nRuntimeLimit = Limit; return nRuntimeLimit; } -static int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) +static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) { int fNotUseRandomOld = s->fNotUseRandom; s->fNotUseRandom = fNotUseRandom; -- cgit v1.2.3