mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
rework sat.mus to use restart count for bounded minimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c3eb279637
commit
962979b09c
|
@ -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<bool> _disable_min(s.m_config.m_core_minimize, false);
|
||||
flet<bool> _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<unsigned> _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();
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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; }
|
||||
|
|
Loading…
Reference in a new issue