From 088aabc1023e6745bedeb16f9f8f01515c38e4b7 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Wed, 15 Feb 2017 17:02:32 -0800 Subject: - Small changes to the watch lists behavior. - Implementation of bookmark, unbookmark and rollback procedures. - Minor changes. --- src/sat/satoko/satoko.h | 7 +++-- src/sat/satoko/solver.c | 5 ++-- src/sat/satoko/solver.h | 6 ++++ src/sat/satoko/solver_api.c | 56 ++++++++++++++++++++++++++++++++++++- src/sat/satoko/types.h | 1 + src/sat/satoko/utils/vec/vec_sdbl.h | 6 ++++ src/sat/satoko/watch_list.h | 22 +++++++++++++++ 7 files changed, 98 insertions(+), 5 deletions(-) diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 8d55a81c..88070eac 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -89,9 +89,12 @@ extern void satoko_assump_push(satoko_t *s, unsigned); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); -extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars); -extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars); +extern void satoko_mark_cone(satoko_t *, int *, int); +extern void satoko_unmark_cone(satoko_t *, int *, int); +extern void satoko_rollback(satoko_t *); +extern void satoko_bookmark(satoko_t *); +extern void satoko_unbookmark(satoko_t *); /* If problem is unsatisfiable under assumptions, this function is used to * obtain the final conflict clause expressed in the assumptions. * diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index d2bf1b5e..21a4860d 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -402,6 +402,7 @@ static inline void solver_garbage_collect(solver_t *s) clause_realloc(new_cdb, s->all_clauses, &(w->cref)); } + /* Update CREFS */ for (i = 0; i < vec_uint_size(s->trail); i++) if (lit_reason(s, vec_uint_at(s->trail, i)) != UNDEF) clause_realloc(new_cdb, s->all_clauses, &(vec_uint_data(s->reasons)[lit2var(vec_uint_at(s->trail, i))])); @@ -427,7 +428,7 @@ static inline void solver_reduce_cdb(solver_t *s) struct clause **learnts_cls; learnts_cls = satoko_alloc(struct clause *, n_learnts); - vec_uint_foreach(s->learnts, cref, i) + vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt) learnts_cls[i] = clause_read(s, cref); limit = (unsigned)(n_learnts * s->opts.learnt_ratio); @@ -504,7 +505,7 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt) return cref; } -void solver_cancel_until(solver_t * s, unsigned level) +void solver_cancel_until(solver_t *s, unsigned level) { int i; diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 84c25689..68cc97dc 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -92,6 +92,12 @@ struct solver_t_ { vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and * clauses minimization with binary resolution */ + /* Bookmark */ + unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */ + unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */ + unsigned book_vars; /* Bookmark number of variables */ + unsigned book_trail; /* Bookmark trail size */ + /* Temporary data used for solving cones */ vec_char_t *marks; diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 65fab837..9cad0a14 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -229,7 +229,8 @@ void satoko_add_variable(solver_t *s, char sign) vec_uint_push_back(s->stamps, 0); vec_char_push_back(s->seen, 0); heap_insert(s->var_order, var); - if (s->marks) vec_char_push_back(s->marks, 0); + if (s->marks) + vec_char_push_back(s->marks, 0); } int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) @@ -315,6 +316,59 @@ satoko_stats_t satoko_stats(satoko_t *s) return s->stats; } +void satoko_bookmark(satoko_t *s) +{ + assert(solver_dlevel(s) == 0); + s->book_cl_orig = vec_uint_size(s->originals); + s->book_cl_lrnt = vec_uint_size(s->learnts); + s->book_vars = vec_char_size(s->assigns); + s->book_trail = vec_uint_size(s->trail); +} + +void satoko_unbookmark(satoko_t *s) +{ + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_vars = 0; + s->book_trail = 0; +} + +void satoko_rollback(satoko_t *s) +{ + unsigned i, cref; + unsigned n_originals = vec_uint_size(s->originals) - s->book_cl_orig; + unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt; + struct clause **cl_to_remove; + + assert(solver_dlevel(s) == 0); + cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts); + /* Mark clauses */ + vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig) + cl_to_remove[i] = clause_read(s, cref); + vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt) + cl_to_remove[n_originals + i] = clause_read(s, cref); + for (i = 0; i < n_originals + n_learnts; i++) { + clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i])); + cl_to_remove[i]->f_mark = 1; + } + vec_uint_shrink(s->originals, s->book_cl_orig); + vec_uint_shrink(s->learnts, s->book_cl_lrnt); + /* Shrink variable related vectors */ + vec_act_shrink(s->activity, s->book_vars); + vec_uint_shrink(s->levels, s->book_vars); + vec_uint_shrink(s->reasons, s->book_vars); + vec_char_shrink(s->assigns, s->book_vars); + vec_char_shrink(s->polarity, s->book_vars); + solver_rebuild_order(s); + /* Rewind solver and cancel level 0 assignments to the trail */ + solver_cancel_until(s, 0); + vec_uint_shrink(s->trail, s->book_trail); + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_vars = 0; + s->book_trail = 0; +} + void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars) { int i; diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h index d51aed4c..9c47ca7c 100644 --- a/src/sat/satoko/types.h +++ b/src/sat/satoko/types.h @@ -26,6 +26,7 @@ typedef vec_sdbl_t vec_act_t ; #define vec_act_free(vec) vec_sdbl_free(vec) #define vec_act_size(vec) vec_sdbl_size(vec) #define vec_act_data(vec) vec_sdbl_data(vec) +#define vec_act_shrink(vec, size) vec_sdbl_shrink(vec, size) #define vec_act_at(vec, idx) vec_sdbl_at(vec, idx) #define vec_act_push_back(vec, value) vec_sdbl_push_back(vec, value) diff --git a/src/sat/satoko/utils/vec/vec_sdbl.h b/src/sat/satoko/utils/vec/vec_sdbl.h index aefd687a..ec1c731c 100755 --- a/src/sat/satoko/utils/vec/vec_sdbl.h +++ b/src/sat/satoko/utils/vec/vec_sdbl.h @@ -86,6 +86,12 @@ static inline unsigned vec_sdbl_size(vec_sdbl_t *p) return p->size; } +static inline void vec_sdbl_shrink(vec_sdbl_t *p, unsigned new_size) +{ + assert(new_size <= p->cap); + p->size = new_size; +} + static inline void vec_sdbl_resize(vec_sdbl_t *p, unsigned new_size) { p->size = new_size; diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h index 96399a83..49f419f2 100644 --- a/src/sat/satoko/watch_list.h +++ b/src/sat/satoko/watch_list.h @@ -100,6 +100,27 @@ static inline struct watcher *watch_list_array(struct watch_list *wl) return wl->watchers; } +/* TODO: I still have mixed feelings if this change should be done, keeping the + * old code commented after it. */ +static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin) +{ + struct watcher *watchers = watch_list_array(wl); + unsigned i; + if (is_bin) { + for (i = 0; watchers[i].cref != cref; i++); + assert(i < watch_list_size(wl)); + wl->n_bin--; + memmove((wl->watchers + i), (wl->watchers + i + 1), + (wl->size - i - 1) * sizeof(struct watcher)); + } else { + for (i = wl->n_bin; watchers[i].cref != cref; i++); + assert(i < watch_list_size(wl)); + stk_swap(struct watcher, wl->watchers[i], wl->watchers[wl->size - 1]); + } + wl->size -= 1; +} + +/* static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsigned is_bin) { struct watcher *watchers = watch_list_array(wl); @@ -114,6 +135,7 @@ static inline void watch_list_remove(struct watch_list *wl, unsigned cref, unsig (wl->size - i - 1) * sizeof(struct watcher)); wl->size -= 1; } +*/ static inline vec_wl_t *vec_wl_alloc(unsigned cap) { -- cgit v1.2.3