diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 380b8ee94..06851d10d 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -23,7 +23,7 @@ Notes: namespace sat { - mus::mus(solver& s):s(s), m_is_active(false),m_restart(0), m_max_restarts(0) {} + mus::mus(solver& s):s(s), m_is_active(false), m_max_num_restarts(UINT_MAX) {} mus::~mus() {} @@ -31,8 +31,6 @@ namespace sat { m_core.reset(); m_mus.reset(); m_model.reset(); - m_max_restarts = (s.m_stats.m_restart - m_restart) + 10; - m_restart = s.m_stats.m_restart; } void mus::set_core() { @@ -49,12 +47,12 @@ namespace sat { } lbool mus::operator()() { + m_max_num_restarts = s.m_config.m_core_minimize_partial ? s.num_restarts() + 10 : UINT_MAX; flet _disable_min(s.m_config.m_core_minimize, false); flet _is_active(m_is_active, true); - IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); + IF_VERBOSE(3, verbose_stream() << "(sat.mus size: " << s.get_core().size() << " core: [" << s.get_core() << "])\n";); reset(); lbool r = mus1(); - m_restart = s.m_stats.m_restart; return r; } @@ -63,13 +61,13 @@ namespace sat { TRACE("sat", tout << "old core: " << s.get_core() << "\n";); literal_vector& core = get_core(); literal_vector& mus = m_mus; - if (core.size() > 64) { + if (!minimize_partial && core.size() > 64) { return mus2(); } - unsigned delta_time = 0; - unsigned core_miss = 0; while (!core.empty()) { - IF_VERBOSE(3, verbose_stream() << "(opt.mus reducing core: " << core.size() << " mus: " << mus.size() << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat.mus num-to-process: " << core.size() << " mus: " << mus.size(); + if (minimize_partial) verbose_stream() << " max-restarts: " << m_max_num_restarts; + verbose_stream() << ")\n";); TRACE("sat", tout << "core: " << core << "\n"; tout << "mus: " << mus << "\n";); @@ -78,34 +76,35 @@ namespace sat { set_core(); return l_undef; } - if (minimize_partial && 3*delta_time > core.size() && core.size() < mus.size()) { - break; - } unsigned num_literals = core.size() + mus.size(); if (num_literals <= 2) { // IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";); break; } - if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); - set_core(); - return l_true; - } literal lit = core.back(); core.pop_back(); lbool is_sat; { + flet _restart_bound(s.m_config.m_restart_max, m_max_num_restarts); scoped_append _sa(mus, core); mus.push_back(~lit); is_sat = s.check(mus.size(), mus.c_ptr()); TRACE("sat", tout << "mus: " << mus << "\n";); } + IF_VERBOSE(1, verbose_stream() << "(sat.mus " << is_sat << ")\n";); switch (is_sat) { case l_undef: - core.push_back(lit); - set_core(); - return l_undef; + if (!s.canceled()) { + // treat restart max as sat, so literal is in the mus + mus.push_back(lit); + } + else { + core.push_back(lit); + set_core(); + return l_undef; + } + break; case l_true: { SASSERT(value_at(lit, s.get_model()) == l_false); mus.push_back(lit); @@ -115,11 +114,9 @@ namespace sat { case l_false: literal_vector const& new_core = s.get_core(); if (new_core.contains(~lit)) { - IF_VERBOSE(3, verbose_stream() << "miss core " << lit << "\n";); - ++core_miss; + IF_VERBOSE(3, verbose_stream() << "(sat.mus unit reduction, literal is in both cores " << lit << ")\n";); } else { - core_miss = 0; TRACE("sat", tout << "core: " << new_core << " mus: " << mus << "\n";); core.reset(); for (unsigned i = 0; i < new_core.size(); ++i) { @@ -131,14 +128,6 @@ namespace sat { } break; } - - unsigned new_num_literals = core.size() + mus.size(); - if (new_num_literals == num_literals) { - delta_time++; - } - else { - delta_time = 0; - } } set_core(); IF_VERBOSE(3, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";); @@ -159,13 +148,9 @@ namespace sat { lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) { lbool is_sat = l_true; - if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); - return l_true; - } if (has_support) { scoped_append _sa(m_mus, support.to_vector()); - is_sat = s.check(m_mus.size(), m_mus.c_ptr()); + is_sat = s.check(m_mus.size(), m_mus.c_ptr()); switch (is_sat) { case l_false: { literal_set core(s.get_core()); @@ -173,7 +158,7 @@ namespace sat { assignment.reset(); return l_true; } - case l_undef: + case l_undef: return l_undef; case l_true: update_model(); diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index 74f6d75f0..946f66ed6 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -26,8 +26,7 @@ namespace sat { literal_vector m_mus; bool m_is_active; model m_model; // model obtained during minimal unsat core - unsigned m_restart; - unsigned m_max_restarts; + unsigned m_max_num_restarts; public: diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index dcf7e2acb..aa7e6edea 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -209,6 +209,7 @@ namespace sat { bool inconsistent() const { return m_inconsistent; } unsigned num_vars() const { return m_level.size(); } unsigned num_clauses() const; + unsigned num_restarts() const { return m_restarts; } bool is_external(bool_var v) const { return m_external[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; }