summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-12-22 15:38:06 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2011-12-22 15:38:06 -0800
commit844c385e2b8610ec8bdc4a55400f8efe79eac119 (patch)
treef154bf6fa36ece55c10e849bf05f5ee73669cc7e
parent1c51d9577df1ade3b7a8ce9cc2117ea4e938e144 (diff)
downloadabc-844c385e2b8610ec8bdc4a55400f8efe79eac119.tar.gz
abc-844c385e2b8610ec8bdc4a55400f8efe79eac119.tar.bz2
abc-844c385e2b8610ec8bdc4a55400f8efe79eac119.zip
Transforming the solver to use different clause representation.
-rw-r--r--src/aig/fra/fraCec.c2
-rw-r--r--src/sat/bsat/satSolver.c286
2 files changed, 144 insertions, 144 deletions
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 6e655590..38bf73d9 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
}
// free the sat_solver
- if ( fVerbose )
+// if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
//sat_solver_store_write( pSat, "trace.cnf" );
//sat_solver_store_free( pSat );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 32adeb7c..4d851d0f 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -39,7 +39,7 @@ ABC_NAMESPACE_IMPL_START
// For derivation output (verbosity level 2)
#define L_IND "%-*d"
-#define L_ind sat_solver_dlevel(s)*2+2,sat_solver_dlevel(s)
+#define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s)
#define L_LIT "%sx%d"
#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
@@ -103,15 +103,15 @@ static inline void clause_print (clause* c) {
//=================================================================================================
// Encode literals in clause pointers:
-static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
+static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); }
static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); }
//=================================================================================================
// Simple helpers:
-static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); }
-static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
+static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
//=================================================================================================
// Variable order functions:
@@ -319,7 +319,7 @@ static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >
/* pre: size > 1 && no variable occurs twice
*/
-static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
+static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int size;
clause* c;
@@ -370,55 +370,10 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
}
-static void clause_remove(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- assert(lit_neg(lits[0]) < s->size*2);
- assert(lit_neg(lits[1]) < s->size*2);
-
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
-
- assert(lits[0] < s->size*2);
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
-
- if (clause_learnt(c)){
- s->stats.learnts--;
- s->stats.learnts_literals -= clause_size(c);
- }else{
- s->stats.clauses--;
- s->stats.clauses_literals -= clause_size(c);
- }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- ABC_FREE(c);
-#else
- Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
-}
-
-
-static lbool clause_simplify(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- lbool* values = s->assigns;
- int i;
-
- assert(sat_solver_dlevel(s) == 0);
-
- for (i = 0; i < clause_size(c); i++){
- lbool sig = !lit_sign(lits[i]); sig += sig - 1;
- if (values[lit_var(lits[i])] == sig)
- return l_True;
- }
- return l_False;
-}
-
//=================================================================================================
// Minor (solver) functions:
-static inline int enqueue(sat_solver* s, lit l, clause* from)
+static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
{
lbool* values = s->assigns;
int v = lit_var(l);
@@ -439,7 +394,7 @@ static inline int enqueue(sat_solver* s, lit l, clause* from)
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
#endif
values [v] = sig;
- levels [v] = sat_solver_dlevel(s);
+ levels [v] = sat_solver_dl(s);
reasons[v] = from;
s->trail[s->qtail++] = l;
@@ -449,7 +404,7 @@ static inline int enqueue(sat_solver* s, lit l, clause* from)
}
-static inline int assume(sat_solver* s, lit l){
+static inline int sat_solver_assume(sat_solver* s, lit l){
assert(s->qtail == s->qhead);
assert(s->assigns[lit_var(l)] == l_Undef);
#ifdef VERBOSEDEBUG
@@ -457,7 +412,7 @@ static inline int assume(sat_solver* s, lit l){
printf( "act = %.20f\n", s->activity[lit_var(l)] );
#endif
veci_push(&s->trail_lim,s->qtail);
- return enqueue(s,l,(clause*)0);
+ return sat_solver_enqueue(s,l,(clause*)0);
}
@@ -469,7 +424,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
int lastLev;
int c;
- if (sat_solver_dlevel(s) <= level)
+ if (sat_solver_dl(s) <= level)
return;
trail = s->trail;
@@ -503,8 +458,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
- clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
- enqueue(s,*begin,c);
+ clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
+ sat_solver_enqueue(s,*begin,c);
///////////////////////////////////
// add clause to internal storage
@@ -740,7 +695,7 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dlevel(s))
+ if (levels[lit_var(q)] == sat_solver_dl(s))
cnt++;
else
veci_push(learnt,q);
@@ -759,7 +714,7 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
tags[lit_var(q)] = l_True;
veci_push(&s->tagged,lit_var(q));
act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dlevel(s))
+ if (levels[lit_var(q)] == sat_solver_dl(s))
cnt++;
else
veci_push(learnt,q);
@@ -864,7 +819,7 @@ clause* sat_solver_propagate(sat_solver* s)
}
*j++ = *i;
- if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+ if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
@@ -904,7 +859,7 @@ clause* sat_solver_propagate(sat_solver* s)
*j++ = *i;
// Clause is unit under assignment:
- if (!enqueue(s,lits[0], *i)){
+ if (!sat_solver_enqueue(s,lits[0], *i)){
confl = *i++;
// Copy the remaining watches:
while (i < end)
@@ -923,37 +878,6 @@ clause* sat_solver_propagate(sat_solver* s)
return confl;
}
-static int clause_cmp (const void* x, const void* y) {
- return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
-void sat_solver_reducedb(sat_solver* s)
-{
- int i, j;
- double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
- clause** learnts = (clause**)vecp_begin(&s->learnts);
- clause** reasons = s->reasons;
-
- sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
-
- for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
- for (; i < vecp_size(&s->learnts); i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
-
- //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
- vecp_resize(&s->learnts,j);
-}
-
//=================================================================================================
// External solver functions:
@@ -1182,6 +1106,118 @@ void sat_solver_rollback( sat_solver* s )
}
+static void clause_remove(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ assert(lit_neg(lits[0]) < s->size*2);
+ assert(lit_neg(lits[1]) < s->size*2);
+
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+ assert(lits[0] < s->size*2);
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+ if (clause_learnt(c)){
+ s->stats.learnts--;
+ s->stats.learnts_literals -= clause_size(c);
+ }else{
+ s->stats.clauses--;
+ s->stats.clauses_literals -= clause_size(c);
+ }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ ABC_FREE(c);
+#else
+ Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+}
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ lbool* values = s->assigns;
+ int i;
+
+ assert(sat_solver_dl(s) == 0);
+
+ for (i = 0; i < clause_size(c); i++){
+ lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+ if (values[lit_var(lits[i])] == sig)
+ return l_True;
+ }
+ return l_False;
+}
+
+int sat_solver_simplify(sat_solver* s)
+{
+ clause** reasons;
+ int type;
+
+ assert(sat_solver_dl(s) == 0);
+
+ if (sat_solver_propagate(s) != 0)
+ return false;
+
+ if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+ return true;
+
+ reasons = s->reasons;
+ for (type = 0; type < 2; type++){
+ vecp* cs = type ? &s->learnts : &s->clauses;
+ clause** cls = (clause**)vecp_begin(cs);
+
+ int i, j;
+ for (j = i = 0; i < vecp_size(cs); i++){
+ if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+ clause_simplify(s,cls[i]) == l_True)
+ clause_remove(s,cls[i]);
+ else
+ cls[j++] = cls[i];
+ }
+ vecp_resize(cs,j);
+ }
+
+ 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;
+}
+
+
+static int clause_cmp (const void* x, const void* y) {
+ return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void sat_solver_reducedb(sat_solver* s)
+{
+ int i, j;
+ double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+ clause** learnts = (clause**)vecp_begin(&s->learnts);
+ clause** reasons = s->reasons;
+
+ sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+ for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+ for (; i < vecp_size(&s->learnts); i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+
+ //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+ vecp_resize(&s->learnts,j);
+}
+
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
clause * c;
@@ -1240,10 +1276,10 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
return false;
if (j - begin == 1) // unit clause
- return enqueue(s,*begin,(clause*)0);
+ return sat_solver_enqueue(s,*begin,(clause*)0);
// create new clause
- c = clause_new(s,begin,j,0);
+ c = clause_create_new(s,begin,j,0);
if ( c )
vecp_push(&s->clauses,c);
@@ -1255,42 +1291,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
}
-int sat_solver_simplify(sat_solver* s)
-{
- clause** reasons;
- int type;
-
- assert(sat_solver_dlevel(s) == 0);
-
- if (sat_solver_propagate(s) != 0)
- return false;
-
- if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
- return true;
-
- reasons = s->reasons;
- for (type = 0; type < 2; type++){
- vecp* cs = type ? &s->learnts : &s->clauses;
- clause** cls = (clause**)vecp_begin(cs);
-
- int i, j;
- for (j = i = 0; i < vecp_size(cs); i++){
- if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
- clause_simplify(s,cls[i]) == l_True)
- clause_remove(s,cls[i]);
- else
- cls[j++] = cls[i];
- }
- vecp_resize(cs,j);
- }
-
- 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 luby(double y, int x)
{
int size, seq;
@@ -1322,7 +1322,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
veci learnt_clause;
int i;
- assert(s->root_level == sat_solver_dlevel(s));
+ assert(s->root_level == sat_solver_dl(s));
s->nRestarts++;
s->stats.starts++;
@@ -1352,7 +1352,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
printf(L_IND"**CONFLICT**\n", L_ind);
#endif
s->stats.conflicts++; conflictC++;
- if (sat_solver_dlevel(s) == s->root_level){
+ if (sat_solver_dl(s) == s->root_level){
#ifdef SAT_USE_ANALYZE_FINAL
sat_solver_analyze_final(s, confl, 0);
#endif
@@ -1376,7 +1376,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
}else{
// NO CONFLICT
int next;
-
+
if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
// Reached bound on number of conflicts:
s->progress_estimate = sat_solver_progress(s);
@@ -1395,13 +1395,13 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
return l_Undef;
}
- if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
+ if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
// Simplify the set of problem clauses:
sat_solver_simplify(s);
- if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
- sat_solver_reducedb(s);
+// sat_solver_reducedb(s);
// New variable decision:
s->stats.decisions++;
@@ -1429,9 +1429,9 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
}
if ( s->polarity[next] ) // positive polarity
- assume(s,toLit(next));
+ sat_solver_assume(s,toLit(next));
else
- assume(s,lit_neg(toLit(next)));
+ sat_solver_assume(s,lit_neg(toLit(next)));
}
}
@@ -1482,7 +1482,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
case 1: // l_True:
break;
case 0: // l_Undef
- assume(s, *i);
+ sat_solver_assume(s, *i);
if (sat_solver_propagate(s) == NULL)
break;
// fallthrough
@@ -1491,7 +1491,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
return l_False;
}
}
- s->root_level = sat_solver_dlevel(s);
+ s->root_level = sat_solver_dl(s);
#endif
@@ -1501,7 +1501,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
for (int i = 0; i < assumps.size(); i++){
Lit p = assumps[i];
assert(var(p) < nVars());
- if (!assume(p)){
+ if (!sat_solver_assume(p)){
GClause r = reason[var(p)];
if (r != GClause_NULL){
Clause* confl;
@@ -1535,7 +1535,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
lit p = *i;
assert(lit_var(p) < s->size);
veci_push(&s->trail_lim,s->qtail);
- if (!enqueue(s,p,(clause*)0))
+ if (!sat_solver_enqueue(s,p,(clause*)0))
{
clause * r = s->reasons[lit_var(p)];
if (r != NULL)
@@ -1573,7 +1573,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
return l_False; }
}
}
- assert(s->root_level == sat_solver_dlevel(s));
+ assert(s->root_level == sat_solver_dl(s));
#endif
s->nCalls2++;