From 871899dceac294f2b76c055a42d87176224028f2 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Thu, 9 Feb 2017 05:17:50 -0800 Subject: =?UTF-8?q?-=20Adding=20a=20compile=20time=20option=20to=20use=20f?= =?UTF-8?q?loats=20for=20var=20activity=20(now=20it=20can=20be=20either=20?= =?UTF-8?q?=E2=80=98double=E2=80=99,=20=E2=80=98float=E2=80=99=20or=20?= =?UTF-8?q?=E2=80=98unsigned=E2=80=99=20(default))=20-=20Adding=20vector?= =?UTF-8?q?=20of=20=E2=80=98float=E2=80=99=20-=20Adding=20an=20option=20to?= =?UTF-8?q?=20configure=20the=20ratio=20of=20learnt=20clauses=20to=20be=20?= =?UTF-8?q?kept=20in=20clause=20database=20at=20each=20reduction=20(0=20me?= =?UTF-8?q?ans=20no=20reduction).=20-=20Other=20small=20changes.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/sat/satoko/act_clause.h | 5 +- src/sat/satoko/act_var.h | 29 +++-- src/sat/satoko/satoko.h | 4 +- src/sat/satoko/solver.c | 15 +-- src/sat/satoko/solver_api.c | 7 +- src/sat/satoko/types.h | 22 +++- src/sat/satoko/utils/misc.h | 6 +- src/sat/satoko/utils/vec/vec_flt.h | 246 +++++++++++++++++++++++++++++++++++++ 8 files changed, 300 insertions(+), 34 deletions(-) create mode 100644 src/sat/satoko/utils/vec/vec_flt.h diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h index 2e80a1e6..1465e5ee 100644 --- a/src/sat/satoko/act_clause.h +++ b/src/sat/satoko/act_clause.h @@ -56,10 +56,9 @@ static inline void clause_act_rescale(solver_t *s) vec_uint_foreach(s->learnts, cref, i) { clause = clause_read(s, cref); - clause->data[clause->size].act >>= 14; + clause->data[clause->size].act >>= 10; } - s->clause_act_inc >>= 14; - s->clause_act_inc = mkt_uint_max(s->clause_act_inc, (1 << 10)); + s->clause_act_inc = stk_uint_max((s->clause_act_inc >> 10), (1 << 11)); } static inline void clause_act_bump(solver_t *s, struct clause *clause) diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h index 161e9d9a..aa8a76ab 100644 --- a/src/sat/satoko/act_var.h +++ b/src/sat/satoko/act_var.h @@ -16,27 +16,27 @@ #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -#ifdef SATOKO_ACT_VAR_DBLE +#if defined SATOKO_ACT_VAR_DBLE || defined SATOKO_ACT_VAR_FLOAT /** Re-scale the activity value for all variables. */ static inline void var_act_rescale(solver_t *s) { unsigned i; - double *activity = vec_dble_data(s->activity); + act_t *activity = vec_act_data(s->activity); - for (i = 0; i < vec_dble_size(s->activity); i++) - activity[i] *= 1e-100; - s->var_act_inc *= 1e-100; + for (i = 0; i < vec_act_size(s->activity); i++) + activity[i] *= VAR_ACT_RESCALE; + s->var_act_inc *= VAR_ACT_RESCALE; } /** Increment the activity value of one variable ('var') */ static inline void var_act_bump(solver_t *s, unsigned var) { - double *activity = vec_dble_data(s->activity); + act_t *activity = vec_act_data(s->activity); activity[var] += s->var_act_inc; - if (activity[var] > 1e100) + if (activity[var] > VAR_ACT_LIMIT) var_act_rescale(s); if (heap_in_heap(s->var_order, var)) heap_decrease(s->var_order, var); @@ -49,25 +49,24 @@ static inline void var_act_decay(solver_t *s) s->var_act_inc *= (1 / s->opts.var_decay); } -#else /* SATOKO_ACT_VAR_DBLE */ +#else static inline void var_act_rescale(solver_t *s) { unsigned i; - unsigned *activity = vec_uint_data(s->activity); + act_t *activity = vec_act_data(s->activity); - for (i = 0; i < vec_uint_size(s->activity); i++) + for (i = 0; i < vec_act_size(s->activity); i++) activity[i] >>= 19; - s->var_act_inc >>= 19; - s->var_act_inc = mkt_uint_max(s->var_act_inc, (1 << 5)); + s->var_act_inc = stk_uint_max((s->var_act_inc >> 19), (1 << 5)); } static inline void var_act_bump(solver_t *s, unsigned var) { - unsigned *activity = vec_uint_data(s->activity); + act_t *activity = vec_act_data(s->activity); activity[var] += s->var_act_inc; - if (activity[var] & 0x80000000) + if (activity[var] & 0xF0000000) var_act_rescale(s); if (heap_in_heap(s->var_order, var)) heap_decrease(s->var_order, var); @@ -78,7 +77,7 @@ static inline void var_act_decay(solver_t *s) s->var_act_inc += (s->var_act_inc >> 4); } -#endif /* SATOKO_ACT_VAR_DBLE */ +#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FLOAT */ ABC_NAMESPACE_HEADER_END #endif /* satoko__act_var_h */ diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 55790714..fb07c6f9 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -9,6 +9,7 @@ #ifndef satoko__satoko_h #define satoko__satoko_h +#include "types.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START @@ -45,10 +46,11 @@ struct satoko_opts { unsigned inc_reduce; /* Increment to reduce */ unsigned inc_special_reduce; /* Special increment to reduce */ unsigned lbd_freeze_clause; + float learnt_ratio; /* Percentage of learned clauses to remove */ /* VSIDS heuristic */ float clause_decay; - double var_decay; + act_t var_decay; /* Binary resolution */ unsigned clause_max_sz_bin_resol; diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index a4114e54..cdd3141e 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -45,7 +45,7 @@ static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level assert(var_reason(s, var) != UNDEF); if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { assert(lit_value(s, lits[1]) == LIT_TRUE); - mkt_swap(unsigned, lits[0], lits[1]); + stk_swap(unsigned, lits[0], lits[1]); } /* Check scan the literals of the reason clause. @@ -126,7 +126,7 @@ static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits) sz = vec_uint_size(clause_lits) - 1; for (i = 1; i < vec_uint_size(clause_lits) - counter; i++) if (vec_uint_at(s->stamps, lit2var(lits[i])) != s->cur_stamp) { - mkt_swap(unsigned, lits[i], lits[sz]); + stk_swap(unsigned, lits[i], lits[sz]); i--; sz--; } @@ -268,7 +268,7 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { assert(lit_value(s, lits[1]) == LIT_TRUE); - mkt_swap(unsigned, lits[0], lits[1] ); + stk_swap(unsigned, lits[0], lits[1] ); } if (clause->f_learnt) @@ -310,7 +310,7 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt *bt_level = solver_calc_bt_level(s, learnt); *lbd = clause_clac_lbd(s, vec_uint_data(learnt), vec_uint_size(learnt)); - if (vec_uint_size( s->last_dlevel) > 0) { + if (vec_uint_size(s->last_dlevel) > 0) { vec_uint_foreach(s->last_dlevel, var, i) { if (clause_read(s, var_reason(s, var))->lbd < *lbd) var_act_bump(s, var); @@ -428,7 +428,7 @@ static inline void solver_reduce_cdb(solver_t *s) vec_uint_foreach(s->learnts, cref, i) learnts_cls[i] = clause_read(s, cref); - limit = n_learnts / 2; + limit = (unsigned)(n_learnts * s->opts.learnt_ratio); satoko_sort((void *)learnts_cls, n_learnts, (int (*)(const void *, const void *)) clause_compare); @@ -562,7 +562,7 @@ unsigned solver_propagate(solver_t *s) // Make sure the false literal is data[1]: neg_lit = lit_neg(p); if (lits[0] == neg_lit) - mkt_swap(unsigned, lits[0], lits[1]); + stk_swap(unsigned, lits[0], lits[1]); assert(lits[1] == neg_lit); w.cref = i->cref; @@ -635,7 +635,8 @@ char solver_search(solver_t *s) satoko_simplify(s); /* Reduce the set of learnt clauses */ - if (s->stats.n_conflicts >= s->n_confl_bfr_reduce) { + if (s->opts.learnt_ratio && + s->stats.n_conflicts >= s->n_confl_bfr_reduce) { s->RC1 = (s->stats.n_conflicts / s->RC2) + 1; solver_reduce_cdb(s); s->RC2 += s->opts.inc_reduce; diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index e041cc62..980cc160 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -165,6 +165,7 @@ void satoko_default_opts(satoko_opts_t *opts) opts->inc_reduce = 300; opts->inc_special_reduce = 1000; opts->lbd_freeze_clause = 30; + opts->learnt_ratio = 0.5; /* VSIDS heuristic */ opts->var_decay = (act_t) 0.95; opts->clause_decay = (clause_act_t) 0.995; @@ -187,7 +188,7 @@ void satoko_configure(satoko_t *s, satoko_opts_t *user_opts) int satoko_simplify(solver_t * s) { unsigned i, j = 0; - unsigned cref; + unsigned cref; assert(solver_dlevel(s) == 0); if (solver_propagate(s) != UNDEF) @@ -198,7 +199,7 @@ int satoko_simplify(solver_t * s) vec_uint_foreach(s->originals, cref, i) { struct clause *clause = clause_read(s, cref); - if (clause_is_satisfied(s, clause)) { + if (clause_is_satisfied(s, clause)) { clause->f_mark = 1; s->stats.n_original_lits -= clause->size; clause_unwatch(s, cref); @@ -236,7 +237,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) unsigned max_var; unsigned cref; - qsort((void *) lits, size, sizeof(unsigned), mkt_uint_compare); + qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare); max_var = lit2var(lits[size - 1]); while (max_var >= vec_act_size(s->activity)) satoko_add_variable(s, LIT_FALSE); diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h index 2811c2c6..ee9363bc 100644 --- a/src/sat/satoko/types.h +++ b/src/sat/satoko/types.h @@ -10,23 +10,40 @@ #define satoko__types_h #include "utils/vec/vec_dble.h" +#include "utils/vec/vec_flt.h" #include "utils/vec/vec_uint.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -#define SATOKO_ACT_VAR_DBLE -#define SATOKO_ACT_CLAUSE_FLOAT +// #define SATOKO_ACT_VAR_DBLE +// #define SATOKO_ACT_VAR_FLOAT +// #define SATOKO_ACT_CLAUSE_FLOAT #ifdef SATOKO_ACT_VAR_DBLE #define VAR_ACT_INIT_INC 1.0 + #define VAR_ACT_LIMIT (double)1e100 + #define VAR_ACT_RESCALE (double)1e-100 typedef double act_t; typedef vec_dble_t vec_act_t ; #define vec_act_alloc(size) vec_dble_alloc(size) #define vec_act_free(vec) vec_dble_free(vec) #define vec_act_size(vec) vec_dble_size(vec) + #define vec_act_data(vec) vec_dble_data(vec) #define vec_act_at(vec, idx) vec_dble_at(vec, idx) #define vec_act_push_back(vec, value) vec_dble_push_back(vec, value) +#elif defined(SATOKO_ACT_VAR_FLOAT) + #define VAR_ACT_INIT_INC 1.0 + #define VAR_ACT_LIMIT (float)1e20 + #define VAR_ACT_RESCALE (float)1e-20 + typedef float act_t; + typedef vec_flt_t vec_act_t ; + #define vec_act_alloc(size) vec_flt_alloc(size) + #define vec_act_free(vec) vec_flt_free(vec) + #define vec_act_size(vec) vec_flt_size(vec) + #define vec_act_data(vec) vec_flt_data(vec) + #define vec_act_at(vec, idx) vec_flt_at(vec, idx) + #define vec_act_push_back(vec, value) vec_flt_push_back(vec, value) #else #define VAR_ACT_INIT_INC (1 << 5) typedef unsigned act_t; @@ -34,6 +51,7 @@ ABC_NAMESPACE_HEADER_START #define vec_act_alloc(size) vec_uint_alloc(size) #define vec_act_free(vec) vec_uint_free(vec) #define vec_act_size(vec) vec_uint_size(vec) + #define vec_act_data(vec) vec_uint_data(vec) #define vec_act_at(vec, idx) vec_uint_at(vec, idx) #define vec_act_push_back(vec, value) vec_uint_push_back(vec, value) #endif /* SATOKO_ACT_VAR_DBLE */ diff --git a/src/sat/satoko/utils/misc.h b/src/sat/satoko/utils/misc.h index 481e23b7..7205a096 100755 --- a/src/sat/satoko/utils/misc.h +++ b/src/sat/satoko/utils/misc.h @@ -12,14 +12,14 @@ #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -#define mkt_swap(type, a, b) { type t = a; a = b; b = t; } +#define stk_swap(type, a, b) { type t = a; a = b; b = t; } -static inline unsigned mkt_uint_max(unsigned a, unsigned b) +static inline unsigned stk_uint_max(unsigned a, unsigned b) { return a > b ? a : b; } -static inline int mkt_uint_compare(const void *p1, const void *p2) +static inline int stk_uint_compare(const void *p1, const void *p2) { const unsigned pp1 = *(const unsigned *)p1; const unsigned pp2 = *(const unsigned *)p2; diff --git a/src/sat/satoko/utils/vec/vec_flt.h b/src/sat/satoko/utils/vec/vec_flt.h new file mode 100644 index 00000000..d7c896d9 --- /dev/null +++ b/src/sat/satoko/utils/vec/vec_flt.h @@ -0,0 +1,246 @@ +//===--- vec_int.h ----------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +#ifndef satoko__utils__vec__vec_flt_h +#define satoko__utils__vec__vec_flt_h + +#include +#include +#include + +#include "../mem.h" + +#include "misc/util/abc_global.h" +ABC_NAMESPACE_HEADER_START + +typedef struct vec_flt_t_ vec_flt_t; +struct vec_flt_t_ { + unsigned cap; + unsigned size; + float *data; +}; + +//===------------------------------------------------------------------------=== +// Vector Macros +//===------------------------------------------------------------------------=== +#define vec_flt_foreach(vec, entry, i) \ + for (i = 0; (i < vec->size) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +#define vec_flt_foreach_start(vec, entry, i, start) \ + for (i = start; (i < vec_flt_size(vec)) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +#define vec_flt_foreach_stop(vec, entry, i, stop) \ + for (i = 0; (i < stop) && (((entry) = vec_flt_at(vec, i)), 1); i++) + +//===------------------------------------------------------------------------=== +// Vector API +//===------------------------------------------------------------------------=== +static inline vec_flt_t *vec_flt_alloc(unsigned cap) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + if (cap > 0 && cap < 16) + cap = 16; + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + return p; +} + +static inline vec_flt_t *vec_flt_alloc_exact(unsigned cap) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + p->size = 0; + p->cap = cap; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + return p; +} + +static inline vec_flt_t *vec_flt_init(unsigned size, float value) +{ + vec_flt_t* p = satoko_alloc(vec_flt_t, 1); + + p->cap = size; + p->size = size; + p->data = p->cap ? satoko_alloc(float, p->cap) : NULL; + memset(p->data, value, sizeof(float) * p->size); + return p; +} + +static inline void vec_flt_free(vec_flt_t *p) +{ + if (p->data != NULL) + satoko_free(p->data); + satoko_free(p); +} + +static inline unsigned vec_flt_size(vec_flt_t *p) +{ + return p->size; +} + +static inline void vec_flt_resize(vec_flt_t *p, unsigned new_size) +{ + p->size = new_size; + if (p->cap >= new_size) + return; + p->data = satoko_realloc(float, p->data, new_size); + assert(p->data != NULL); + p->cap = new_size; +} + +static inline void vec_flt_reserve(vec_flt_t *p, unsigned new_cap) +{ + if (p->cap >= new_cap) + return; + p->data = satoko_realloc(float, p->data, new_cap); + assert(p->data != NULL); + p->cap = new_cap; +} + +static inline unsigned vec_flt_capacity(vec_flt_t *p) +{ + return p->cap; +} + +static inline int vec_flt_empty(vec_flt_t *p) +{ + return p->size ? 0 : 1; +} + +static inline void vec_flt_erase(vec_flt_t *p) +{ + satoko_free(p->data); + p->size = 0; + p->cap = 0; +} + +static inline float vec_flt_at(vec_flt_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data[i]; +} + +static inline float *vec_flt_at_ptr(vec_flt_t *p, unsigned i) +{ + assert(i >= 0 && i < p->size); + return p->data + i; +} + +static inline float *vec_flt_data(vec_flt_t *p) +{ + assert(p); + return p->data; +} + +static inline void vec_flt_duplicate(vec_flt_t *dest, const vec_flt_t *src) +{ + assert(dest != NULL && src != NULL); + vec_flt_resize(dest, src->cap); + memcpy(dest->data, src->data, sizeof(float) * src->cap); + dest->size = src->size; +} + +static inline void vec_flt_copy(vec_flt_t *dest, const vec_flt_t *src) +{ + assert(dest != NULL && src != NULL); + vec_flt_resize(dest, src->size); + memcpy(dest->data, src->data, sizeof(float) * src->size); + dest->size = src->size; +} + +static inline void vec_flt_push_back(vec_flt_t *p, float value) +{ + if (p->size == p->cap) { + if (p->cap < 16) + vec_flt_reserve(p, 16); + else + vec_flt_reserve(p, 2 * p->cap); + } + p->data[p->size] = value; + p->size++; +} + +static inline void vec_flt_assign(vec_flt_t *p, unsigned i, float value) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + p->data[i] = value; +} + +static inline void vec_flt_insert(vec_flt_t *p, unsigned i, float value) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + vec_flt_push_back(p, 0); + memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(float)); + p->data[i] = value; +} + +static inline void vec_flt_drop(vec_flt_t *p, unsigned i) +{ + assert((i >= 0) && (i < vec_flt_size(p))); + memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(float)); + p->size -= 1; +} + +static inline void vec_flt_clear(vec_flt_t *p) +{ + p->size = 0; +} + +static inline int vec_flt_asc_compare(const void *p1, const void *p2) +{ + const float *pp1 = (const float *) p1; + const float *pp2 = (const float *) p2; + + if (*pp1 < *pp2) + return -1; + if (*pp1 > *pp2) + return 1; + return 0; +} + +static inline int vec_flt_desc_compare(const void* p1, const void* p2) +{ + const float *pp1 = (const float *) p1; + const float *pp2 = (const float *) p2; + + if (*pp1 > *pp2) + return -1; + if (*pp1 < *pp2) + return 1; + return 0; +} + +static inline void vec_flt_sort(vec_flt_t* p, int ascending) +{ + if (ascending) + qsort((void *) p->data, p->size, sizeof(float), + (int (*)(const void*, const void*)) vec_flt_asc_compare); + else + qsort((void *) p->data, p->size, sizeof(float), + (int (*)(const void*, const void*)) vec_flt_desc_compare); +} + +static inline long vec_flt_memory(vec_flt_t *p) +{ + return p == NULL ? 0 : sizeof(float) * p->cap + sizeof(vec_flt_t); +} + +static inline void vec_flt_print(vec_flt_t *p) +{ + unsigned i; + assert(p != NULL); + fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap); + for (i = 0; i < p->size; i++) + fprintf(stdout, " %f", p->data[i]); + fprintf(stdout, " }\n"); +} + +ABC_NAMESPACE_HEADER_END +#endif /* satoko__utils__vec__vec_flt_h */ -- cgit v1.2.3