summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/satoko/act_clause.h5
-rw-r--r--src/sat/satoko/act_var.h29
-rw-r--r--src/sat/satoko/satoko.h4
-rw-r--r--src/sat/satoko/solver.c15
-rw-r--r--src/sat/satoko/solver_api.c7
-rw-r--r--src/sat/satoko/types.h22
-rwxr-xr-xsrc/sat/satoko/utils/misc.h6
-rw-r--r--src/sat/satoko/utils/vec/vec_flt.h246
8 files changed, 300 insertions, 34 deletions
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 <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#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 */
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:10:01 +0000