diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-09 05:17:50 -0800 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-09 05:17:50 -0800 |
commit | 871899dceac294f2b76c055a42d87176224028f2 (patch) | |
tree | be960be285aeeee82adb0de91f0e60022b835bf8 /src/sat/satoko/solver_api.c | |
parent | 040b88a7c6bc437f6f9dc792510d5d905b516eb5 (diff) | |
download | abc-871899dceac294f2b76c055a42d87176224028f2.tar.gz abc-871899dceac294f2b76c055a42d87176224028f2.tar.bz2 abc-871899dceac294f2b76c055a42d87176224028f2.zip |
- 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.
Diffstat (limited to 'src/sat/satoko/solver_api.c')
-rw-r--r-- | src/sat/satoko/solver_api.c | 7 |
1 files changed, 4 insertions, 3 deletions
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); |