- Small bug fix in var activity (improve performance)

- New implementation of watcher lists.

4 files changed, 55 insertions, 56 deletions

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));