- Adding a compile time option to use floats for var activity (now it can be…

- Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default))
- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.

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)

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 */

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;

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;

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

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 */

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;

src/sat/satoko/utils/vec/vec_flt.h

+//===--- 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 */