diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 9ecc16ecf..b28b7bec0 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -28,10 +28,11 @@ Notes: #include"probe_arith.h" #include"quant_tactics.h" #include"qffpa_tactic.h" +#include"sls_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), + cond(mk_is_qfbv_probe(), mk_qfbv_sls_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 77ff50454..61305386e 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -584,8 +584,8 @@ public: run_update(cur_depth); } - void randomize_local(goal_ref const & g) { - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); + void randomize_local(goal_ref const & g, unsigned int flip) { + ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, flip); // Randomize _all_ candidates: diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 6783d9621..c194af267 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -35,6 +35,17 @@ Notes: #include"sls_tactic.h" #include"nnf_tactic.h" +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 30 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 +#define _VNS_ 0 +#define _WEIGHT_DIST_ 3 +#define _WEIGHT_DIST_FACTOR_ 0.1 + #include"sls_params.hpp" #include"sls_evaluator.h" #include"sls_tracker.h" @@ -257,7 +268,7 @@ class sls_tactic : public tactic { // inversion doesn't make sense, let's do a flip instead. if (mt == MV_INV) mt = MV_FLIP; - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); + ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves); unsigned ucc = unsat_constants.size(); unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; func_decl * fd = unsat_constants[rc]; @@ -303,6 +314,82 @@ class sls_tactic : public tactic { m_mpz_manager.del(new_value); } + double find_best_move_vns(goal_ref const & g, ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { + mpz old_value, temp; + unsigned bv_sz, max_bv_sz = 0; + double new_score = score; + + for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0 ; i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + if (max_bv_sz < bv_sz) max_bv_sz = bv_sz; + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { + if (!m_mpz_manager.is_even(old_value)) { + // for odd values, try +1 + mk_inc(bv_sz, old_value, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + move = MV_INC; + } + else { + // for even values, try -1 + mk_dec(bv_sz, old_value, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + move = MV_DEC; + } + + // try inverting + mk_inv(bv_sz, old_value, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + move = MV_INV; + + // try to flip lsb + mk_flip(srt, old_value, 0, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { + new_bit = 0; + move = MV_FLIP; + } + } + + // reset to what it was before + double check = incremental_score(g, fd, old_value); + SASSERT(check == score); + } + +#if _VNS_ == 1 + for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++) +#else + if (new_score <= score) + for (unsigned j = 1; j < max_bv_sz && new_score < 1.0; j++) +#endif + for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0 ; i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + // What would happen if we flipped bit #j ? + if (j < bv_sz) + { + mk_flip(srt, old_value, j, temp); + + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { + new_bit = j; + move = MV_FLIP; + } + } + // reset to what it was before + double check = incremental_score(g, fd, old_value); + SASSERT(check == score); + } + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + return new_score; + } + double find_best_move(goal_ref const & g, ptr_vector & to_evaluate, double score, unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { mpz old_value, temp; @@ -372,22 +459,29 @@ class sls_tactic : public tactic { unsigned plateau_cnt = 0; - while (plateau_cnt < m_plateau_limit) { - + // Andreas: Why do we only allow so few plateaus? +#if _RESTARTS_ + while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#else + while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#endif do { checkpoint(); old_score = score; new_const = (unsigned)-1; - ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g); + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves); TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl; for (unsigned i = 0 ; i < to_evaluate.size(); i++) tout << to_evaluate[i]->get_name() << std::endl; ); +#if _VNS_ + score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); +#else score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); - +#endif if (new_const == static_cast(-1)) { TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl; for (unsigned i = 0; i < g->size(); i++) { @@ -400,9 +494,11 @@ class sls_tactic : public tactic { for (unsigned i = 0; i < g->size(); i++) tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " << m_tracker.get_score(g->form(i)) << std::endl; ); + // Andreas: If new_const == -1, shouldn't score = old_score anyway? score = old_score; } else { + // Andreas: Why does randomizing not count as a move? (Now it does.) m_stats.m_moves++; func_decl * fd = to_evaluate[new_const]; @@ -441,6 +537,7 @@ class sls_tactic : public tactic { if (score >= 1.0) { // score could theoretically be imprecise. + // Andreas: Can it only be imprecise in one direction? bool all_true = true; for (unsigned i = 0; i < g->size() && all_true; i++) if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) @@ -451,19 +548,30 @@ class sls_tactic : public tactic { } else TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;); } + /* + if (m_stats.m_moves % 100 == 0) + { + verbose_stream() << "(" << std::fixed << std::setprecision(10) << score << ")" << std::endl; + verbose_stream() << "(" << std::fixed << std::setprecision(2) << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; + }*/ } while (score > old_score && res == l_undef); - - if (score != old_score) + + // Andreas: Why do you check for old_score? This should always be equal due to the loop invariant. + if (score != old_score) { + report_tactic_progress("This should not happen I guess.", plateau_cnt); plateau_cnt = 0; - else { + } else { + m_stats.m_moves++; plateau_cnt++; - if (plateau_cnt < m_plateau_limit) { + //report_tactic_progress("Plateau.", plateau_cnt); + // Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway. + //if (plateau_cnt < m_plateau_limit) { TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; ); - m_evaluator.randomize_local(g); + m_evaluator.randomize_local(g, m_stats.m_moves); //mk_random_move(g); score = top_score(g); - } + //} } } @@ -484,7 +592,8 @@ class sls_tactic : public tactic { do { checkpoint(); - if ((m_stats.m_restarts % 100) == 0) + // Andreas: I think restarts are too impotant to ignore 99% of them are happening... + //if ((m_stats.m_restarts % 100) == 0) report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); res = search(g); @@ -492,9 +601,12 @@ class sls_tactic : public tactic { if (res == l_undef) m_tracker.randomize(); } - while (res != l_true && m_stats.m_restarts++ < m_max_restarts); + while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts); - if (res == l_true) { + verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; + + if (res == l_true) { + report_tactic_progress("Number of flips:", m_stats.m_moves); if (m_produce_models) { model_ref mdl = m_tracker.get_model(); mc = model2model_converter(mdl.get()); @@ -628,7 +740,13 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m), simp2_p)), using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m), +#if _CNF_ + // Andreas: We will probably never use this. CNF sucks. + mk_cnf_tactic(m, p)); +#else + // Andreas: How does a NNF actually look like? Can it contain ITE operators? mk_nnf_tactic(m, p)); +#endif } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 7fbafec60..1061bd90e 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -28,8 +28,8 @@ class sls_tracker { random_gen m_rng; unsigned m_random_bits; unsigned m_random_bits_cnt; - mpz m_zero, m_one, m_two; - + mpz m_zero, m_one, m_two; + struct value_score { value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; ~value_score() { if (m) m->del(value); } @@ -249,12 +249,46 @@ public: } } - void initialize(goal_ref const & g) { + void initialize_recursive(init_proc proc, expr_mark visited, expr * e) { + if (m_manager.is_and(e) || m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + initialize_recursive(proc, visited, q); + } + } + for_each_expr(proc, visited, e); + } + + void initialize_recursive(expr * e) { + if (m_manager.is_and(e) || m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + initialize_recursive(q); + } + } + ptr_vector t; + m_constants_occ.insert_if_not_there(e, t); + find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); + expr_fast_mark1 visited; + quick_for_each_expr(ffd_proc, visited, e); + } + + void initialize(goal_ref const & g) { init_proc proc(m_manager, *this); expr_mark visited; unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = g->form(i); + // Andreas: Maybe not fully correct. +#if _FOCUS_ == 2 + initialize_recursive(proc, visited, e); +#endif for_each_expr(proc, visited, e); } @@ -262,6 +296,10 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = g->form(i); + // Andreas: Maybe not fully correct. +#if _FOCUS_ == 2 + initialize_recursive(e); +#endif ptr_vector t; m_constants_occ.insert_if_not_there(e, t); find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); @@ -382,8 +420,6 @@ public: TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); } -#define _SCORE_AND_MIN - double score_bool(expr * n, bool negated = false) { TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); @@ -400,30 +436,41 @@ public: SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - #ifdef _SCORE_AND_MIN - double min = 1.0; + // Andreas: Seems to have no effect. Probably it does not even occur. +#if _SCORE_AND_AVG_ + double sum = 0.0; + for (unsigned i = 0; i < a->get_num_args(); i++) + sum += get_score(args[i]); + res = sum / (double) a->get_num_args(); +#else + double min = 1.0; for (unsigned i = 0; i < a->get_num_args(); i++) { double cur = get_score(args[i]); if (cur < min) min = cur; } res = min; - #else - double sum = 0.0; - for (unsigned i = 0; i < a->get_num_args(); i++) - sum += get_score(args[i]); - res = sum / (double) a->get_num_args(); - #endif +#endif } else if (m_manager.is_or(n)) { SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - double max = 0.0; + // Andreas: Seems to have no effect. Probably it is still too similar to the original version. +#if _SCORE_OR_MUL_ + double inv = 1.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + inv *= (1.0 - get_score(args[i])); + } + res = 1.0 - inv; +#else + double max = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) { double cur = get_score(args[i]); if (cur > max) max = cur; } res = max; +#endif } else if (m_manager.is_ite(n)) { SASSERT(!negated); @@ -468,7 +515,7 @@ public: } m_mpz_manager.machine_div(diff, m_two, diff); } - res = 1.0 - (hamming_distance / (double) bv_sz); + res = 1.0 - (hamming_distance / (double) bv_sz); #else rational r(diff); r /= m_powers(bv_sz); @@ -503,7 +550,7 @@ public: double dbl = n.get_double(); // In extreme cases, n is 0.9999 but to_double returns something > 1.0 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); + m_mpz_manager.del(diff); } } else { @@ -564,7 +611,7 @@ public: TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } - m_mpz_manager.del(x); + m_mpz_manager.del(x); m_mpz_manager.del(y); } else if (m_manager.is_not(n)) { @@ -598,6 +645,20 @@ public: SASSERT(res >= 0.0 && res <= 1.0); +#if _WEIGHT_DIST_ + app * a = to_app(n); + family_id afid = a->get_family_id(); + if (afid == m_bv_util.get_family_id()) +#endif +#if _WEIGHT_DIST_ == 1 + if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_; +#elif _WEIGHT_DIST_ == 2 + res *= res; +#elif _WEIGHT_DIST_ == 3 + if (res < 1.0) res = 0.0; +#endif + + TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); return res; } @@ -647,7 +708,111 @@ public: NOT_IMPLEMENTED_YET(); } - ptr_vector & get_unsat_constants(goal_ref const & g) { + ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { + for (unsigned i = 0; i < sz; i++) { + expr * q = g->form(i); + if (m_mpz_manager.eq(get_value(q), m_one)) + continue; + ptr_vector const & this_decls = m_constants_occ.find(q); + unsigned sz2 = this_decls.size(); + for (unsigned j = 0; j < sz2; j++) { + func_decl * fd = this_decls[j]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + } + } + return m_temp_constants; + } + + expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) { + for (unsigned i = pos; i < sz; i++) { + expr * q = g->form(i); + if (m_mpz_manager.neq(get_value(q), m_one)) + return q; + } + for (unsigned i = 0; i < pos; i++) { + expr * q = g->form(i); + if (m_mpz_manager.neq(get_value(q), m_one)) + return q; + } + return 0; + } + + ptr_vector & get_unsat_constants_walksat(goal_ref const & g, unsigned sz, unsigned int pos) { + expr * q = get_unsat_assertion(g, sz, pos); + // Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration. + if (!q) + return m_temp_constants; + + ptr_vector const & this_decls = m_constants_occ.find(q); + unsigned sz2 = this_decls.size(); + for (unsigned j = 0; j < sz2; j++) { + func_decl * fd = this_decls[j]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + } + return m_temp_constants; + } + + ptr_vector & go_deeper(expr * e) { + if (m_manager.is_bool(e)) { + if (m_manager.is_and(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + // Andreas: might be used for guided branching + //for (unsigned i = 0; i < a->get_num_args(); i++) { + //double cur = get_score(args[i]); + //} + // Andreas: A random number is better here since reusing flip will cause patterns. + unsigned int sz = a->get_num_args(); + unsigned int pos = get_random_uint(16) % sz; + for (unsigned int i = pos; i < sz; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + for (unsigned int i = 0; i < pos; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + } + else if (m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + unsigned int pos = get_random_uint(16) % sz; + for (unsigned int i = pos; i < sz; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + for (unsigned int i = 0; i < pos; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + } + } + ptr_vector const & this_decls = m_constants_occ.find(e); + unsigned sz2 = this_decls.size(); + for (unsigned j = 0; j < sz2; j++) { + func_decl * fd = this_decls[j]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + } + return m_temp_constants; + } + + ptr_vector & get_unsat_constants_crsat(goal_ref const & g, unsigned sz, unsigned int pos) { + expr * q = get_unsat_assertion(g, sz, pos); + if (!q) + return m_temp_constants; + + return go_deeper(q); + } + + ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { unsigned sz = g->size(); if (sz == 1) { @@ -655,19 +820,41 @@ public: } else { m_temp_constants.reset(); - for (unsigned i = 0; i < sz; i++) { - expr * q = g->form(i); - if (m_mpz_manager.eq(get_value(q), m_one)) - continue; - ptr_vector const & this_decls = m_constants_occ.find(q); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } +#if _FOCUS_ == 1 +#if _BFS_ == 3 + unsigned int pos = 0; + double max = get_score(g->form(0)); + unsigned sz = g->size(); + for (unsigned i = 1; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } } - return m_temp_constants; +#elif _BFS_ == 2 + unsigned int pos = 0; + double min = get_score(g->form(0)); + unsigned sz = g->size(); + for (unsigned i = 1; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; } + } +#elif _BFS_ == 1 + unsigned int pos = flip % m_constants.size(); +#else + unsigned int pos = get_random_uint(16) % m_constants.size(); +#endif + return get_unsat_constants_walksat(g, sz, pos); +#elif _FOCUS_ == 2 +#if _BFS_ + unsigned int pos = flip % m_constants.size(); +#else + unsigned int pos = get_random_uint(16) % m_constants.size(); +#endif + return get_unsat_constants_crsat(g, sz, pos); +#else + return get_unsat_constants_gsat(g, sz); +#endif } } }; diff --git a/versions/z3-crsat-0.01.txt b/versions/z3-crsat-0.01.txt new file mode 100644 index 000000000..49e1a1525 --- /dev/null +++ b/versions/z3-crsat-0.01.txt @@ -0,0 +1,12 @@ +More focused (_FOCUS_ == 2) WalkSAT version. +Variables are chosen among candidates in only one unsatisfied bit-vector term. +Flip rate slightly slower; probably due to larger hash-table and recursive formula structure. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 3 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-gsat-0.01.txt b/versions/z3-gsat-0.01.txt new file mode 100644 index 000000000..eb806a67f --- /dev/null +++ b/versions/z3-gsat-0.01.txt @@ -0,0 +1,10 @@ +Basic GSAT version. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 0 +#define _FOCUS_ 0 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-gsat-res-0.01.txt b/versions/z3-gsat-res-0.01.txt new file mode 100644 index 000000000..6a211f2bc --- /dev/null +++ b/versions/z3-gsat-res-0.01.txt @@ -0,0 +1,10 @@ +Basic GSAT version corresponding to Christoph's original code. +Restarts after 100 plateaus. + +#define _CNF_ 0 +#define _BFS_ 0 +#define _FOCUS_ 0 +#define _RESTARTS_ 1 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01.txt b/versions/z3-wsat-0.01.txt new file mode 100644 index 000000000..141193f76 --- /dev/null +++ b/versions/z3-wsat-0.01.txt @@ -0,0 +1,12 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion. +Flip rate increased by roughly 10%-300%. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01b.txt b/versions/z3-wsat-0.01b.txt new file mode 100644 index 000000000..2c0c0e7ad --- /dev/null +++ b/versions/z3-wsat-0.01b.txt @@ -0,0 +1,12 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion. +Chooses a random top level assertion instead of using a BFS approach (_BFS_ == 0). +No restarts. + +#define _CNF_ 0 +#define _BFS_ 0 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01c.txt b/versions/z3-wsat-0.01c.txt new file mode 100644 index 000000000..223560e08 --- /dev/null +++ b/versions/z3-wsat-0.01c.txt @@ -0,0 +1,12 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion. +AND is scored by average; OR is scored by inverse multiplication. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 1 +#define _SCORE_OR_MUL_ 1 \ No newline at end of file diff --git a/versions/z3-wsat-0.01d.txt b/versions/z3-wsat-0.01d.txt new file mode 100644 index 000000000..072191370 --- /dev/null +++ b/versions/z3-wsat-0.01d.txt @@ -0,0 +1,11 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion with MINIMAL top_score. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 2 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01e.txt b/versions/z3-wsat-0.01e.txt new file mode 100644 index 000000000..b018c5e0d --- /dev/null +++ b/versions/z3-wsat-0.01e.txt @@ -0,0 +1,11 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion with MAXIMAL top_score. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 3 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.02.txt b/versions/z3-wsat-0.02.txt new file mode 100644 index 000000000..34dcb157c --- /dev/null +++ b/versions/z3-wsat-0.02.txt @@ -0,0 +1,13 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion. +Score function reduced to 0/1. +No restarts. + +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 +#define _WEIGHTED_DIST_ 1 \ No newline at end of file diff --git a/versions/z3-wsat-res-0.01.txt b/versions/z3-wsat-res-0.01.txt new file mode 100644 index 000000000..575180a59 --- /dev/null +++ b/versions/z3-wsat-res-0.01.txt @@ -0,0 +1,13 @@ +Basic WalkSAT version. +Variables are chosen among candidates in only ONE top level assertion. +Flip rate increased by roughly 10%-300% compared to GSAT. +Restarts after 100 plateaus. +Fps slightly decreased due to restarts. + +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 1 +#define _TIMELIMIT_ 300 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 \ No newline at end of file