From b70096a97f82ad638e25472ea5e7a0d877d639dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 17:22:44 -0700 Subject: [PATCH] testing double lookahead Signed-off-by: Nikolaj Bjorner --- src/sat/sat_drat.cpp | 17 +++++++++++++++ src/sat/sat_drat.h | 2 ++ src/sat/sat_local_search.cpp | 8 +++---- src/sat/sat_local_search.h | 4 ++-- src/sat/sat_lookahead.h | 42 ++++++++++++++++++++++++++++++++---- src/test/main.cpp | 18 ++++++++++------ 6 files changed, 75 insertions(+), 16 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index ba4173eed..0f1b578f1 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -449,6 +449,23 @@ namespace sat { } } } + void drat::add(literal_vector const& c) { + for (unsigned i = 0; i < c.size(); ++i) declare(c[i]); + if (m_out) dump(c.size(), c.begin(), status::learned); + if (s.m_config.m_drat_check) { + switch (c.size()) { + case 0: add(); break; + case 1: append(c[0], status::learned); break; + default: { + verify(c.size(), c.begin()); + clause* cl = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), true); + append(*cl, status::external); + break; + } + } + } + } + void drat::del(literal l) { if (m_out) dump(1, &l, status::deleted); if (s.m_config.m_drat_check) append(l, status::deleted); diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index e9663628b..2765d104c 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -57,6 +57,7 @@ namespace sat { void append(literal l, status st); void append(literal l1, literal l2, status st); void append(clause& c, status st); + friend std::ostream& operator<<(std::ostream & out, status st); status get_status(bool learned) const; @@ -82,6 +83,7 @@ namespace sat { void add(literal l1, literal l2, bool learned); void add(clause& c, bool learned); void add(literal_vector const& c, svector const& premises); + void add(literal_vector const& c); // add learned clause bool is_cleaned(clause& c) const; void del(literal l); diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index c9a947712..6b0205cc2 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -142,11 +142,11 @@ namespace sat { // the current best noise is below 1000 if (best_unsat_rate >= last_best_unsat_rate) { // worse - noise = noise - noise * 2 * noise_delta; + m_noise -= m_noise * 2 * m_noise_delta; } else { // better - noise = noise + (10000 - noise) * noise_delta; + m_noise += (10000 - m_noise) * m_noise_delta; } for (unsigned i = 0; i < m_constraints.size(); ++i) { constraint& c = m_constraints[i]; @@ -381,7 +381,7 @@ namespace sat { if (tries % 10 == 0 || m_unsat_stack.empty()) { \ IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ << " :flips " << flips \ - << " :noise " << noise \ + << " :noise " << m_noise \ << " :unsat " << /*m_unsat_stack.size()*/ best_unsat \ << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ } @@ -506,7 +506,7 @@ namespace sat { SASSERT(c.m_k < constraint_value(c)); // TBD: dynamic noise strategy //if (m_rand() % 100 < 98) { - if (m_rand() % 10000 >= noise) { + if (m_rand() % 10000 >= m_noise) { // take this branch with 98% probability. // find the first one, to fast break the rest unsigned best_bsb = 0; diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 7fb5396fe..678eee60a 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -176,8 +176,8 @@ namespace sat { unsigned m_max_steps = (1 << 30); // dynamic noise - unsigned noise = 400; // normalized by 10000 - double noise_delta = 0.05; + double m_noise = 400; // normalized by 10000 + double m_noise_delta = 0.05; // for tuning int s_id = 0; // strategy id diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index fa9fea724..3344e82e1 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -113,6 +113,9 @@ namespace sat { config m_config; double m_delta_trigger; + drat m_drat; + literal_vector m_assumptions; + literal_vector m_trail; // trail of units unsigned_vector m_trail_lim; vector m_binary; // literal: binary clauses @@ -229,6 +232,7 @@ namespace sat { m_binary[(~l2).index()].push_back(l1); m_binary_trail.push_back((~l1).index()); ++m_stats.m_add_binary; + if (s.m_config.m_drat) validate_binary(l1, l2); } void del_binary(unsigned idx) { @@ -240,6 +244,17 @@ namespace sat { ++m_stats.m_del_binary; } + + void validate_binary(literal l1, literal l2) { + if (m_search_mode == lookahead_mode::searching) { + m_assumptions.push_back(l1); + m_assumptions.push_back(l2); + m_drat.add(m_assumptions); + m_assumptions.pop_back(); + m_assumptions.pop_back(); + } + } + // ------------------------------------- // track consequences of binary clauses // see also 72 - 79 in sat11.w @@ -1034,14 +1049,18 @@ namespace sat { for (unsigned i = 0; i < c.size(); ++i) { m_full_watches[(~c[i]).index()].push_back(c1); } + if (s.m_config.m_drat) m_drat.add(c, false); } // copy units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { literal l = s.m_trail[i]; + if (s.m_config.m_drat) m_drat.add(l, false); assign(l); } + propagate(); + m_qhead = m_trail.size(); TRACE("sat", s.display(tout); display(tout);); } @@ -1056,11 +1075,13 @@ namespace sat { m_retired_ternary_lim.push_back(m_retired_ternary.size()); m_qhead_lim.push_back(m_qhead); scoped_level _sl(*this, level); + m_assumptions.push_back(~lit); assign(lit); propagate(); } void pop() { + m_assumptions.pop_back(); m_inconsistent = false; SASSERT(m_search_mode == lookahead_mode::searching); @@ -1319,7 +1340,7 @@ namespace sat { for (; m_qhead < m_trail.size(); ++m_qhead) { if (inconsistent()) break; literal l = m_trail[m_qhead]; - TRACE("sat", tout << "propagate " << l << "\n";); + TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); propagate_binary(l); propagate_clauses(l); } @@ -1360,7 +1381,7 @@ namespace sat { TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); reset_wnb(lit); push_lookahead1(lit, level); - //do_double(lit, base); + do_double(lit, base); bool unsat = inconsistent(); pop_lookahead1(lit); if (unsat) { @@ -1386,12 +1407,14 @@ namespace sat { } void init_wnb() { + TRACE("sat", tout << "init_wnb: " << m_qhead << "\n";); m_qhead_lim.push_back(m_qhead); m_trail_lim.push_back(m_trail.size()); } void reset_wnb() { m_qhead = m_qhead_lim.back(); + TRACE("sat", tout << "reset_wnb: " << m_qhead << "\n";); unsigned old_sz = m_trail_lim.back(); for (unsigned i = old_sz; i < m_trail.size(); ++i) { set_undef(m_trail[i]); @@ -1541,14 +1564,15 @@ namespace sat { SASSERT(dl_no_overflow(base)); unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); scoped_level _sl(*this, dl_truth); + init_wnb(); assign(l); propagate(); bool change = true; unsigned num_iterations = 0; - init_wnb(); while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { change = false; num_iterations++; + base += 2*m_lookahead.size(); for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; if (is_fixed_at(lit, dl_truth)) continue; @@ -1564,7 +1588,6 @@ namespace sat { } } SASSERT(dl_truth - 2 * m_lookahead.size() > base); - base += 2*m_lookahead.size(); } reset_wnb(); SASSERT(m_level == dl_truth); @@ -1576,6 +1599,14 @@ namespace sat { unsigned scope_lvl() const { return m_trail_lim.size(); } + void validate_assign(literal l) { + if (s.m_config.m_drat && m_search_mode == lookahead_mode::searching) { + m_assumptions.push_back(l); + m_drat.add(m_assumptions); + m_assumptions.pop_back(); + } + } + void assign(literal l) { SASSERT(m_level > 0); if (is_undef(l)) { @@ -1586,11 +1617,13 @@ namespace sat { m_stats.m_propagations++; TRACE("sat", tout << "removing free var v" << l.var() << "\n";); m_freevars.remove(l.var()); + validate_assign(l); } } else if (is_false(l)) { TRACE("sat", tout << "conflict: " << l << " @ " << m_level << " " << m_search_mode << "\n";); SASSERT(!is_true(l)); + validate_assign(l); set_conflict(); } } @@ -1709,6 +1742,7 @@ namespace sat { public: lookahead(solver& s) : s(s), + m_drat(s), m_level(2), m_prefix(0) { m_search_mode = lookahead_mode::searching; diff --git a/src/test/main.cpp b/src/test/main.cpp index dd705de4b..28b1537f9 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -77,12 +77,12 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t int i = 1; while (i < argc) { char * arg = argv[i]; + char * eq_pos = 0; if (arg[0] == '-' || arg[0] == '/') { char * opt_name = arg + 1; char * opt_arg = 0; char * colon = strchr(arg, ':'); - char * eq_pos = 0; if (colon) { opt_arg = colon + 1; *colon = 0; @@ -119,13 +119,19 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t enable_debug(opt_arg); } #endif - else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) { - char * key = arg; - *eq_pos = 0; - char * value = eq_pos+1; + } + else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) { + char * key = arg; + *eq_pos = 0; + char * value = eq_pos+1; + try { gparams::set(key, value); } - } + catch (z3_exception& ex) { + std::cerr << ex.msg() << "\n"; + } + } + i++; } }