mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

Complete Fu & Malik MAXSAT implementation

Browse source 
Mistakes:
(1) ast_manager shouldn't be replicated.
(2) assumptions should be used to compare with unsat cores
This commit is contained in:
Anh-Dung Phan 2013-10-16 17:55:53 -07:00
parent 8ae0b06912
commit 3da47a280e
2 changed files with 41 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/opt/fu_malik.cpp
View file

@ -6,8 +6,8 @@ Module Name:
fu_malik.cpp
Abstract:
Fu&Malik built-in optimization method.
Adapted from sample code.
Fu & Malik built-in optimization method.
Adapted from sample code in C.
Author:
@ -40,16 +40,18 @@ namespace opt {
solver& s;
expr_ref_vector m_soft;
expr_ref_vector m_aux;
public:
fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft):
m(m),
s(s),
m_soft(soft),
m_aux(m)
{
for (unsigned i = 0; i < m_soft.size(); i++) {
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
s.assert_expr(m.mk_or(soft[i], m_aux[i].get()));
s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
}
}
@ -82,12 +84,12 @@ namespace opt {
ptr_vector<expr> core;
s.get_unsat_core(core);
// update soft-constraints and aux_vars
for (unsigned i = 0; i < m_soft.size(); i++) {
// Update soft-constraints and aux_vars
for (unsigned i = 0; i < m_soft.size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < core.size(); ++j) {
found = m_soft[i].get() == core[j];
found = assumptions[i].get() == core[j];
}
if (!found) {
continue;
@ -106,46 +108,57 @@ namespace opt {
private:
void assert_at_most_one(expr_ref_vector const& block_vars) {
expr_ref has_one(m), no_one(m), at_most_one(m);
mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, no_one);
at_most_one = m.mk_or(has_one, no_one);
expr_ref has_one(m), has_zero(m), at_most_one(m);
mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero);
at_most_one = m.mk_or(has_one, has_zero);
s.assert_expr(at_most_one);
}
void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& no_one) {
void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) {
SASSERT(n != 0);
if (n == 1) {
has_one = vars[0];
no_one = m.mk_not(vars[0]);
has_zero = m.mk_not(vars[0]);
}
else {
unsigned mid = n/2;
expr_ref has_one1(m), has_one2(m), no_one1(m), no_one2(m);
mk_at_most_one(mid, vars, has_one1, no_one1);
mk_at_most_one(n-mid, vars+mid, has_one2, no_one2);
has_one = m.mk_or(m.mk_and(has_one1, no_one2), m.mk_and(has_one2, no_one1));
no_one = m.mk_and(no_one1, no_one2);
expr_ref has_one1(m), has_one2(m), has_zero1(m), has_zero2(m);
mk_at_most_one(mid, vars, has_one1, has_zero1);
mk_at_most_one(n-mid, vars+mid, has_one2, has_zero2);
has_one = m.mk_or(m.mk_and(has_one1, has_zero2), m.mk_and(has_one2, has_zero1));
has_zero = m.mk_and(has_zero1, has_zero2);
}
}
};
// TBD: the vector of soft constraints gets updated
// but we really want to return the maximal set of
// original soft constraints that are satisfied.
// so we need to read out of the model what soft constraints
// were satisfied.
lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) {
ast_manager m = soft_constraints.get_manager();
ast_manager& m = soft_constraints.get_manager();
lbool is_sat = s.check_sat(0,0);
if (!soft_constraints.empty() && is_sat == l_true) {
s.push();
fu_malik fm(m, s, soft_constraints);
while (!fm.step());
// Get a list of satisfying soft_constraints
model_ref model;
s.get_model(model);
expr_ref_vector result(m);
for (unsigned i = 0; i < soft_constraints.size(); ++i) {
expr_ref val(m);
VERIFY(model->eval(soft_constraints[i].get(), val));
if (!m.is_false(val)) {
result.push_back(soft_constraints[i].get());
}
}
soft_constraints.reset();
soft_constraints.append(result);
s.pop(1);
}
// we are done and soft_constraints has
// We are done and soft_constraints has
// been updated with the max-sat assignment.
return is_sat;

4
src/opt/fu_malik.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Fu&Malik built-in optimization method.
Adapted from sample code.
Adapted from sample code in C.
Author:
@ -23,7 +23,7 @@ Notes:
namespace opt {
/**
takes solver with hard constraints added.
Takes solver with hard constraints added.
Returns a maximal satisfying subset of soft_constraints
that are still consistent with the solver state.
*/