Skip to content

Commit 5dc8127

Browse files
NikolajBjornerNikolajBjorner
committed
refine maxresw option
1 parent 623b322 commit 5dc8127

4 files changed

Lines changed: 102 additions & 61 deletions

File tree

‎src/opt/maxcore.cpp‎

Lines changed: 96 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,8 @@ class maxcore : public maxsmt_solver_base {
193193
}
194194

195195
void add(expr* e) {
196-
s().assert_expr(e);
196+
if (!m.is_true(e))
197+
s().assert_expr(e);
197198
}
198199

199200
void add_soft(expr* e, rational const& w) {
@@ -536,22 +537,89 @@ class maxcore : public maxsmt_solver_base {
536537
}
537538
else {
538539
for (auto const &core : cores) {
539-
for (unsigned i = 0; i + 1 < core.size(); ++i) {
540-
auto [f, def, w] = core[i];
541-
add(def);
542-
new_assumption(f, w);
543-
}
544-
auto [f, def, w] = core.back();
545-
add(def);
546-
f = mk_not(f);
547-
add(f);
548-
m_lower += w;
549-
trace();
540+
process_unsatw(core);
550541
}
551542
return l_true;
552543
}
553544
}
554545

546+
void process_unsatw(weighted_softs const& core) {
547+
for (unsigned i = 0; i + 1 < core.size(); ++i) {
548+
auto [f, c, d, w] = core[i];
549+
add(c);
550+
add(d);
551+
new_assumption(f, w);
552+
}
553+
auto [f, c, d, w] = core.back();
554+
add(c);
555+
add(d);
556+
f = mk_not(f);
557+
add(f);
558+
if (core.size() <= 2)
559+
m_defs.push_back(f);
560+
m_lower += w;
561+
IF_VERBOSE(2, verbose_stream() << "(opt.maxresw increase-lower-bound " << w << ")\n");
562+
trace();
563+
}
564+
565+
weighted_softs core2weighted_soft(exprs const& core) {
566+
weighted_softs soft;
567+
for (expr *e : core) {
568+
rational w = get_weight(e);
569+
expr_ref tt(m.mk_true(), m);
570+
expr_ref s(e, m);
571+
soft.push_back({s, tt, tt, w});
572+
}
573+
std::sort(soft.begin(), soft.end(), [](auto const &a, auto const &b) { return a.weight > b.weight; });
574+
remove_soft(core, m_asms);
575+
expr_ref fml(m), conj(m), disj(m), c(m), a(m);
576+
IF_VERBOSE(2, verbose_stream() << "(opt.maxresw core weights:";
577+
for (auto const &[s, c, d, w] : soft) verbose_stream() << " " << w; verbose_stream() << ")\n";);
578+
for (unsigned i = 0; i + 1 < soft.size(); ++i) {
579+
rational w1 = soft[i].weight;
580+
rational w2 = soft[i + 1].weight;
581+
auto s1 = soft[i].soft;
582+
auto s2 = soft[i + 1].soft;
583+
SASSERT(w1 >= w2);
584+
// a => s1 | s2
585+
// c => s1 & s2
586+
// s1 := a
587+
// s2 := c
588+
// assume s1, w1 - w2
589+
// new soft constraints are s1 or s2 : w2, s1 & s2 or s3 : w3, ...
590+
// remove soft constraint of weight w_n
591+
c = mk_fresh_bool("c");
592+
a = mk_fresh_bool("a");
593+
594+
conj = m.mk_and(s1, s2);
595+
update_model(c, conj);
596+
conj = m.mk_implies(c, conj);
597+
598+
disj = m.mk_or(s1, s2);
599+
update_model(a, disj);
600+
disj = m.mk_implies(a, disj);
601+
602+
soft[i].weight = w2;
603+
soft[i].soft = a;
604+
soft[i + 1].soft = c;
605+
soft[i + 1].conj = conj;
606+
soft[i + 1].disj = disj;
607+
m_defs.push_back(conj);
608+
m_defs.push_back(disj);
609+
if (w1 > w2) {
610+
for (unsigned j = 0; j < i; ++j) {
611+
auto [s, conj, disj, w] = soft[j];
612+
if (!m.is_true(conj)) {
613+
add(conj);
614+
soft[j].conj = m.mk_true();
615+
}
616+
}
617+
new_assumption(s1, w1 - w2);
618+
}
619+
}
620+
return soft;
621+
}
622+
555623
lbool get_cores(vector<weighted_softs>& cores) {
556624
lbool is_sat = l_false;
557625
cores.reset();
@@ -578,50 +646,8 @@ class maxcore : public maxsmt_solver_base {
578646
return l_true;
579647
}
580648

581-
weighted_softs soft;
582-
for (expr* e : core) {
583-
rational w = get_weight(e);
584-
expr_ref fml(m.mk_true(), m);
585-
expr_ref s(e, m);
586-
soft.push_back({s, fml, w});
587-
}
588-
std::sort(soft.begin(), soft.end(),
589-
[](auto const& a, auto const& b) {
590-
return a.weight > b.weight;
591-
});
592-
remove_soft(core, m_asms);
593-
expr_ref fml(m), d(m);
594-
for (unsigned i = 0; i + 1 < soft.size(); ++i) {
595-
rational w1 = soft[i].weight;
596-
rational w2 = soft[i + 1].weight;
597-
auto s1 = soft[i].soft;
598-
auto s2 = soft[i + 1].soft;
599-
// verbose_stream() << "processing softs of weights " << s1 << " " << w1 << " and " << s2 << " " << w2 << "\n";
600-
SASSERT(w1 >= w2);
601-
// s1 := s1 or s2
602-
// d => s1 & s2
603-
// s2 := d
604-
// assume s1, w1 - w2
605-
// new soft constraints are s1 or s2 : w2, s1 & s2 or s3 : w3, ...
606-
// remove soft constraint of weight w_n
607-
d = mk_fresh_bool("d");
608-
fml = m.mk_and(s1, s2);
609-
update_model(d, fml);
610-
soft[i].weight = w2;
611-
soft[i].soft = m.mk_or(s1, s2);
612-
soft[i + 1].soft = d;
613-
soft[i + 1].def = m.mk_implies(d, fml);
614-
if (w1 > w2) {
615-
for (unsigned j = 0; j < i; ++j) {
616-
auto [s, def, w] = soft[j];
617-
if (!m.is_true(def)) {
618-
add(def);
619-
soft[j].def = m.mk_true();
620-
}
621-
}
622-
new_assumption(s1, w1 - w2);
623-
}
624-
}
649+
weighted_softs soft = core2weighted_soft(core);
650+
625651
cores.push_back(soft);
626652

627653
if (core.size() >= m_max_core_size)
@@ -687,7 +713,8 @@ class maxcore : public maxsmt_solver_base {
687713
max_resolve_rc2bin(core, w);
688714
break;
689715
case strategy_t::s_primalw:
690-
UNREACHABLE();
716+
max_resolve(core, w);
717+
break;
691718
default:
692719
max_resolve(core, w);
693720
break;
@@ -1067,6 +1094,18 @@ class maxcore : public maxsmt_solver_base {
10671094
}
10681095

10691096
void relax_cores(vector<expr_ref_vector> const& cores) {
1097+
if (m_st == s_primalw) {
1098+
for (auto const & core : cores) {
1099+
exprs _core(core.size(), core.data());
1100+
weighted_softs soft = core2weighted_soft(_core);
1101+
IF_VERBOSE(2, verbose_stream() << "(opt.maxresw relax-core weights:";
1102+
for (auto const &[s, c, d, w] : soft) verbose_stream() << " " << w;
1103+
verbose_stream() << ")\n";);
1104+
process_unsatw(soft);
1105+
}
1106+
return;
1107+
}
1108+
10701109
vector<weighted_core> wcores;
10711110
for (auto & core : cores) {
10721111
exprs _core(core.size(), core.data());

‎src/opt/maxsmt.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,10 @@ namespace opt {
4040

4141
struct weighted_soft {
4242
expr_ref soft;
43-
expr_ref def;
43+
expr_ref conj;
44+
expr_ref disj;
4445
rational weight;
45-
weighted_soft(expr_ref const& s, expr_ref const& d, rational const& w): soft(s), def(d), weight(w) {}
46+
weighted_soft(expr_ref const& s, expr_ref const& c, expr_ref const& d, rational const& w): soft(s), conj(c), disj(d), weight(w) {}
4647
};
4748
using weighted_softs = vector<weighted_soft>;
4849

‎src/opt/opt_context.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -800,7 +800,8 @@ namespace opt {
800800
if (!is_maxsat_query())
801801
return;
802802

803-
if (m_maxsat_engine != symbol("maxres") &&
803+
if (m_maxsat_engine != symbol("maxres") &&
804+
m_maxsat_engine != symbol("maxresw") &&
804805
m_maxsat_engine != symbol("rc2") &&
805806
m_maxsat_engine != symbol("rc2tot") &&
806807
m_maxsat_engine != symbol("rc2bin") &&

‎src/opt/opt_lns.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ namespace opt {
262262
bool all_assumed = true;
263263
for (expr* c : core)
264264
all_assumed &= m_is_assumption.is_marked(c);
265-
IF_VERBOSE(2, verbose_stream() << "core " << all_assumed << " - " << core.size() << "\n");
265+
IF_VERBOSE(5, verbose_stream() << "core " << all_assumed << " - " << core.size() << "\n");
266266
if (all_assumed)
267267
m_cores.push_back(core);
268268
}

0 commit comments

Comments
 (0)