Skip to content

A
abc
Commit 09d3e1ff by Alan Mishchenko
Options

Proof-logging in the updated solver.

parent a7031bb3
Showing with 483 additions and 218 deletions
src/aig/fra/fraCec.c
......@@ -105,8 +105,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
// simplify the problem
clk = clock();
status = sat_solver2_simplify(pSat);
printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
ABC_PRT( "Time", clock() - clk );
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
// ABC_PRT( "Time", clock() - clk );
if ( status == 0 )
{
Vec_IntFree( vCiIds );
......
src/sat/bsat/satSolver.h
......@@ -113,8 +113,8 @@ extern void * sat_solver_store_release( sat_solver * s );
//=================================================================================================
// Solver representation:
//struct clause_t;
//typedef struct clause_t clause;
struct clause_t;
typedef struct clause_t clause;
struct sat_solver_t
{
......
src/sat/bsat/satSolver2.c
......@@ -38,7 +38,7 @@ ABC_NAMESPACE_IMPL_START
// For derivation output (verbosity level 2)
#define L_IND "%-*d"
#define L_ind sat_solver2_dlevel(s)*3+3,sat_solver2_dlevel(s)
#define L_ind solver2_dlevel(s)*3+3,solver2_dlevel(s)
#define L_LIT "%sx%d"
#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
static void printlits(lit* begin, lit* end)
......@@ -65,6 +65,8 @@ static inline double drand(double* seed) {
static inline int irand(double* seed, int size) {
return (int)(drand(seed) * size); }
static inline int sat_float2int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
static inline float sat_int2float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
//=================================================================================================
// Predeclarations:
......@@ -80,46 +82,88 @@ static const int varX = 3;
struct varinfo_t
{
unsigned val : 2;
unsigned pol : 1;
unsigned mark : 1;
unsigned tag : 3;
unsigned lev : 25;
unsigned val : 2; // variable value
unsigned pol : 1; // last polarity
unsigned tag : 3; // conflict analysis tags
unsigned lev : 26; // variable level
};
static inline int var_value (sat_solver2 * s, int v) { return s->vi[v].val; }
static inline int var_polar (sat_solver2 * s, int v) { return s->vi[v].pol; }
static inline int var_tag (sat_solver2 * s, int v) { return s->vi[v].tag; }
static inline int var_mark (sat_solver2 * s, int v) { return s->vi[v].mark; }
static inline int var_level (sat_solver2 * s, int v) { return s->vi[v].lev; }
static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; }
static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; }
static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; }
static inline void var_set_value (sat_solver2* s, int v, int val ) { s->vi[v].val = val; }
static inline void var_set_polar (sat_solver2* s, int v, int pol ) { s->vi[v].pol = pol; }
static inline void var_set_level (sat_solver2* s, int v, int lev ) { s->vi[v].lev = lev; }
// variable tags
static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; }
static inline void var_set_tag (sat_solver2* s, int v, int tag) {
assert( tag > 0 && tag < 16 );
if ( s->vi[v].tag == 0 )
veci_push( &s->tagged, v );
s->vi[v].tag = tag;
}
static inline void var_add_tag (sat_solver2* s, int v, int tag) {
assert( tag > 0 && tag < 16 );
if ( s->vi[v].tag == 0 )
veci_push( &s->tagged, v );
s->vi[v].tag |= tag;
}
static inline void solver2_clear_tags(sat_solver2* s, int start) {
int i, * tagged = veci_begin(&s->tagged);
for (i = start; i < veci_size(&s->tagged); i++)
s->vi[tagged[i]].tag = 0;
veci_resize(&s->tagged,start);
}
static inline void var_set_value (sat_solver2 * s, int v, int val ) { s->vi[v].val = val; }
static inline void var_set_polar (sat_solver2 * s, int v, int pol ) { s->vi[v].pol = pol; }
static inline void var_set_tag (sat_solver2 * s, int v, int tag ) { s->vi[v].tag = tag; }
static inline void var_set_mark (sat_solver2 * s, int v, int mark) { s->vi[v].mark = mark; }
static inline void var_set_level (sat_solver2 * s, int v, int lev ) { s->vi[v].lev = lev; }
// level marks
static inline int var_lev_mark (sat_solver2* s, int v) {
return (veci_begin(&s->trail_lim)[var_level(s,v)] & 0x80000000) > 0;
}
static inline void var_lev_set_mark (sat_solver2* s, int v) {
int level = var_level(s,v);
assert( level < veci_size(&s->trail_lim) );
veci_begin(&s->trail_lim)[level] |= 0x80000000;
veci_push(&s->mark_levels, level);
}
static inline void solver2_clear_marks(sat_solver2* s) {
int i, * mark_levels = veci_begin(&s->mark_levels);
for (i = 0; i < veci_size(&s->mark_levels); i++)
veci_begin(&s->trail_lim)[mark_levels[i]] &= 0x7FFFFFFF;
veci_resize(&s->mark_levels,0);
}
// other inlines
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v]; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)]; }
static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
//=================================================================================================
// Clause datatype + minor functions:
struct clause_t // should have even number of entries!
typedef struct satset_t satset;
struct satset_t // should have even number of entries!
{
unsigned learnt : 1;
unsigned fMark : 1;
unsigned fPartA : 1;
unsigned fRefed : 1;
unsigned nLits : 28;
unsigned mark : 1;
unsigned partA : 1;
unsigned nLits : 29;
int Id;
lit lits[0];
lit pLits[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 lit* clause_begin (satset* c) { return c->pLits; }
static inline int clause_learnt (satset* c) { return c->learnt; }
static inline int clause_nlits (satset* c) { return c->nLits; }
static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits + (nLits & 1); }
static inline clause* get_clause (sat_solver2* s, int c) { return (clause *)(s->pMemArray + c); }
static inline cla clause_id (sat_solver2* s, clause* c) { return (cla)((int *)c - s->pMemArray); }
static inline satset* get_clause (sat_solver2* s, int c) { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL; }
static inline cla clause_id (sat_solver2* s, satset* c) { return (cla)((int *)c - veci_begin(&s->clauses)); }
static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL; }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; }
#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) )
......@@ -127,17 +171,55 @@ static inline cla clause_id (sat_solver2* s, clause* c) { return (cla)(
for ( i = s->iLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
//=================================================================================================
// Proof logging:
static inline void proof_chain_start( sat_solver2* s, satset* c )
{
if ( s->fProofLogging )
{
s->iStartChain = veci_size(&s->proof_clas);
veci_push(&s->proof_clas, 0);
veci_push(&s->proof_clas, 0);
veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 );
veci_push(&s->proof_vars, 0);
veci_push(&s->proof_vars, 0);
veci_push(&s->proof_vars, 0);
}
}
static inline void proof_chain_resolve( sat_solver2* s, satset* c, int Var )
{
if ( s->fProofLogging && c )
{
veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 );
veci_push(&s->proof_vars, Var);
}
}
static inline void proof_chain_stop( sat_solver2* s )
{
if ( s->fProofLogging )
{
satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain);
assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) );
c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2;
s->iStartChain = 0;
// printf( "%d ", c->nLits );
}
}
//=================================================================================================
// Simple helpers:
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]; }
static inline int solver2_dlevel(sat_solver2* s) { return veci_size(&s->trail_lim); }
static inline veci* solver2_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;
satset* c;
int i, Cid, nLits = end - begin;
assert(nLits > 1);
assert(begin[0] >= 0);
......@@ -145,44 +227,43 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
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 )
if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap )
{
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 );
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;
s->clauses.size = Abc_MaxInt( veci_size(&s->clauses), 2 );
}
// create clause
c = (clause*)(s->pMemArray + s->nMemSize);
c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
c->learnt = learnt;
c->nLits = nLits;
for (i = 0; i < nLits; i++)
c->lits[i] = begin[i];
c->pLits[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);
//veci_push(&s->claProof, 0);
}
else
{
c->Id = -(s->stats.clauses + 1);
}
c->Id = s->stats.clauses + 1;
// extend storage
Cid = s->nMemSize;
s->nMemSize += clause_size(nLits);
if ( s->nMemSize > s->nMemAlloc )
Cid = veci_size(&s->clauses);
s->clauses.size += clause_size(nLits);
if ( veci_size(&s->clauses) > s->clauses.cap )
printf( "Out of memory!!!\n" );
assert( s->nMemSize <= s->nMemAlloc );
assert( veci_size(&s->clauses) <= s->clauses.cap );
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));
veci_push(solver2_wlist(s,lit_neg(begin[0])),clause_id(s,c));
veci_push(solver2_wlist(s,lit_neg(begin[1])),clause_id(s,c));
// remember the last one and first learnt
s->iLast = Cid;
......@@ -284,56 +365,85 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select
//=================================================================================================
// Activity functions:
static inline void act_var_rescale(sat_solver2* s) {
unsigned* activity = s->activity;
int i, clk = clock();
static int Total = 0;
#ifdef USE_FLOAT_ACTIVITY
static inline void act_var_rescale(sat_solver2* s) {
double* activity = s->activity;
int i;
for (i = 0; i < s->size; i++)
activity[i] >>= 19;
s->var_inc >>= 19;
// assert( s->var_inc > 15 );
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 );
activity[i] *= 1e-100;
s->var_inc *= 1e-100;
}
static inline void act_clause_rescale(sat_solver2* s) {
static int Total = 0;
float * claActs = (float *)veci_begin(&s->claActs);
int i, clk = clock();
for (i = 0; i < veci_size(&s->claActs); i++)
claActs[i] *= (float)1e-20;
s->cla_inc *= (float)1e-20;
printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
Total += clock() - clk;
Abc_PrintTime( 1, "Time", Total );
}
static inline void act_var_bump(sat_solver2* s, int v) {
static int Counter = 0;
s->activity[v] += s->var_inc;
if (s->activity[v] & 0x80000000)
if (s->activity[v] > 1e100)
act_var_rescale(s);
if (s->orderpos[v] != -1)
order_update(s,v);
}
static inline void act_clause_bump(sat_solver2* s, satset*c) {
float * claActs = (float *)veci_begin(&s->claActs);
assert( c->Id < veci_size(&s->claActs) );
claActs[c->Id] += s->cla_inc;
if (claActs[c->Id] > (float)1e20)
act_clause_rescale(s);
}
static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
//static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
#else
static inline void act_var_rescale(sat_solver2* s) {
unsigned* activity = s->activity;
int i;
for (i = 0; i < s->size; i++)
activity[i] >>= 19;
s->var_inc >>= 19;
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause_rescale(sat_solver2* s) {
static int Total = 0;
int i, clk = clock();
unsigned * tagged = (unsigned *)veci_begin(&s->claActs);
unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
for (i = 1; i < veci_size(&s->claActs); i++)
tagged[i] >>= 14;
claActs[i] >>= 14;
s->cla_inc >>= 14;
// assert( s->cla_inc > (1<<10)-1 );
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
Total += clock() - clk;
Abc_PrintTime( 1, "Time", Total );
}
static inline void act_clause_bump(sat_solver2* s, clause *c) {
static inline void act_var_bump(sat_solver2* s, int v) {
s->activity[v] += s->var_inc;
if (s->activity[v] & 0x80000000)
act_var_rescale(s);
if (s->orderpos[v] != -1)
order_update(s,v);
}
static inline void act_clause_bump(sat_solver2* s, satset*c) {
unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
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)
claActs[c->Id] += s->cla_inc;
if (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_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
#endif
//=================================================================================================
// Minor (solver) functions:
......@@ -352,7 +462,7 @@ static inline int enqueue(sat_solver2* s, lit l, int from)
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
#endif
var_set_value( s, v, lit_sign(l) );
var_set_level( s, v, sat_solver2_dlevel(s) );
var_set_level( s, v, solver2_dlevel(s) );
s->reasons[v] = from;
s->trail[s->qtail++] = l;
order_assigned(s, v);
......@@ -377,7 +487,7 @@ static void sat_solver2_canceluntil(sat_solver2* s, int level) {
int lastLev;
int c, x;
if (sat_solver2_dlevel(s) <= level)
if (solver2_dlevel(s) <= level)
return;
trail = s->trail;
......@@ -440,7 +550,7 @@ static double sat_solver2_progress(sat_solver2* s)
| stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/
/*
void Solver::analyzeFinal(Clause* confl, bool skip_first)
void Solver::analyzeFinal(satset* confl, bool skip_first)
{
// -- NOTE! This code is relatively untested. Please report bugs!
conflict.clear();
......@@ -481,102 +591,166 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first)
#ifdef SAT_USE_ANALYZE_FINAL
static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
static void sat_solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
{
int* tagged;
int i, j, start;
int i, j, start, x;
veci_resize(&s->conf_final,0);
if ( s->root_level == 0 )
return;
assert( veci_size(&s->tagged) == 0 );
for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
{
int x = lit_var(clause_begin(conf)[i]);
x = lit_var(clause_begin(conf)[i]);
if ( var_level(s,x) )
{
var_set_tag(s, x, 1);
veci_push(&s->tagged,x);
}
}
start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
int x = lit_var(s->trail[i]);
if (s->vi[x].tag == 1){
if (s->reasons[x] == 0){
assert( var_level(s,x) );
veci_push(&s->conf_final,lit_neg(s->trail[i]));
}else{
clause* c = get_clause(s, s->reasons[x]);
x = lit_var(s->trail[i]);
if (var_tag(s,x)){
satset* c = get_clause(s, var_reason(s,x));
if (c){
int* lits = clause_begin(c);
for (j = 1; j < clause_nlits(c); j++)
if ( var_level(s,lit_var(lits[j])) )
{
var_set_tag(s, lit_var(lits[j]), 1);
veci_push(&s->tagged,lit_var(lits[j]));
}
}else {
assert( var_level(s,x) );
veci_push(&s->conf_final,lit_neg(s->trail[i]));
}
}
}
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);
solver2_clear_tags(s,0);
}
#endif
static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl)
static int sat_solver2_lit_removable_rec(sat_solver2* s, int v)
{
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);
// tag[0]: True if original conflict clause literal.
// tag[1]: Processed by this procedure
// tag[2]: 0=non-removable, 1=removable
satset* c;
int i, x;
// skip visited
if (var_tag(s,v) & 2)
return (var_tag(s,v) & 4) > 0;
// skip decisions on a wrong level
c = get_clause(s, var_reason(s,v));
if ( c == NULL ){
var_add_tag(s,v,2);
return 0;
}
for ( i = 1; i < (int)c->nLits; i++ ){
x = lit_var(c->pLits[i]);
if (var_tag(s,x) & 1)
sat_solver2_lit_removable_rec(s, x);
else{
if (var_level(s,x) == 0 || var_tag(s,x) == 6) continue; // -- 'x' checked before, found to be removable (or belongs to the toplevel)
if (var_tag(s,x) == 2 || !var_lev_mark(s,x) || !sat_solver2_lit_removable_rec(s, x))
{ // -- 'x' checked before, found NOT to be removable, or it belongs to a wrong level, or cannot be removed
var_add_tag(s,v,2);
return 0;
}
}
}
// if (pfl && visit[p0] & 1){
// result.push(p0); }
var_add_tag(s,v,6);
return 1;
}
static int sat_solver2_lit_removable(sat_solver2* s, int x)
{
satset* c;
int i, top;
if ( !var_reason(s,x) )
return 0;
if ( var_tag(s,x) & 2 )
{
assert( var_tag(s,x) & 1 );
return 1;
}
top = veci_size(&s->tagged);
veci_resize(&s->stack,0);
veci_push(&s->stack,lit_var(l));
while (veci_size(&s->stack) > 0)
veci_push(&s->stack, x << 1);
while (veci_size(&s->stack))
{
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;
}
x = veci_pop(&s->stack);
if ( s->fProofLogging ){
if ( x & 1 ){
if ( var_tag(s,x >> 1) & 1 )
veci_push(&s->min_lit_order, x >> 1 );
continue;
}
veci_push(&s->stack, x ^ 1 );
}
x >>= 1;
c = get_clause(s, var_reason(s,x));
for (i = 1; i < (int)c->nLits; i++){
x = lit_var(c->pLits[i]);
if (var_tag(s,x) || !var_level(s,x))
continue;
if (!var_reason(s,x) || !var_lev_mark(s,x)){
solver2_clear_tags(s, top);
return 0;
}
veci_push(&s->stack, x << 1);
var_set_tag(s, x, 2);
}
}
return true;
return 1;
}
static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
static void sat_solver2_logging_order(sat_solver2* s, int x)
{
lit* trail = s->trail;
int cnt = 0;
lit p = lit_Undef;
int ind = s->qtail-1;
lit* lits;
int i, j, minl;
int* tagged;
assert( veci_size(&s->tagged) == 0 );
satset* c;
int i;
if ( (var_tag(s,x) & 4) )
return;
var_add_tag(s, x, 4);
veci_resize(&s->stack,0);
veci_push(&s->stack,x << 1);
while (veci_size(&s->stack))
{
x = veci_pop(&s->stack);
if ( x & 1 ){
veci_push(&s->min_step_order, x >> 1 );
continue;
}
veci_push(&s->stack, x ^ 1 );
x >>= 1;
c = get_clause(s, var_reason(s,x));
// if ( !c )
// printf( "sat_solver2_logging_order(): Error in conflict analysis!!!\n" );
for (i = 1; i < (int)c->nLits; i++){
x = lit_var(c->pLits[i]);
if ( !var_level(s,x) || (var_tag(s,x) & 1) )
continue;
veci_push(&s->stack, x << 1);
var_add_tag(s, x, 4);
}
}
}
static void sat_solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
{
int cnt = 0;
lit p = lit_Undef;
int x, ind = s->qtail-1;
lit* lits,* vars, i, j, k;
assert( veci_size(&s->tagged) == 0 );
// tag[0] - visited by conflict analysis (afterwards: literals of the learned clause)
// tag[1] - visited by sat_solver2_lit_removable() with success
// tag[2] - visited by sat_solver2_logging_order()
/*
proof_chain_start( s, c );
veci_push(learnt,lit_Undef);
do{
assert(c != 0);
if (clause_learnt(c))
......@@ -588,46 +762,107 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
assert(lit_var(q) >= 0 && lit_var(q) < s->size);
if (!var_tag(s, lit_var(q)) && var_level(s,lit_var(q))){
var_set_tag(s, lit_var(q), 1);
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
if (var_level(s,lit_var(q)) == sat_solver2_dlevel(s))
if (var_level(s,lit_var(q)) == solver2_dlevel(s))
cnt++;
else
veci_push(learnt,q);
}
}
while (!var_tag(s, lit_var(trail[ind--])));
while (!var_tag(s, lit_var(s->trail[ind--])));
p = trail[ind+1];
c = get_clause(s, s->reasons[lit_var(p)]);
p = s->trail[ind+1];
c = get_clause(s, lit_reason(s,p));
cnt--;
}while (cnt > 0);
*veci_begin(learnt) = lit_neg(p);
*/
proof_chain_start( s, c );
veci_push(learnt,lit_Undef);
while ( 1 ){
assert(c != 0);
if (clause_learnt(c))
act_clause_bump(s,c);
for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){
x = lit_var(c->pLits[j]);
assert(x >= 0 && x < s->size);
if ( var_tag(s, x) )
continue;
if ( var_level(s,x) == 0 )
{
proof_chain_resolve( s, var_unit_clause(s, x), x );
continue;
}
var_set_tag(s, x, 1);
act_var_bump(s,x);
if (var_level(s,x) == solver2_dlevel(s))
cnt++;
else
veci_push(learnt,c->pLits[j]);
}
while (!var_tag(s, lit_var(s->trail[ind--])));
p = s->trail[ind+1];
c = get_clause(s, lit_reason(s,p));
cnt--;
if ( cnt == 0 )
break;
proof_chain_resolve( s, c, lit_var(p) );
}
*veci_begin(learnt) = lit_neg(p);
// mark levels
assert( veci_size(&s->mark_levels) == 0 );
lits = veci_begin(learnt);
minl = 0;
for (i = 1; i < veci_size(learnt); i++)
minl |= 1 << (var_level(s,lit_var(lits[i])) & 31);
var_lev_set_mark(s, lit_var(lits[i]));
// simplify (full)
veci_resize(&s->min_lit_order, 0);
for (i = j = 1; i < veci_size(learnt); i++){
if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver2_lit_removable(s,lits[i],minl))
// if (!sat_solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
if (!sat_solver2_lit_removable( s,lit_var(lits[i])) )
lits[j++] = lits[i];
}
// record the proof
if ( s->fProofLogging )
{
// collect additional clauses to resolve
veci_resize(&s->min_step_order, 0);
vars = veci_begin(&s->min_lit_order);
for (i = 0; i < veci_size(&s->min_lit_order); i++)
sat_solver2_logging_order( s, vars[i] );
// add them in the reverse order
vars = veci_begin(&s->min_step_order);
for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
c = get_clause(s, var_reason(s,vars[i]));
proof_chain_resolve( s, c, vars[i] );
for ( k = 1; k < (int)c->nLits; k++ )
{
x = lit_var(c->pLits[k]);
if ( var_level(s,x) == 0 )
proof_chain_resolve( s, var_unit_clause(s, x), x );
}
}
proof_chain_stop( s );
}
// unmark levels
solver2_clear_marks( s );
// update size of learnt + statistics
s->stats.max_literals += veci_size(learnt);
veci_resize(learnt,j);
s->stats.tot_literals += j;
// clear tags
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);
solver2_clear_tags(s,0);
#ifdef DEBUG
for (i = 0; i < s->size; i++)
......@@ -660,16 +895,16 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
#endif
}
clause* sat_solver2_propagate(sat_solver2* s)
satset* sat_solver2_propagate(sat_solver2* s)
{
clause * c, * confl = NULL;
satset* c, * confl = NULL;
veci* ws;
lit* lits, false_lit, p, * stop, * k;
cla* begin,* end, *i, *j;
while (confl == 0 && s->qtail - s->qhead > 0){
p = s->trail[s->qhead++];
ws = sat_solver2_read_wlist(s,p);
ws = solver2_wlist(s,p);
begin = (cla*)veci_begin(ws);
end = begin + veci_size(ws);
......@@ -703,7 +938,7 @@ clause* sat_solver2_propagate(sat_solver2* s)
if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
lits[1] = *k;
*k = false_lit;
veci_push(sat_solver2_read_wlist(s,lit_neg(lits[1])),*i);
veci_push(solver2_wlist(s,lit_neg(lits[1])),*i);
goto next; }
}
......@@ -729,14 +964,14 @@ next: i++;
static void clause_remove(sat_solver2* s, clause* c)
static void clause_remove(sat_solver2* s, satset* 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));
veci_remove(solver2_wlist(s,lit_neg(lits[0])),clause_id(s,c));
veci_remove(solver2_wlist(s,lit_neg(lits[1])),clause_id(s,c));
if (clause_learnt(c)){
s->stats.learnts--;
......@@ -748,11 +983,11 @@ static void clause_remove(sat_solver2* s, clause* c)
}
static lbool clause_simplify(sat_solver2* s, clause* c)
static lbool clause_simplify(sat_solver2* s, satset* c)
{
lit* lits = clause_begin(c);
int i;
assert(sat_solver2_dlevel(s) == 0);
assert(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;
......@@ -764,7 +999,7 @@ int sat_solver2_simplify(sat_solver2* s)
{
// int type;
int Counter = 0;
assert(sat_solver2_dlevel(s) == 0);
assert(solver2_dlevel(s) == 0);
if (sat_solver2_propagate(s) != 0)
return false;
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
......@@ -775,8 +1010,8 @@ int sat_solver2_simplify(sat_solver2* s)
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] &&
satset* c = get_clause(s,cls[i]);
if (lit_reason(s,*clause_begin(c)) != cls[i] &&
clause_simplify(s,c) == l_True)
clause_remove(s,c), Counter++;
else
......@@ -794,7 +1029,8 @@ int sat_solver2_simplify(sat_solver2* s)
void sat_solver2_reducedb(sat_solver2* s)
{
clause * c;
/*
satset* c;
cla Cid;
int clk = clock();
......@@ -814,10 +1050,10 @@ void sat_solver2_reducedb(sat_solver2* s)
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->mark = 0;
if ( clause_nlits(c) > 2 && lit_reason(s,*clause_begin(c)) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
{
c->fMark = 1;
c->mark = 1;
Counter++;
}
k++;
......@@ -826,28 +1062,25 @@ printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d ", Counter
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)
{
double var_decay = 0.95;
double clause_decay = 0.999;
double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
// s->var_decay = (float)(1 / var_decay );
// s->cla_decay = (float)(1 / clause_decay);
ABC_INT64_T conflictC = 0;
veci learnt_clause;
assert(s->root_level == sat_solver2_dlevel(s));
assert(s->root_level == solver2_dlevel(s));
s->stats.starts++;
veci_resize(&s->model,0);
veci_new(&learnt_clause);
for (;;){
clause* confl = sat_solver2_propagate(s);
satset* confl = sat_solver2_propagate(s);
if (confl != 0){
// CONFLICT
int blevel;
......@@ -856,7 +1089,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
printf(L_IND"**CONFLICT**\n", L_ind);
#endif
s->stats.conflicts++; conflictC++;
if (sat_solver2_dlevel(s) == s->root_level){
if (solver2_dlevel(s) == s->root_level){
#ifdef SAT_USE_ANALYZE_FINAL
sat_solver2_analyze_final(s, confl, 0);
#endif
......@@ -901,7 +1134,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
return l_Undef;
}
// if (sat_solver2_dlevel(s) == 0 && !s->fSkipSimplify)
// if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
// Simplify the set of problem clauses:
// sat_solver2_simplify(s);
......@@ -951,7 +1184,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 = (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);
......@@ -961,20 +1194,32 @@ 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);
veci_new(&s->mark_levels);
veci_new(&s->min_lit_order);
veci_new(&s->min_step_order);
veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
veci_new(&s->claActs); veci_push(&s->claActs, -1);
veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
// initialize other
s->iLearnt = -1; // the first learnt clause
s->iLast = -1; // the last learnt clause
#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);
s->var_inc = (1 << 5);
#endif
s->random_seed = 91648253;
s->fProofLogging = 1;
return s;
}
void sat_solver2_setnvars(sat_solver2* s,int n)
{
int var;
......@@ -985,10 +1230,14 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
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);
#ifdef USE_FLOAT_ACTIVITY
s->activity = ABC_REALLOC(double, s->activity, s->cap);
#else
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
#endif
}
for (var = s->size; var < n; var++){
......@@ -1008,7 +1257,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
void sat_solver2_delete(sat_solver2* s)
{
ABC_FREE(s->pMemArray);
// report statistics
assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
printf( "Used %6.2f Mb for proof-logging.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20) );
// delete vectors
veci_delete(&s->order);
......@@ -1018,8 +1269,14 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->model);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
veci_delete(&s->mark_levels);
veci_delete(&s->min_lit_order);
veci_delete(&s->min_step_order);
veci_delete(&s->proof_clas);
veci_delete(&s->proof_vars);
veci_delete(&s->claActs);
veci_delete(&s->claProofs);
veci_delete(&s->clauses);
// delete arrays
if (s->vi != 0){
......@@ -1029,10 +1286,10 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->wlists[i]);
ABC_FREE(s->wlists );
ABC_FREE(s->vi );
ABC_FREE(s->activity );
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
ABC_FREE(s->trail );
ABC_FREE(s->activity );
}
ABC_FREE(s);
}
......@@ -1162,7 +1419,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
return l_False;
}
}
s->root_level = sat_solver2_dlevel(s);
s->root_level = solver2_dlevel(s);
#endif
......@@ -1175,7 +1432,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (!assume(p)){
GClause r = reason[var(p)];
if (r != GClause_NULL){
Clause* confl;
satset* confl;
if (r.isLit()){
confl = propagate_tmpbin;
(*confl)[1] = ~p;
......@@ -1189,7 +1446,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
conflict.push(~p);
cancelUntil(0);
return false; }
Clause* confl = propagate();
satset* confl = propagate();
if (confl != NULL){
analyzeFinal(confl), assert(conflict.size() > 0);
cancelUntil(0);
......@@ -1208,10 +1465,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
veci_push(&s->trail_lim,s->qtail);
if (!enqueue(s,p,0))
{
clause * r = get_clause(s, s->reasons[lit_var(p)]);
satset* r = get_clause(s, lit_reason(s,p));
if (r != NULL)
{
clause* confl = r;
satset* confl = r;
sat_solver2_analyze_final(s, confl, 1);
veci_push(&s->conf_final, lit_neg(p));
}
......@@ -1225,7 +1482,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
}
else
{
clause* confl = sat_solver2_propagate(s);
satset* confl = sat_solver2_propagate(s);
if (confl != NULL){
sat_solver2_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0);
......@@ -1233,7 +1490,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
return l_False; }
}
}
assert(s->root_level == sat_solver2_dlevel(s));
assert(s->root_level == solver2_dlevel(s));
#endif
// s->nCalls2++;
......
src/sat/bsat/satSolver2.h
......@@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_HEADER_START
//#define USE_FLOAT_ACTIVITY
//=================================================================================================
// Public interface:
......@@ -70,9 +70,6 @@ extern void * sat_solver2_store_release( sat_solver2 * s );
//=================================================================================================
// Solver representation:
//struct clause_t;
//typedef struct clause_t clause;
struct varinfo_t;
typedef struct varinfo_t varinfo;
......@@ -91,21 +88,26 @@ struct sat_solver2_t
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
int fNotUseRandom; // do not allow random decisions with a fixed probability
// int fSkipSimplify; // set to one to skip simplification of the clause database
int fProofLogging; // enable proof-logging
// clauses
veci clauses; // clause memory
veci* wlists; // watcher lists (for each literal)
int iLearnt; // the first learnt clause
int iLast; // the last learnt clause
veci* wlists; // watcher lists (for each literal)
// clause memory
int * pMemArray;
int nMemAlloc;
int nMemSize;
// activities
#ifdef USE_FLOAT_ACTIVITY
double var_inc; // Amount to bump next variable with.
double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
float cla_inc; // Amount to bump next clause with.
float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
double* activity; // A heuristic measurement of the activity of a variable.
#else
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.
#endif
veci claActs; // clause activities
veci claProofs; // clause proofs
......@@ -123,6 +125,15 @@ struct sat_solver2_t
veci model; // If problem is solved, this vector contains the model (contains: lbool).
veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
// this vector represent the final conflict clause expressed in the assumptions.
veci mark_levels; // temporary storage for labeled levels
veci min_lit_order; // ordering of removable literals
veci min_step_order;// ordering of resolution steps
// proof logging
veci proof_clas; // sequence of proof clauses
veci proof_vars; // sequence of proof variables
int iStartChain; // beginning of the chain
// statistics
stats_t stats;
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
......
src/sat/bsat/satUtil.c
......@@ -169,16 +169,15 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
SeeAlso []
***********************************************************************/
void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p )
void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
{
// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
printf( "starts : %10d\n", (int)p->stats.starts );
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( "inspects2 : %10d\n", (int)p->stats.inspects2 );
printf( "memory : %10d\n", p->nMemSize );
printf( "starts : %10d\n", (int)s->stats.starts );
printf( "conflicts : %10d\n", (int)s->stats.conflicts );
printf( "decisions : %10d\n", (int)s->stats.decisions );
printf( "propagations : %10d\n", (int)s->stats.propagations );
// printf( "inspects : %10d\n", (int)s->stats.inspects );
// printf( "inspects2 : %10d\n", (int)s->stats.inspects2 );
printf( "memory : %10d\n", veci_size(&s->clauses) );
}
/**Function*************************************************************
......
src/sat/bsat/satVec.h
......@@ -44,7 +44,8 @@ static inline void veci_new (veci* v) {
static inline void veci_delete (veci* v) { ABC_FREE(v->ptr); }
static inline int* veci_begin (veci* v) { return v->ptr; }
static inline int veci_size (veci* v) { return v->size; }
static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !!
static inline void veci_resize (veci* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !!
static inline int veci_pop (veci* v) { assert(v->size); return v->ptr[--v->size]; }
static inline void veci_push (veci* v, int e)
{
if (v->size == v->cap) {
......@@ -82,7 +83,7 @@ static inline void vecp_new (vecp* v) {
static inline void vecp_delete (vecp* v) { ABC_FREE(v->ptr); }
static inline void** vecp_begin (vecp* v) { return v->ptr; }
static inline int vecp_size (vecp* v) { return v->size; }
static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !!
static inline void vecp_resize (vecp* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !!
static inline void vecp_push (vecp* v, void* e)
{
if (v->size == v->cap) {
......@@ -143,9 +144,6 @@ struct stats_t
};
typedef struct stats_t stats_t;
struct clause_t;
typedef struct clause_t clause;
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