Skip to content

A
abc
Commit 6c766b4f by Alan Mishchenko
Options

Implementing rollback in the updated solver.

parent dea5708d
Showing with 192 additions and 55 deletions
src/sat/bsat/satProof.c
......@@ -215,7 +215,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
SeeAlso []
***********************************************************************/
void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
{
satset * pNext;
int i, hNode;
......@@ -223,7 +223,7 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V
return;
// start with node
pNode->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 );
Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNode) << 1 );
// perform DFS search
while ( Vec_IntSize(vStack) )
{
......@@ -236,12 +236,12 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V
// extracted first time
Vec_IntPush( vStack, hNode ^ 1 ); // add second time
// add its anticedents ;
pNode = Proof_NodeRead( p, hNode >> 1 );
Proof_NodeForeachFanin( p, pNode, pNext, i )
pNode = Proof_NodeRead( vProof, hNode >> 1 );
Proof_NodeForeachFanin( vProof, pNode, pNext, i )
if ( pNext && !pNext->Id )
{
pNext->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time
Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNext) << 1 ); // add first time
}
}
}
......@@ -314,17 +314,17 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
SeeAlso []
***********************************************************************/
void Proof_CollectUsed_rec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
void Proof_CollectUsed_rec( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed )
{
satset * pNext;
int i;
if ( pNode->Id )
return;
pNode->Id = 1;
Proof_NodeForeachFanin( p, pNode, pNext, i )
Proof_NodeForeachFanin( vProof, pNode, pNext, i )
if ( pNext && !pNext->Id )
Proof_CollectUsed_rec( p, pNext, vUsed );
Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) );
Proof_CollectUsed_rec( vProof, pNext, vUsed );
Vec_IntPush( vUsed, Proof_NodeHandle(vProof, pNode) );
}
/**Function*************************************************************
......@@ -637,7 +637,7 @@ void Sat_ProofCheck( sat_solver2 * s )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Rec_Int_t * vResolves;
Vec_Int_t * vUsed, * vTemp;
......@@ -731,7 +731,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
satset * pNode, * pFanin;
......@@ -822,7 +822,7 @@ void * Sat_ProofCore( sat_solver2 * s )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Int_t * vCore, * vUsed;
// collect visited clauses
......
src/sat/bsat/satSolver2.c
......@@ -141,10 +141,13 @@ static inline void solver2_clear_marks(sat_solver2* s) {
//=================================================================================================
// Clause datatype + minor functions:
static inline satset* clause_read (sat_solver2* s, cla h) { return satset_read( &s->clauses, h ); }
static inline cla clause_handle (sat_solver2* s, satset* c) { return satset_handle( &s->clauses, c ); }
static inline int clause_check (sat_solver2* s, satset* c) { return satset_check( &s->clauses, c ); }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (clause_handle(s,c)<<2) | 1; }
static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); }
static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; }
static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; }
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
......@@ -161,7 +164,7 @@ void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s
int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; }
#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 )
#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->clauses, c, h, s->hLearntFirst )
#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 )
//=================================================================================================
// Simple helpers:
......@@ -377,26 +380,27 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i
assert(nLits < 1 || lit_var(begin[0]) < s->size);
assert(nLits < 2 || lit_var(begin[1]) < s->size);
// add memory if needed
if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap )
// assign clause ID
if ( learnt )
{
int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
// memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) );
// printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
s->clauses.cap = nMemAlloc;
if ( veci_size(&s->clauses) == 0 )
veci_push( &s->clauses, -1 );
if ( veci_size(&s->learnts) + satset_size(nLits) > s->learnts.cap )
{
int nMemAlloc = s->learnts.cap ? 2 * s->learnts.cap : (1 << 20);
s->learnts.ptr = ABC_REALLOC( int, veci_begin(&s->learnts), nMemAlloc );
// printf( "Reallocing from %d to %d...\n", s->learnts.cap, nMemAlloc );
s->learnts.cap = nMemAlloc;
if ( veci_size(&s->learnts) == 0 )
veci_push( &s->learnts, -1 );
}
// create clause
c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
c = (satset*)(veci_begin(&s->learnts) + veci_size(&s->learnts));
((int*)c)[0] = 0;
c->learnt = learnt;
c->nEnts = nLits;
for (i = 0; i < nLits; i++)
c->pEnts[i] = begin[i];
// assign clause ID
if ( learnt )
{
// count the clause
s->stats.learnts++;
s->stats.learnts_literals += nLits;
c->Id = s->stats.learnts;
......@@ -406,28 +410,44 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i
veci_push(&s->claProofs, proof_id);
if ( nLits > 2 )
act_clause_bump( s,c );
// extend storage
Cid = (veci_size(&s->learnts) << 1) | 1;
s->learnts.size += satset_size(nLits);
assert( veci_size(&s->learnts) <= s->learnts.cap );
assert(((ABC_PTRUINT_T)c & 3) == 0);
// printf( "Clause for proof %d: ", proof_id );
// satset_print( c );
}
else
{
if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap )
{
int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
// printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
s->clauses.cap = nMemAlloc;
if ( veci_size(&s->clauses) == 0 )
veci_push( &s->clauses, -1 );
}
// create clause
c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
((int*)c)[0] = 0;
c->learnt = learnt;
c->nEnts = nLits;
for (i = 0; i < nLits; i++)
c->pEnts[i] = begin[i];
// count the clause
s->stats.clauses++;
s->stats.clauses_literals += nLits;
c->Id = s->stats.clauses;
}
// extend storage
Cid = veci_size(&s->clauses);
Cid = (veci_size(&s->clauses) << 1);
s->clauses.size += satset_size(nLits);
assert( veci_size(&s->clauses) <= s->clauses.cap );
assert(((ABC_PTRUINT_T)c & 3) == 0);
// remember the last one and first learnt
// remember the last one
s->hLearntLast = Cid;
if ( learnt && s->hLearntFirst == -1 )
s->hLearntFirst = Cid;
}
// watch the clause
if ( nLits > 1 ){
veci_push(solver2_wlist(s,lit_neg(begin[0])),Cid);
......@@ -439,7 +459,7 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i
//=================================================================================================
// Minor (solver) functions:
static inline int solver2_enqueue(sat_solver2* s, lit l, int from)
static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
{
int v = lit_var(l);
#ifdef VERBOSEDEBUG
......@@ -507,7 +527,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
int Cid = clause_create_new(s,begin,end,1, proof_id);
cla Cid = clause_create_new(s,begin,end,1, proof_id);
assert(veci_size(cls) > 0);
if ( veci_size(cls) == 1 )
{
......@@ -1195,13 +1215,9 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->min_lit_order);
veci_new(&s->min_step_order);
veci_new(&s->learnt_live);
veci_new(&s->proofs); veci_push(&s->proofs, -1);
veci_new(&s->claActs); veci_push(&s->claActs, -1);
veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
// initialize other
s->hLearntFirst = -1; // the first learnt clause
s->hLearntLast = -1; // the last learnt clause
#ifdef USE_FLOAT_ACTIVITY2
s->var_inc = 1;
s->cla_inc = 1;
......@@ -1221,12 +1237,28 @@ sat_solver2* sat_solver2_new(void)
s->fProofLogging = 0;
#endif
// prealloc some arrays
// prealloc clause
assert( !s->clauses.ptr );
s->clauses.cap = (1 << 20);
s->clauses.ptr = ABC_ALLOC( int, s->clauses.cap );
veci_push(&s->clauses, -1);
// prealloc learnt
assert( !s->learnts.ptr );
s->learnts.cap = (1 << 20);
s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap );
veci_push(&s->learnts, -1);
// prealloc proofs
if ( s->fProofLogging )
{
assert( !s->proofs.ptr );
s->proofs.cap = (1 << 20);
s->proofs.ptr = ABC_REALLOC( int, s->proofs.ptr, s->proofs.cap );
s->proofs.ptr = ABC_ALLOC( int, s->proofs.cap );
veci_push(&s->proofs, -1);
}
// initialize clause pointers
s->hClausePivot = 1;
s->hLearntPivot = 1;
s->hLearntLast = -1; // the last learnt clause
return s;
}
......@@ -1254,7 +1286,11 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
}
for (var = s->size; var < n; var++){
assert(!s->wlists[2*var].size);
assert(!s->wlists[2*var+1].size);
if ( s->wlists[2*var].ptr == NULL )
veci_new(&s->wlists[2*var]);
if ( s->wlists[2*var+1].ptr == NULL )
veci_new(&s->wlists[2*var+1]);
*((int*)s->vi + var) = 0; s->vi[var].val = varX;
s->orderpos[var] = veci_size(&s->order);
......@@ -1304,6 +1340,7 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->claActs);
veci_delete(&s->claProofs);
veci_delete(&s->clauses);
veci_delete(&s->learnts);
// delete arrays
if (s->vi != 0){
......@@ -1460,15 +1497,17 @@ void solver2_reducedb(sat_solver2* s)
veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts );
// remap clause proofs and clauses
hHandle = s->hLearntFirst;
pArray = veci_begin(&s->claProofs);
hHandle = 1;
pArray = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
pArray2 = veci_begin(&s->claActs);
satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i )
satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
{
if ( pArray )
pArray[i+1] = pArray[c->Id];
pArray2[i+1] = pArray2[c->Id];
c->Id = hHandle; hHandle += satset_size(c->nEnts);
}
if ( s->fProofLogging )
veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1);
veci_resize(&s->claActs,veci_size(&s->learnt_live)+1);
......@@ -1477,33 +1516,120 @@ void solver2_reducedb(sat_solver2* s)
{
pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( pArray[k] < s->hLearntFirst )
if ( pArray[k] & 1 )
pArray[j++] = pArray[k];
else if ( !(c = clause_read(s, pArray[k]))->mark )
pArray[j++] = c->Id;
veci_resize(&s->wlists[i],j);
}
// compact units
if ( s->fProofLogging )
for ( i = 0; i < s->size; i++ )
if ( s->units[i] >= s->hLearntFirst )
if ( s->units[i] && (s->units[i] & 1) )
s->units[i] = clause_read(s, s->units[i])->Id;
// compact clauses
satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i )
satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
{
hTemp = c->Id; c->Id = i + 1;
memmove( veci_begin(&s->clauses) + hTemp, c, sizeof(int)*satset_size(c->nEnts) );
memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*satset_size(c->nEnts) );
}
assert( hHandle == hTemp + satset_size(c->nEnts) );
veci_resize(&s->clauses,hHandle);
veci_resize(&s->learnts,hHandle);
s->stats.learnts = veci_size(&s->learnt_live);
// compact proof (compacts 'proofs' and update 'claProofs')
if ( s->fProofLogging )
Sat_ProofReduce( s );
TimeTotal += clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
// reverses to the previously bookmarked point
void sat_solver2_rollback( sat_solver2* s )
{
int i, k, j;
assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->clauses) );
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
veci_resize(&s->order, 0);
if ( s->hClausePivot > 1 || s->hLearntPivot > 1 )
{
// update order
for ( i = 0; i < s->iVarPivot; i++ )
{
if ( var_value(s, i) != varX )
continue;
s->orderpos[i] = veci_size(&s->order);
veci_push(&s->order,i);
order_update(s, i);
}
// compact watches
for ( i = 0; i < s->size*2; i++ )
{
cla* pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( clause_is_used(s, pArray[k]) )
pArray[j++] = pArray[k];
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;
}
// reset
if ( s->hLearntPivot < veci_size(&s->learnts) )
{
satset* first = satset_read(&s->learnts, s->hLearntPivot);
veci_resize(&s->claActs, first->Id);
if ( s->fProofLogging ) {
veci_resize(&s->claProofs, first->Id);
Sat_ProofReduce( s );
}
}
veci_resize(&s->clauses, s->hClausePivot);
veci_resize(&s->learnts, s->hLearntPivot);
for ( i = s->iVarPivot; i < s->size*2; i++ )
s->wlists[i].size = 0;
s->size = s->iVarPivot;
// initialize other vars
if ( s->size == 0 )
{
// s->size = 0;
// s->cap = 0;
s->qhead = 0;
s->qtail = 0;
#ifdef USE_FLOAT_ACTIVITY
s->var_inc = 1;
s->cla_inc = 1;
s->var_decay = (float)(1 / 0.95 );
s->cla_decay = (float)(1 / 0.999 );
#else
s->var_inc = (1 << 5);
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;
s->stats.starts = 0;
s->stats.decisions = 0;
s->stats.propagations = 0;
s->stats.inspects = 0;
s->stats.conflicts = 0;
s->stats.clauses = 0;
s->stats.clauses_literals = 0;
s->stats.learnts = 0;
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
}
}
int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
{
int restart_iter = 0;
......
src/sat/bsat/satSolver2.h
......@@ -46,6 +46,7 @@ extern void sat_solver2_delete(sat_solver2* s);
extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
extern int sat_solver2_simplify(sat_solver2* s);
extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
extern void sat_solver2_rollback(sat_solver2* s);
extern void sat_solver2_setnvars(sat_solver2* s,int n);
......@@ -112,9 +113,12 @@ struct sat_solver2_t
// clauses
veci clauses; // clause memory
veci learnts; // learnt memory
veci* wlists; // watcher lists (for each literal)
int hLearntFirst; // the first learnt clause
int hClausePivot; // the pivot among problem clause
int hLearntPivot; // the pivot among learned clause
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int iVarPivot; // the pivot among the variables
veci claActs; // clause activities
veci claProofs; // clause proofs
......@@ -245,6 +249,13 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
return fNotUseRandomOld;
}
static inline int sat_solver2_bookmark(sat_solver2* s)
{
s->hLearntPivot = veci_size(&s->learnts);
s->hClausePivot = veci_size(&s->clauses);
s->iVarPivot = s->size;
}
ABC_NAMESPACE_HEADER_END
#endif
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