mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

working on weighted maxsat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-28 21:30:57 -07:00
parent 906bbb4eeb
commit d30f183476
5 changed files with 109 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/opt_context.cpp
View file

@ -59,14 +59,15 @@ namespace opt {
is_sat = opt::fu_malik_maxsat(*s, fmls_copy); is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
} }
else { else {
is_sat = weighted_maxsat(*s, fmls_copy, m_weights); is_sat = weighted_maxsat(get_opt_solver(*s), fmls_copy, m_weights);
} }
std::cout << "is-sat: " << is_sat << "\n"; std::cout << "is-sat: " << is_sat << "\n";
if (is_sat != l_true) { if (is_sat != l_true) {
return; return;
} }
std::cout << "Satisfying soft constraints\n";
for (unsigned i = 0; i < fmls_copy.size(); ++i) { for (unsigned i = 0; i < fmls_copy.size(); ++i) {
std::cout << "Satisfying soft constraint: " << mk_pp(fmls_copy[i].get(), m) << "\n"; std::cout << mk_pp(fmls_copy[i].get(), m) << "\n";
} }
} }
@ -75,9 +76,7 @@ namespace opt {
for (unsigned i = 0; i < fmls_copy.size(); ++i) { for (unsigned i = 0; i < fmls_copy.size(); ++i) {
s->assert_expr(fmls_copy[i].get()); s->assert_expr(fmls_copy[i].get());
} }
// SASSERT(instanceof(*s, opt_solver)); is_sat = optimize_objectives(get_opt_solver(*s), m_objectives, values);
// if (!instsanceof ...) { throw ... invalid usage ..}
is_sat = optimize_objectives(dynamic_cast<opt_solver&>(*s), m_objectives, values);
std::cout << "is-sat: " << is_sat << std::endl; std::cout << "is-sat: " << is_sat << std::endl;
if (is_sat != l_true) { if (is_sat != l_true) {
@ -108,6 +107,13 @@ namespace opt {
return true; return true;
} }
opt_solver& context::get_opt_solver(solver& s) {
if (typeid(opt_solver) != typeid(s)) {
throw default_exception("BUG: optimization context has not been initialized correctly");
}
return dynamic_cast<opt_solver&>(s);
}
void context::cancel() { void context::cancel() {
if (m_solver) { if (m_solver) {
m_solver->cancel(); m_solver->cancel();

4
src/opt/opt_context.h
View file

@ -30,6 +30,8 @@ Notes:
namespace opt { namespace opt {
class opt_solver;
class context { class context {
ast_manager& m; ast_manager& m;
expr_ref_vector m_hard_constraints; expr_ref_vector m_hard_constraints;
@ -70,6 +72,8 @@ namespace opt {
private: private:
bool is_maxsat_problem() const; bool is_maxsat_problem() const;
opt_solver& get_opt_solver(solver& s);
}; };
} }

3
src/opt/opt_solver.h
View file

@ -78,6 +78,9 @@ namespace opt {
toggle_objective(opt_solver& s, bool new_value); toggle_objective(opt_solver& s, bool new_value);
~toggle_objective(); ~toggle_objective();
}; };
smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
private: private:
smt::theory_opt& get_optimizer(); smt::theory_opt& get_optimizer();
}; };

118
src/opt/weighted_maxsat.cpp
View file

@ -20,34 +20,59 @@ Notes:
#include "smt_theory.h" #include "smt_theory.h"
#include "smt_context.h" #include "smt_context.h"
namespace opt { namespace smt {
class theory_weighted_maxsat : public smt::theory { class theory_weighted_maxsat : public theory {
expr_ref_vector m_vars;
expr_ref_vector m_fmls;
vector<rational> m_weights; // weights of theory variables. vector<rational> m_weights; // weights of theory variables.
svector<smt::theory_var> m_costs; // set of asserted theory variables svector<theory_var> m_costs; // set of asserted theory variables
rational m_cost; // current sum of asserted costs rational m_cost; // current sum of asserted costs
rational m_min_cost; // current minimal cost assignment. rational m_min_cost; // current minimal cost assignment.
svector<smt::theory_var> m_assignment; // current best assignment. svector<theory_var> m_assignment; // current best assignment.
public: public:
theory_weighted_maxsat(ast_manager& m): theory_weighted_maxsat(ast_manager& m):
theory(m.get_family_id("weighted_maxsat")) theory(m.get_family_id("weighted_maxsat")),
m_vars(m),
m_fmls(m)
{} {}
void get_assignment(expr_ref_vector& result) {
result.reset();
for (unsigned i = 0; i < m_assignment.size(); ++i) {
result.push_back(m_fmls[m_assignment[i]].get());
}
}
void assert_weighted(expr* fml, rational const& w) { void assert_weighted(expr* fml, rational const& w) {
smt::bool_var v = smt::null_theory_var; context & ctx = get_context();
// internalize fml ast_manager& m = get_manager();
// assert weighted clause. v \/ fml expr_ref var(m);
// var = m.mk_fresh_const("w", m.mk_bool_sort());
ctx.internalize(fml, false); // TBD: assume or require simplification?
ctx.internalize(var, false);
enode* x, *y;
x = ctx.get_enode(fml);
y = ctx.get_enode(var);
theory_var v = mk_var(y);
SASSERT(v == m_vars.size());
SASSERT(v == m_weights.size());
m_vars.push_back(var);
m_fmls.push_back(fml);
ctx.attach_th_var(y, this, v);
literal lx(ctx.get_bool_var(fml));
literal ly(ctx.get_bool_var(var));
ctx.mk_th_axiom(get_id(), lx, ly);
m_weights.push_back(w); m_weights.push_back(w);
m_min_cost += w; m_min_cost += w;
} }
virtual void assign_eh(smt::bool_var v, bool is_true) { virtual void assign_eh(bool_var v, bool is_true) {
smt::context& ctx = get_context();
if (is_true) { if (is_true) {
context& ctx = get_context();
rational const& w = m_weights[v]; rational const& w = m_weights[v];
ctx.push_trail(value_trail<smt::context, rational>(m_cost)); ctx.push_trail(value_trail<context, rational>(m_cost));
// TBD: ctx.push_trail(...trail.pop_back(m_costly)); ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
m_cost += w; m_cost += w;
m_costs.push_back(v); m_costs.push_back(v);
if (m_cost > m_min_cost) { if (m_cost > m_min_cost) {
@ -56,57 +81,92 @@ namespace opt {
} }
} }
virtual smt::final_check_status final_check_eh() { virtual final_check_status final_check_eh() {
if (m_cost < m_min_cost) { if (m_cost < m_min_cost) {
m_min_cost = m_cost; m_min_cost = m_cost;
m_assignment.reset(); m_assignment.reset();
m_assignment.append(m_costs); m_assignment.append(m_costs);
} }
block(); block();
return smt::FC_DONE; return FC_DONE;
} }
virtual void reset_eh() {
theory::reset_eh();
m_vars.reset();
m_weights.reset();
m_costs.reset();
m_cost.reset();
m_min_cost.reset();
m_assignment.reset();
}
virtual theory * mk_fresh(context * new_ctx) { UNREACHABLE(); return 0;} // TBD
virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; }
virtual bool internalize_term(app * term) { return false; }
virtual void new_eq_eh(theory_var v1, theory_var v2) { UNREACHABLE(); }
virtual void new_diseq_eh(theory_var v1, theory_var v2) { UNREACHABLE(); }
private: private:
class compare_cost { class compare_cost {
theory_weighted_maxsat& m_th; theory_weighted_maxsat& m_th;
public: public:
compare_cost(theory_weighted_maxsat& t):m_th(t) {} compare_cost(theory_weighted_maxsat& t):m_th(t) {}
bool operator() (smt::theory_var v, smt::theory_var w) const { bool operator() (theory_var v, theory_var w) const {
return m_th.m_weights[v] < m_th.m_weights[w]; return m_th.m_weights[v] < m_th.m_weights[w];
} }
}; };
void block() { void block() {
ast_manager& m = get_manager(); ast_manager& m = get_manager();
smt::context& ctx = get_context(); context& ctx = get_context();
smt::literal_vector lits; literal_vector lits;
compare_cost compare_cost(*this); compare_cost compare_cost(*this);
std::sort(m_costs.begin(), m_costs.end(), compare_cost); svector<theory_var> costs(m_costs);
std::sort(costs.begin(), costs.end(), compare_cost);
rational weight(0); rational weight(0);
for (unsigned i = 0; i < m_costs.size() && for (unsigned i = 0; i < costs.size() && weight < m_min_cost; ++i) {
weight < m_min_cost; ++i) { weight += m_weights[costs[i]];
weight += m_weights[m_costs[i]]; lits.push_back(~literal(costs[i]));
lits.push_back(~smt::literal(m_costs[i]));
} }
smt::justification * js = 0; justification * js = 0;
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
js = new (ctx.get_region()) js = new (ctx.get_region())
smt::theory_lemma_justification(get_id(), ctx, lits.size(), lits.c_ptr()); theory_lemma_justification(get_id(), ctx, lits.size(), lits.c_ptr());
} }
ctx.mk_clause(lits.size(), lits.c_ptr(), js, smt::CLS_AUX_LEMMA, 0); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
} }
}; };
}
namespace opt {
/** /**
Takes solver with hard constraints added. Takes solver with hard constraints added.
Returns a maximal satisfying subset of weighted soft_constraints Returns a maximal satisfying subset of weighted soft_constraints
that are still consistent with the solver state. that are still consistent with the solver state.
*/ */
lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) { lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
NOT_IMPLEMENTED_YET(); ast_manager& m = soft_constraints.get_manager();
return l_false; smt::context& ctx = s.get_context();
smt::theory_id th_id = m.get_family_id("weighted_maxsat");
smt::theory* th = ctx.get_theory(th_id);
if (!th) {
th = alloc(smt::theory_weighted_maxsat, m);
ctx.register_plugin(th);
}
smt::theory_weighted_maxsat* wth = dynamic_cast<smt::theory_weighted_maxsat*>(th);
for (unsigned i = 0; i < soft_constraints.size(); ++i) {
wth->assert_weighted(soft_constraints[i].get(), weights[i]);
}
lbool result = s.check_sat_core(0,0);
wth->get_assignment(soft_constraints);
return result;
} }
}; };

4
src/opt/weighted_maxsat.h
View file

@ -18,7 +18,7 @@ Notes:
#ifndef _OPT_WEIGHTED_MAX_SAT_H_ #ifndef _OPT_WEIGHTED_MAX_SAT_H_
#define _OPT_WEIGHTED_MAX_SAT_H_ #define _OPT_WEIGHTED_MAX_SAT_H_
#include "solver.h" #include "opt_solver.h"
namespace opt { namespace opt {
/** /**
@ -27,7 +27,7 @@ namespace opt {
that are still consistent with the solver state. that are still consistent with the solver state.
*/ */
lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights); lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
}; };
#endif #endif