From 30037e06533b1c7291e32025ebb7c9a2e875e079 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Tue, 14 Feb 2017 14:43:44 -0800 Subject: - Small bug fix in var activity (improve performance) - New implementation of watcher lists. --- src/sat/satoko/solver.c | 14 +++++------- src/sat/satoko/solver.h | 20 +++++------------ src/sat/satoko/solver_api.c | 23 ++++++++----------- src/sat/satoko/watch_list.h | 54 ++++++++++++++++++++++++++++++--------------- 4 files changed, 55 insertions(+), 56 deletions(-) (limited to 'src/sat/satoko') diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 2abc9833..d2bf1b5e 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -114,7 +114,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits) vec_uint_assign(s->stamps, lit2var(lit), s->cur_stamp); counter = 0; - watch_list_foreach(s->bin_watches, w, neg_lit) { + watch_list_foreach_bin(s->watches, w, neg_lit) { unsigned imp_lit = w->blocker; if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp && lit_value(s, imp_lit) == LIT_TRUE) { @@ -400,8 +400,6 @@ static inline void solver_garbage_collect(solver_t *s) struct watcher *w; watch_list_foreach(s->watches, w, i) clause_realloc(new_cdb, s->all_clauses, &(w->cref)); - watch_list_foreach(s->bin_watches, w, i) - clause_realloc(new_cdb, s->all_clauses, &(w->cref)); } for (i = 0; i < vec_uint_size(s->trail); i++) @@ -541,7 +539,7 @@ unsigned solver_propagate(solver_t *s) struct watcher *i, *j; n_propagations++; - watch_list_foreach(s->bin_watches, i, p) { + watch_list_foreach_bin(s->watches, i, p) { if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) continue; if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING) @@ -553,16 +551,14 @@ unsigned solver_propagate(solver_t *s) ws = vec_wl_at(s->watches, p); begin = watch_list_array(ws); end = begin + watch_list_size(ws); - for (i = j = begin; i < end;) { + for (i = j = begin + ws->n_bin; i < end;) { struct clause *clause; struct watcher w; - if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) - { + if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) { *j++ = *i++; continue; } - if (lit_value(s, i->blocker) == LIT_TRUE) { *j++ = *i++; continue; @@ -590,7 +586,7 @@ unsigned solver_propagate(solver_t *s) if (lit_value(s, lits[k]) != LIT_FALSE) { lits[1] = lits[k]; lits[k] = neg_lit; - watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w); + watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w, 0); goto next; } } diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 01912a6e..84c25689 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -49,7 +49,6 @@ struct solver_t_ { vec_uint_t *learnts; vec_uint_t *originals; vec_wl_t *watches; - vec_wl_t *bin_watches; /* Activity heuristic */ act_t var_act_inc; /* Amount to bump next variable with. */ @@ -200,6 +199,7 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason) vec_uint_push_back(s->trail, lit); return SATOKO_OK; } + static inline int solver_varnum(solver_t *s) { return vec_char_size(s->assigns); @@ -227,25 +227,15 @@ static inline void clause_watch(solver_t *s, unsigned cref) w2.cref = cref; w1.blocker = clause->data[1].lit; w2.blocker = clause->data[0].lit; - if (clause->size == 2) { - watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), w1); - watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), w2); - } else { - watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1); - watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2); - } + watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1, (clause->size == 2)); + watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2, (clause->size == 2)); } static inline void clause_unwatch(solver_t *s, unsigned cref) { struct clause *clause = cdb_handler(s->all_clauses, cref); - if (clause->size == 2) { - watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), cref); - watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), cref); - } else { - watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref); - watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref); - } + watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref, (clause->size == 2)); + watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref, (clause->size == 2)); } ABC_NAMESPACE_HEADER_END diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index b446fb05..65fab837 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -89,7 +89,6 @@ solver_t * satoko_create() s->originals = vec_uint_alloc(0); s->learnts = vec_uint_alloc(0); s->watches = vec_wl_alloc(0); - s->bin_watches = vec_wl_alloc(0); /* Activity heuristic */ s->var_act_inc = VAR_ACT_INIT_INC; s->clause_act_inc = CLAUSE_ACT_INIT_INC; @@ -128,7 +127,6 @@ void satoko_destroy(solver_t *s) vec_uint_free(s->originals); vec_uint_free(s->learnts); vec_wl_free(s->watches); - vec_wl_free(s->bin_watches); vec_act_free(s->activity); heap_free(s->var_order); vec_uint_free(s->levels); @@ -145,7 +143,8 @@ void satoko_destroy(solver_t *s) vec_uint_free(s->stack); vec_uint_free(s->last_dlevel); vec_uint_free(s->stamps); - if (s->marks) vec_char_free(s->marks); + if (s->marks) + vec_char_free(s->marks); satoko_free(s); } @@ -220,13 +219,9 @@ int satoko_simplify(solver_t * s) void satoko_add_variable(solver_t *s, char sign) { unsigned var = vec_act_size(s->activity); - vec_wl_push(s->bin_watches); - vec_wl_push(s->bin_watches); vec_wl_push(s->watches); vec_wl_push(s->watches); - /* Variable activity are initialized with the lowest possible value - * which in satoko double implementation (SDBL) is the constant 1 */ - vec_act_push_back(s->activity, SDBL_CONST1); + vec_act_push_back(s->activity, 0); vec_uint_push_back(s->levels, 0); vec_char_push_back(s->assigns, VAR_UNASSING); vec_char_push_back(s->polarity, sign); @@ -320,23 +315,23 @@ satoko_stats_t satoko_stats(satoko_t *s) return s->stats; } -void satoko_mark_cone(satoko_t *s, int * pvars, int nvars) +void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars) { int i; if (!solver_has_marks(s)) - s->marks = vec_char_init(solver_varnum(s), 0); - for (i = 0; i < nvars; i++) - { + s->marks = vec_char_init(solver_varnum(s), 0); + for (i = 0; i < n_vars; i++) { var_set_mark(s, pvars[i]); if (!heap_in_heap(s->var_order, pvars[i])) heap_insert(s->var_order, pvars[i]); } } -void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars) + +void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars) { int i; assert(solver_has_marks(s)); - for (i = 0; i < nvars; i++) + for (i = 0; i < n_vars; i++) var_clean_mark(s, pvars[i]); } diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h index ef1c1a07..96399a83 100644 --- a/src/sat/satoko/watch_list.h +++ b/src/sat/satoko/watch_list.h @@ -10,6 +10,7 @@ #define satoko__watch_list_h #include "utils/mem.h" +#include "utils/misc.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START @@ -22,6 +23,7 @@ struct watcher { struct watch_list { unsigned cap; unsigned size; + unsigned n_bin; struct watcher *watchers; }; @@ -40,6 +42,10 @@ struct vec_wl_t_ { watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \ watch++) +#define watch_list_foreach_bin(vec, watch, lit) \ + for (watch = watch_list_array(vec_wl_at(vec, lit)); \ + watch < watch_list_array(vec_wl_at(vec, lit)) + vec_wl_at(vec, lit)->n_bin; \ + watch++) //===------------------------------------------------------------------------=== // Watch list API //===------------------------------------------------------------------------=== @@ -60,25 +66,33 @@ static inline void watch_list_shrink(struct watch_list *wl, unsigned size) wl->size = size; } -static inline void watch_list_push(struct watch_list *wl, struct watcher w) +static inline void watch_list_grow(struct watch_list *wl) { - assert(wl); - if (wl->size == wl->cap) { - unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3; - struct watcher *watchers = - satoko_realloc(struct watcher, wl->watchers, new_size); - if (watchers == NULL) { - printf("Failed to realloc memory from %.1f MB to %.1f " - "MB.\n", - 1.0 * wl->cap / (1 << 20), - 1.0 * new_size / (1 << 20)); - fflush(stdout); - return; - } - wl->watchers = watchers; - wl->cap = new_size; + unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3; + struct watcher *watchers = + satoko_realloc(struct watcher, wl->watchers, new_size); + if (watchers == NULL) { + printf("Failed to realloc memory from %.1f MB to %.1f " + "MB.\n", + 1.0 * wl->cap / (1 << 20), + 1.0 * new_size / (1 << 20)); + fflush(stdout); + return; } + wl->watchers = watchers; + wl->cap = new_size; +} + +static inline void watch_list_push(struct watch_list *wl, struct watcher w, unsigned is_bin) +{ + assert(wl); + if (wl->size == wl->cap) + watch_list_grow(wl); wl->watchers[wl->size++] = w; + if (is_bin && wl->size > wl->n_bin) { + stk_swap(struct watcher, wl->watchers[wl->n_bin], wl->watchers[wl->size - 1]); + wl->n_bin++; + } } static inline struct watcher *watch_list_array(struct watch_list *wl) @@ -86,11 +100,15 @@ static inline struct watcher *watch_list_array(struct watch_list *wl) return wl->watchers; } -static inline void watch_list_remove(struct watch_list *wl, unsigned cref) +static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin) { struct watcher *watchers = watch_list_array(wl); unsigned i; - for (i = 0; watchers[i].cref != cref; i++); + if (is_bin) { + for (i = 0; watchers[i].cref != cref; i++); + wl->n_bin--; + } else + for (i = wl->n_bin; watchers[i].cref != cref; i++); assert(i < watch_list_size(wl)); memmove((wl->watchers + i), (wl->watchers + i + 1), (wl->size - i - 1) * sizeof(struct watcher)); -- cgit v1.2.3