Skip to content

A
abc
Commit 1c16c456 by Alan Mishchenko
Options

Started experiments with a new solver.

parent fc4ab6bd
Showing with 267 additions and 647 deletions
src/sat/bsat/satSolver2.c
...@@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
#define SAT_USE_ANALYZE_FINAL #define SAT_USE_ANALYZE_FINAL
//#define SAT_USE_WATCH_ARRAYS
//================================================================================================= //=================================================================================================
// Debug: // Debug:
...@@ -103,28 +102,24 @@ static inline void var_set_level (sat_solver2 * s, int v, int lev ) { s->vi[ ...@@ -103,28 +102,24 @@ static inline void var_set_level (sat_solver2 * s, int v, int lev ) { s->vi[
//================================================================================================= //=================================================================================================
// Clause datatype + minor functions: // 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 learnt : 1;
unsigned fMark : 1; unsigned fMark : 1;
unsigned fPartA : 1; unsigned fPartA : 1;
unsigned fRefed : 1; unsigned fRefed : 1;
unsigned nLits : 28; unsigned nLits : 28;
unsigned act; int Id;
unsigned proof;
#ifndef SAT_USE_WATCH_ARRAYS
int pNext[2];
#endif
lit lits[0]; lit lits[0];
}; };
static inline lit* clause_begin (clause* c) { return c->lits; } static inline lit* clause_begin (clause* c) { return c->lits; }
static inline int clause_learnt (clause* c) { return c->learnt; } static inline int clause_learnt (clause* c) { return c->learnt; }
static inline int clause_nlits (clause* c) { return c->nLits; } 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 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 ) \ #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) ) for ( i = 16; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
...@@ -138,6 +133,65 @@ static inline int sat_solver2_dlevel(sat_solver2* s) { return vec ...@@ -138,6 +133,65 @@ static inline int sat_solver2_dlevel(sat_solver2* s) { return vec
static inline veci* sat_solver2_read_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; } 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: // Variable order functions:
static inline void order_update(sat_solver2* s, int v) // updateorder static inline void order_update(sat_solver2* s, int v) // updateorder
...@@ -178,13 +232,11 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select ...@@ -178,13 +232,11 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select
{ {
int* heap = veci_begin(&s->order); int* heap = veci_begin(&s->order);
int* orderpos = s->orderpos; int* orderpos = s->orderpos;
// lbool* values = s->assigns;
// Random decision: // Random decision:
if (drand(&s->random_seed) < random_var_freq){ if (drand(&s->random_seed) < random_var_freq){
int next = irand(&s->random_seed,s->size); int next = irand(&s->random_seed,s->size);
assert(next >= 0 && next < s->size); assert(next >= 0 && next < s->size);
// if (values[next] == l_Undef)
if (var_value(s, next) == varX) if (var_value(s, next) == varX)
return next; return next;
} }
...@@ -222,15 +274,13 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select ...@@ -222,15 +274,13 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select
orderpos[heap[i]] = i; orderpos[heap[i]] = i;
} }
//printf( "-%d ", next );
// if (values[next] == l_Undef)
if (var_value(s, next) == varX) if (var_value(s, next) == varX)
return next; return next;
} }
return var_Undef; return var_Undef;
} }
//================================================================================================= //=================================================================================================
// Activity functions: // Activity functions:
...@@ -261,11 +311,11 @@ static inline void act_var_bump(sat_solver2* s, int v) { ...@@ -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_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
static inline void act_clause_rescale(sat_solver2* s) { static inline void act_clause_rescale(sat_solver2* s) {
clause * c;
int i, clk = clock();
static int Total = 0; static int Total = 0;
sat_solver_foreach_learnt( s, c, i ) int i, clk = clock();
c->act >>= 14; unsigned * tagged = (unsigned *)veci_begin(&s->claActs);
for (i = 1; i < veci_size(&s->claActs); i++)
tagged[i] >>= 14;
s->cla_inc >>= 14; s->cla_inc >>= 14;
// assert( s->cla_inc > (1<<10)-1 ); // assert( s->cla_inc > (1<<10)-1 );
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
...@@ -274,219 +324,20 @@ static inline void act_clause_rescale(sat_solver2* s) { ...@@ -274,219 +324,20 @@ static inline void act_clause_rescale(sat_solver2* s) {
Abc_PrintTime( 1, "Time", Total ); Abc_PrintTime( 1, "Time", Total );
} }
static inline void act_clause_bump(sat_solver2* s, clause *c) { static inline void act_clause_bump(sat_solver2* s, clause *c) {
c->act += s->cla_inc; assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
if (c->act & 0x80000000) ((unsigned *)veci_begin(&s->claActs))[c->Id] += s->cla_inc;
if (((unsigned *)veci_begin(&s->claActs))[c->Id] & 0x80000000)
act_clause_rescale(s); 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_decay; }
static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); } 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: // 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) static inline int enqueue(sat_solver2* s, lit l, int from)
{ {
int v = lit_var(l); int v = lit_var(l);
...@@ -579,44 +430,6 @@ static double sat_solver2_progress(sat_solver2* s) ...@@ -579,44 +430,6 @@ static double sat_solver2_progress(sat_solver2* s)
//================================================================================================= //=================================================================================================
// Major methods: // 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] | analyzeFinal : (p : Lit) -> [void]
...@@ -711,9 +524,46 @@ static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_fir ...@@ -711,9 +524,46 @@ static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_fir
veci_resize(&s->tagged,0); veci_resize(&s->tagged,0);
} }
#endif #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;
}
static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
{ {
lit* trail = s->trail; lit* trail = s->trail;
...@@ -810,236 +660,6 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt) ...@@ -810,236 +660,6 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
#endif #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* sat_solver2_propagate(sat_solver2* s)
{ {
clause * c, * confl = NULL; clause * c, * confl = NULL;
...@@ -1047,11 +667,6 @@ clause* sat_solver2_propagate(sat_solver2* s) ...@@ -1047,11 +667,6 @@ clause* sat_solver2_propagate(sat_solver2* s)
lit* lits, false_lit, p, * stop, * k; lit* lits, false_lit, p, * stop, * k;
cla* begin,* end, *i, *j; 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){ while (confl == 0 && s->qtail - s->qhead > 0){
p = s->trail[s->qhead++]; p = s->trail[s->qhead++];
ws = sat_solver2_read_wlist(s,p); ws = sat_solver2_read_wlist(s,p);
...@@ -1113,44 +728,107 @@ next: i++; ...@@ -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; }
void sat_solver2_reducedb(sat_solver2* s) 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;
/* /*
vecp Vec, * pVec = &Vec; for (type = 0; type < 2; type++){
double extra_limD = (double)s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity veci* cs = type ? &s->learnts : &s->clauses;
unsigned extra_lim = (extra_limD < 1.0) ? 1 : (int)extra_limD; int* cls = (int*)veci_begin(cs);
int i, j, * pBeg, * pEnd; int i, j;
for (j = i = 0; i < veci_size(cs); i++){
// move clauses into vector clause * c = get_clause(s,cls[i]);
vecp_new( pVec ); if (s->reasons[lit_var(*clause_begin(c))] != cls[i] &&
pBeg = (int*)veci_begin(&s->learnts); clause_simplify(s,c) == l_True)
pEnd = pBeg + veci_size(&s->learnts); clause_remove(s,c), Counter++;
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 = ((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 else
pBeg[j++] = Cid; cls[j++] = cls[i];
}
veci_resize(cs,j);
} }
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);
*/ */
//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)
{
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
{
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 );
}
ABC_FREE( pPerm );
} }
static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts) static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts)
{ {
double var_decay = 0.95; double var_decay = 0.95;
...@@ -1230,8 +908,8 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I ...@@ -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) if (*nof_learnts >= 0 && s->stats.learnts - s->qtail >= *nof_learnts)
{ {
// Reduce the set of learnt clauses: // Reduce the set of learnt clauses:
// sat_solver2_reducedb(s); sat_solver2_reducedb(s);
// *nof_learnts = *nof_learnts * 12 / 10; //*= 1.1; *nof_learnts = *nof_learnts * 11 / 10; //*= 1.1;
} }
// New variable decision: // New variable decision:
...@@ -1273,8 +951,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I ...@@ -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* sat_solver2_new(void)
{ {
sat_solver2 * s; sat_solver2 * s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
// initialize vectors // initialize vectors
veci_new(&s->order); veci_new(&s->order);
...@@ -1284,6 +961,10 @@ sat_solver2* sat_solver2_new(void) ...@@ -1284,6 +961,10 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->model); veci_new(&s->model);
veci_new(&s->temp_clause); veci_new(&s->temp_clause);
veci_new(&s->conf_final); 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 // initialize other
s->iLearnt = -1; // the first learnt clause s->iLearnt = -1; // the first learnt clause
...@@ -1294,6 +975,36 @@ sat_solver2* sat_solver2_new(void) ...@@ -1294,6 +975,36 @@ sat_solver2* sat_solver2_new(void)
return s; 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) void sat_solver2_delete(sat_solver2* s)
{ {
...@@ -1307,6 +1018,8 @@ 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->model);
veci_delete(&s->temp_clause); veci_delete(&s->temp_clause);
veci_delete(&s->conf_final); veci_delete(&s->conf_final);
veci_delete(&s->claActs);
veci_delete(&s->claProofs);
// delete arrays // delete arrays
if (s->vi != 0){ if (s->vi != 0){
...@@ -1315,7 +1028,6 @@ void sat_solver2_delete(sat_solver2* s) ...@@ -1315,7 +1028,6 @@ void sat_solver2_delete(sat_solver2* s)
for (i = 0; i < s->size*2; i++) for (i = 0; i < s->size*2; i++)
veci_delete(&s->wlists[i]); veci_delete(&s->wlists[i]);
ABC_FREE(s->wlists ); ABC_FREE(s->wlists );
ABC_FREE(s->pWatches );
ABC_FREE(s->vi ); ABC_FREE(s->vi );
ABC_FREE(s->activity ); ABC_FREE(s->activity );
ABC_FREE(s->orderpos ); ABC_FREE(s->orderpos );
...@@ -1388,45 +1100,6 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) ...@@ -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) double luby2(double y, int x)
{ {
int size, seq; int size, seq;
...@@ -1625,74 +1298,5 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -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 ABC_NAMESPACE_IMPL_END
src/sat/bsat/satSolver2.h
...@@ -100,7 +100,6 @@ struct sat_solver2_t ...@@ -100,7 +100,6 @@ struct sat_solver2_t
int iLearnt; // the first learnt clause int iLearnt; // the first learnt clause
int iLast; // the last learnt clause int iLast; // the last learnt clause
veci* wlists; // watcher lists (for each literal) veci* wlists; // watcher lists (for each literal)
cla* pWatches; // watcher lists (for each literal)
// clause memory // clause memory
int * pMemArray; int * pMemArray;
...@@ -111,6 +110,8 @@ struct sat_solver2_t ...@@ -111,6 +110,8 @@ struct sat_solver2_t
int var_inc; // Amount to bump next variable with. int var_inc; // Amount to bump next variable with.
int cla_inc; // Amount to bump next clause with. int cla_inc; // Amount to bump next clause with.
unsigned* activity; // A heuristic measurement of the activity of a variable. unsigned* activity; // A heuristic measurement of the activity of a variable.
veci claActs; // clause activities
veci claProofs; // clause proofs
// internal state // internal state
varinfo * vi; // variable information varinfo * vi; // variable information
...@@ -134,24 +135,39 @@ struct sat_solver2_t ...@@ -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 ); assert( s->model.ptr != NULL && v < s->size );
return (int)(s->model.ptr[v] == l_True); 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 ); assert( s->model.ptr != NULL && v < s->size );
return toLitCond( v, s->model.ptr[v] != l_True ); 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; int i;
for (i = 0; i < s->size; i++) for (i = 0; i < s->size; i++)
s->activity[i] = 0;//.0; s->activity[i] = 0;//.0;
s->var_inc = 1.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 ) if ( s->qtail != s->qhead )
{ {
...@@ -160,20 +176,20 @@ static void sat_solver2_compress(sat_solver2* s) ...@@ -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; *ppArray = s->conf_final.ptr;
return s->conf_final.size; 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; int nRuntimeLimit = s->nRuntimeLimit;
s->nRuntimeLimit = Limit; s->nRuntimeLimit = Limit;
return nRuntimeLimit; 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; int fNotUseRandomOld = s->fNotUseRandom;
s->fNotUseRandom = fNotUseRandom; s->fNotUseRandom = fNotUseRandom;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment