mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
apply 'to-real' coercion only on integers. bug reported by Geoff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
b56837e09b
commit
f522d995d1
|
|
@ -828,7 +828,10 @@ class env {
|
||||||
}
|
}
|
||||||
else if (!strcmp(ch,"$to_real")) {
|
else if (!strcmp(ch,"$to_real")) {
|
||||||
check_arity(terms.size(), 1);
|
check_arity(terms.size(), 1);
|
||||||
r = to_real(terms[0]);
|
r = terms[0];
|
||||||
|
if (r.get_sort().is_int()) {
|
||||||
|
r = to_real(terms[0]);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
else if (!strcmp(ch,"$is_int")) {
|
else if (!strcmp(ch,"$is_int")) {
|
||||||
check_arity(terms.size(), 1);
|
check_arity(terms.size(), 1);
|
||||||
|
|
|
||||||
405
src/opt/bcd2.cpp
405
src/opt/bcd2.cpp
|
|
@ -1,405 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
bcd2.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
bcd2 based MaxSAT.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-4-17
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include "bcd2.h"
|
|
||||||
#include "pb_decl_plugin.h"
|
|
||||||
#include "uint_set.h"
|
|
||||||
#include "ast_pp.h"
|
|
||||||
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
// ------------------------------------------------------
|
|
||||||
// Morgado, Heras, Marques-Silva 2013
|
|
||||||
// (initial version without model-based optimizations)
|
|
||||||
//
|
|
||||||
class bcd2 : public maxsmt_solver_base {
|
|
||||||
struct wcore {
|
|
||||||
expr* m_r;
|
|
||||||
unsigned_vector m_R;
|
|
||||||
rational m_lower;
|
|
||||||
rational m_mid;
|
|
||||||
rational m_upper;
|
|
||||||
};
|
|
||||||
typedef obj_hashtable<expr> expr_set;
|
|
||||||
|
|
||||||
pb_util pb;
|
|
||||||
expr_ref_vector m_soft_aux;
|
|
||||||
obj_map<expr, unsigned> m_relax2index; // expr |-> index
|
|
||||||
obj_map<expr, unsigned> m_soft2index; // expr |-> index
|
|
||||||
expr_ref_vector m_trail;
|
|
||||||
expr_ref_vector m_soft_constraints;
|
|
||||||
expr_set m_asm_set;
|
|
||||||
vector<wcore> m_cores;
|
|
||||||
vector<rational> m_sigmas;
|
|
||||||
rational m_den; // least common multiplier of original denominators
|
|
||||||
bool m_enable_lazy; // enable adding soft constraints lazily (called 'mgbcd2')
|
|
||||||
unsigned_vector m_lazy_soft; // soft constraints to add lazily.
|
|
||||||
|
|
||||||
void set2asms(expr_set const& set, expr_ref_vector & es) const {
|
|
||||||
es.reset();
|
|
||||||
expr_set::iterator it = set.begin(), end = set.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
es.push_back(m.mk_not(*it));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void bcd2_init_soft(weights_t& weights, expr_ref_vector const& soft) {
|
|
||||||
|
|
||||||
// normalize weights to be integral:
|
|
||||||
m_den = rational::one();
|
|
||||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
|
||||||
m_den = lcm(m_den, denominator(m_weights[i]));
|
|
||||||
}
|
|
||||||
if (!m_den.is_one()) {
|
|
||||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
|
||||||
m_weights[i] = m_den*m_weights[i];
|
|
||||||
SASSERT(m_weights[i].is_int());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void init_bcd() {
|
|
||||||
m_trail.reset();
|
|
||||||
m_asm_set.reset();
|
|
||||||
m_cores.reset();
|
|
||||||
m_sigmas.reset();
|
|
||||||
m_lazy_soft.reset();
|
|
||||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
|
||||||
m_sigmas.push_back(m_weights[i]);
|
|
||||||
m_soft_aux.push_back(mk_fresh());
|
|
||||||
if (m_enable_lazy) {
|
|
||||||
m_lazy_soft.push_back(i);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
enable_soft_constraint(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_upper += rational(1);
|
|
||||||
}
|
|
||||||
|
|
||||||
void process_sat() {
|
|
||||||
svector<bool> assignment;
|
|
||||||
update_assignment(assignment);
|
|
||||||
if (check_lazy_soft(assignment)) {
|
|
||||||
update_sigmas();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
public:
|
|
||||||
bcd2(maxsat_context& c,
|
|
||||||
weights_t& ws, expr_ref_vector const& soft):
|
|
||||||
maxsmt_solver_base(c, ws, soft),
|
|
||||||
pb(m),
|
|
||||||
m_soft_aux(m),
|
|
||||||
m_trail(m),
|
|
||||||
m_soft_constraints(m),
|
|
||||||
m_enable_lazy(true) {
|
|
||||||
bcd2_init_soft(ws, soft);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual ~bcd2() {}
|
|
||||||
|
|
||||||
virtual lbool operator()() {
|
|
||||||
expr_ref fml(m), r(m);
|
|
||||||
lbool is_sat = l_undef;
|
|
||||||
expr_ref_vector asms(m);
|
|
||||||
init();
|
|
||||||
init_bcd();
|
|
||||||
if (m.canceled()) {
|
|
||||||
normalize_bounds();
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
process_sat();
|
|
||||||
while (m_lower < m_upper) {
|
|
||||||
trace_bounds("bcd2");
|
|
||||||
assert_soft();
|
|
||||||
solver::scoped_push _scope2(s());
|
|
||||||
TRACE("opt", display(tout););
|
|
||||||
assert_cores();
|
|
||||||
set2asms(m_asm_set, asms);
|
|
||||||
if (m.canceled()) {
|
|
||||||
normalize_bounds();
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
is_sat = s().check_sat(asms.size(), asms.c_ptr());
|
|
||||||
switch(is_sat) {
|
|
||||||
case l_undef:
|
|
||||||
normalize_bounds();
|
|
||||||
return l_undef;
|
|
||||||
case l_true:
|
|
||||||
process_sat();
|
|
||||||
break;
|
|
||||||
case l_false: {
|
|
||||||
ptr_vector<expr> unsat_core;
|
|
||||||
uint_set subC, soft;
|
|
||||||
s().get_unsat_core(unsat_core);
|
|
||||||
core2indices(unsat_core, subC, soft);
|
|
||||||
SASSERT(unsat_core.size() == subC.num_elems() + soft.num_elems());
|
|
||||||
if (soft.num_elems() == 0 && subC.num_elems() == 1) {
|
|
||||||
unsigned s = *subC.begin();
|
|
||||||
wcore& c_s = m_cores[s];
|
|
||||||
c_s.m_lower = refine(c_s.m_R, c_s.m_mid);
|
|
||||||
c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2));
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
wcore c_s;
|
|
||||||
rational delta = min_of_delta(subC);
|
|
||||||
rational lower = sum_of_lower(subC);
|
|
||||||
union_Rs(subC, c_s.m_R);
|
|
||||||
r = mk_fresh();
|
|
||||||
relax(subC, soft, c_s.m_R, delta);
|
|
||||||
c_s.m_lower = refine(c_s.m_R, lower + delta - rational(1));
|
|
||||||
c_s.m_upper = rational::one();
|
|
||||||
c_s.m_upper += sum_of_sigmas(c_s.m_R);
|
|
||||||
c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2));
|
|
||||||
c_s.m_r = r;
|
|
||||||
m_asm_set.insert(r);
|
|
||||||
subtract(m_cores, subC);
|
|
||||||
m_relax2index.insert(r, m_cores.size());
|
|
||||||
m_cores.push_back(c_s);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_lower = compute_lower();
|
|
||||||
}
|
|
||||||
normalize_bounds();
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
private:
|
|
||||||
|
|
||||||
void enable_soft_constraint(unsigned i) {
|
|
||||||
expr_ref fml(m);
|
|
||||||
expr* r = m_soft_aux[i].get();
|
|
||||||
m_soft2index.insert(r, i);
|
|
||||||
fml = m.mk_or(r, m_soft[i]);
|
|
||||||
m_soft_constraints.push_back(fml);
|
|
||||||
m_asm_set.insert(r);
|
|
||||||
SASSERT(m_weights[i].is_int());
|
|
||||||
}
|
|
||||||
|
|
||||||
void assert_soft() {
|
|
||||||
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
|
|
||||||
s().assert_expr(m_soft_constraints[i].get());
|
|
||||||
}
|
|
||||||
m_soft_constraints.reset();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool check_lazy_soft(svector<bool> const& assignment) {
|
|
||||||
bool all_satisfied = true;
|
|
||||||
for (unsigned i = 0; i < m_lazy_soft.size(); ++i) {
|
|
||||||
unsigned j = m_lazy_soft[i];
|
|
||||||
if (!assignment[j]) {
|
|
||||||
enable_soft_constraint(j);
|
|
||||||
m_lazy_soft[i] = m_lazy_soft.back();
|
|
||||||
m_lazy_soft.pop_back();
|
|
||||||
--i;
|
|
||||||
all_satisfied = false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return all_satisfied;
|
|
||||||
}
|
|
||||||
|
|
||||||
void normalize_bounds() {
|
|
||||||
m_lower /= m_den;
|
|
||||||
m_upper /= m_den;
|
|
||||||
}
|
|
||||||
|
|
||||||
expr* mk_fresh() {
|
|
||||||
expr* r = mk_fresh_bool("r");
|
|
||||||
m_trail.push_back(r);
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
|
|
||||||
void update_assignment(svector<bool>& new_assignment) {
|
|
||||||
expr_ref val(m);
|
|
||||||
rational new_upper(0);
|
|
||||||
model_ref model;
|
|
||||||
new_assignment.reset();
|
|
||||||
s().get_model(model);
|
|
||||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
|
||||||
new_assignment.push_back(model->eval(m_soft[i], val) && m.is_true(val));
|
|
||||||
if (!new_assignment[i]) {
|
|
||||||
new_upper += m_weights[i];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (new_upper < m_upper) {
|
|
||||||
m_upper = new_upper;
|
|
||||||
m_model = model;
|
|
||||||
m_assignment.reset();
|
|
||||||
m_assignment.append(new_assignment);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void update_sigmas() {
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
wcore& c_i = m_cores[i];
|
|
||||||
unsigned_vector const& R = c_i.m_R;
|
|
||||||
c_i.m_upper.reset();
|
|
||||||
for (unsigned j = 0; j < R.size(); ++j) {
|
|
||||||
unsigned r_j = R[j];
|
|
||||||
if (!m_assignment[r_j]) {
|
|
||||||
c_i.m_upper += m_weights[r_j];
|
|
||||||
m_sigmas[r_j] = m_weights[r_j];
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_sigmas[r_j].reset();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
c_i.m_mid = div(c_i.m_lower + c_i.m_upper, rational(2));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Minimum of two (positive) numbers. Zero is treated as +infinity.
|
|
||||||
*/
|
|
||||||
rational min_z(rational const& a, rational const& b) {
|
|
||||||
if (a.is_zero()) return b;
|
|
||||||
if (b.is_zero()) return a;
|
|
||||||
if (a < b) return a;
|
|
||||||
return b;
|
|
||||||
}
|
|
||||||
|
|
||||||
rational min_of_delta(uint_set const& subC) {
|
|
||||||
rational delta(0);
|
|
||||||
for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) {
|
|
||||||
unsigned j = *it;
|
|
||||||
wcore const& core = m_cores[j];
|
|
||||||
rational new_delta = rational(1) + core.m_upper - core.m_mid;
|
|
||||||
SASSERT(new_delta.is_pos());
|
|
||||||
delta = min_z(delta, new_delta);
|
|
||||||
}
|
|
||||||
return delta;
|
|
||||||
}
|
|
||||||
|
|
||||||
rational sum_of_lower(uint_set const& subC) {
|
|
||||||
rational lower(0);
|
|
||||||
for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) {
|
|
||||||
lower += m_cores[*it].m_lower;
|
|
||||||
}
|
|
||||||
return lower;
|
|
||||||
}
|
|
||||||
|
|
||||||
rational sum_of_sigmas(unsigned_vector const& R) {
|
|
||||||
rational sum(0);
|
|
||||||
for (unsigned i = 0; i < R.size(); ++i) {
|
|
||||||
sum += m_sigmas[R[i]];
|
|
||||||
}
|
|
||||||
return sum;
|
|
||||||
}
|
|
||||||
void union_Rs(uint_set const& subC, unsigned_vector& R) {
|
|
||||||
for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) {
|
|
||||||
R.append(m_cores[*it].m_R);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
rational compute_lower() {
|
|
||||||
rational result(0);
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
result += m_cores[i].m_lower;
|
|
||||||
}
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
void subtract(vector<wcore>& cores, uint_set const& subC) {
|
|
||||||
unsigned j = 0;
|
|
||||||
for (unsigned i = 0; i < cores.size(); ++i) {
|
|
||||||
if (subC.contains(i)) {
|
|
||||||
m_asm_set.remove(cores[i].m_r);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
if (j != i) {
|
|
||||||
cores[j] = cores[i];
|
|
||||||
}
|
|
||||||
++j;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
cores.resize(j);
|
|
||||||
for (unsigned i = 0; i < cores.size(); ++i) {
|
|
||||||
m_relax2index.insert(cores[i].m_r, i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void core2indices(ptr_vector<expr> const& core, uint_set& subC, uint_set& soft) {
|
|
||||||
for (unsigned i = 0; i < core.size(); ++i) {
|
|
||||||
unsigned j;
|
|
||||||
expr* a;
|
|
||||||
VERIFY(m.is_not(core[i], a));
|
|
||||||
if (m_relax2index.find(a, j)) {
|
|
||||||
subC.insert(j);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
VERIFY(m_soft2index.find(a, j));
|
|
||||||
soft.insert(j);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
rational refine(unsigned_vector const& idx, rational v) {
|
|
||||||
return v + rational(1);
|
|
||||||
}
|
|
||||||
void relax(uint_set& subC, uint_set& soft, unsigned_vector& R, rational& delta) {
|
|
||||||
for (uint_set::iterator it = soft.begin(); it != soft.end(); ++it) {
|
|
||||||
R.push_back(*it);
|
|
||||||
delta = min_z(delta, m_weights[*it]);
|
|
||||||
m_asm_set.remove(m_soft_aux[*it].get());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void assert_cores() {
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
assert_core(m_cores[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
void assert_core(wcore const& core) {
|
|
||||||
expr_ref fml(m);
|
|
||||||
vector<rational> ws;
|
|
||||||
ptr_vector<expr> rs;
|
|
||||||
rational w(0);
|
|
||||||
for (unsigned j = 0; j < core.m_R.size(); ++j) {
|
|
||||||
unsigned idx = core.m_R[j];
|
|
||||||
ws.push_back(m_weights[idx]);
|
|
||||||
w += ws.back();
|
|
||||||
rs.push_back(m_soft_aux[idx].get());
|
|
||||||
}
|
|
||||||
w.neg();
|
|
||||||
w += core.m_mid;
|
|
||||||
ws.push_back(w);
|
|
||||||
rs.push_back(core.m_r);
|
|
||||||
fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid);
|
|
||||||
s().assert_expr(fml);
|
|
||||||
}
|
|
||||||
void display(std::ostream& out) {
|
|
||||||
out << "[" << m_lower << ":" << m_upper << "]\n";
|
|
||||||
s().display(out);
|
|
||||||
out << "\n";
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
wcore const& c = m_cores[i];
|
|
||||||
out << mk_pp(c.m_r, m) << ": ";
|
|
||||||
for (unsigned j = 0; j < c.m_R.size(); ++j) {
|
|
||||||
out << c.m_R[j] << " (" << m_sigmas[c.m_R[j]] << ") ";
|
|
||||||
}
|
|
||||||
out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n";
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
|
||||||
out << mk_pp(m_soft[i], m) << " " << m_weights[i] << "\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
maxsmt_solver_base* mk_bcd2(
|
|
||||||
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
|
|
||||||
return alloc(bcd2, c, ws, soft);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,28 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
bcd2.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Bcd2 based MaxSAT.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-4-17
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#ifndef BCD2_H_
|
|
||||||
#define BCD2_H_
|
|
||||||
|
|
||||||
#include "maxsmt.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
maxsmt_solver_base* mk_bcd2(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft);
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
@ -1,237 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2013 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
fu_malik.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
Fu & Malik built-in optimization method.
|
|
||||||
Adapted from sample code in C.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Anh-Dung Phan (t-anphan) 2013-10-15
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#include "fu_malik.h"
|
|
||||||
#include "qfbv_tactic.h"
|
|
||||||
#include "tactic2solver.h"
|
|
||||||
#include "goal.h"
|
|
||||||
#include "probe.h"
|
|
||||||
#include "tactic.h"
|
|
||||||
#include "ast_pp.h"
|
|
||||||
#include "model_smt2_pp.h"
|
|
||||||
#include "opt_context.h"
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
|
|
||||||
unsat core extraction and the at-most-one constraint.
|
|
||||||
|
|
||||||
Return the number of soft-constraints that can be
|
|
||||||
satisfied. Return -1 if the hard-constraints cannot be
|
|
||||||
satisfied. That is, the formula cannot be satisfied even if all
|
|
||||||
soft-constraints are ignored.
|
|
||||||
|
|
||||||
For more information on the Fu & Malik procedure:
|
|
||||||
|
|
||||||
Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International
|
|
||||||
Conference on Theory and Applications of Satisfiability Testing, 2006.
|
|
||||||
*/
|
|
||||||
namespace opt {
|
|
||||||
|
|
||||||
class fu_malik : public maxsmt_solver_base {
|
|
||||||
filter_model_converter& m_fm;
|
|
||||||
expr_ref_vector m_aux_soft;
|
|
||||||
expr_ref_vector m_aux;
|
|
||||||
model_ref m_model;
|
|
||||||
|
|
||||||
public:
|
|
||||||
fu_malik(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
|
|
||||||
maxsmt_solver_base(c, ws, soft),
|
|
||||||
m_fm(c.fm()),
|
|
||||||
m_aux_soft(soft),
|
|
||||||
m_aux(m)
|
|
||||||
{
|
|
||||||
m_upper = rational(m_aux_soft.size() + 1);
|
|
||||||
m_lower.reset();
|
|
||||||
m_assignment.resize(m_aux_soft.size(), false);
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief One step of the Fu&Malik algorithm.
|
|
||||||
|
|
||||||
Input: soft constraints + aux-vars (aka answer literals)
|
|
||||||
Output: done/not-done when not done return updated set of soft-constraints and aux-vars.
|
|
||||||
- if SAT --> terminates
|
|
||||||
- if UNSAT
|
|
||||||
* compute unsat core
|
|
||||||
* add blocking variable to soft-constraints in the core
|
|
||||||
- replace soft-constraint with the one with the blocking variable
|
|
||||||
- we should also add an aux-var
|
|
||||||
- replace aux-var with a new one
|
|
||||||
* add at-most-one constraint with blocking
|
|
||||||
*/
|
|
||||||
|
|
||||||
typedef obj_hashtable<expr> expr_set;
|
|
||||||
|
|
||||||
void set2vector(expr_set const& set, expr_ref_vector & es) const {
|
|
||||||
es.reset();
|
|
||||||
expr_set::iterator it = set.begin(), end = set.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
es.push_back(*it);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void collect_statistics(statistics& st) const {
|
|
||||||
st.update("opt-fm-num-steps", m_aux_soft.size() + 2 - m_upper.get_unsigned());
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
|
|
||||||
set.reset();
|
|
||||||
expr_set::iterator it = set1.begin(), end = set1.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
set.insert(*it);
|
|
||||||
}
|
|
||||||
it = set2.begin();
|
|
||||||
end = set2.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
set.insert(*it);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
lbool step() {
|
|
||||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_aux_soft.size() + 2 - m_upper.get_unsigned() << ")\n";);
|
|
||||||
expr_ref_vector assumptions(m), block_vars(m);
|
|
||||||
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
|
|
||||||
assumptions.push_back(m.mk_not(m_aux[i].get()));
|
|
||||||
}
|
|
||||||
lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr());
|
|
||||||
if (is_sat != l_false) {
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
|
|
||||||
ptr_vector<expr> core;
|
|
||||||
s().get_unsat_core(core);
|
|
||||||
|
|
||||||
SASSERT(!core.empty());
|
|
||||||
|
|
||||||
// Update soft-constraints and aux_vars
|
|
||||||
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
|
|
||||||
|
|
||||||
bool found = false;
|
|
||||||
for (unsigned j = 0; !found && j < core.size(); ++j) {
|
|
||||||
found = assumptions[i].get() == core[j];
|
|
||||||
}
|
|
||||||
if (!found) {
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
app_ref block_var(m), tmp(m);
|
|
||||||
block_var = m.mk_fresh_const("block_var", m.mk_bool_sort());
|
|
||||||
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
|
|
||||||
m_fm.insert(block_var->get_decl());
|
|
||||||
m_fm.insert(to_app(m_aux[i].get())->get_decl());
|
|
||||||
m_aux_soft[i] = m.mk_or(m_aux_soft[i].get(), block_var);
|
|
||||||
block_vars.push_back(block_var);
|
|
||||||
tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
|
|
||||||
s().assert_expr(tmp);
|
|
||||||
}
|
|
||||||
SASSERT (!block_vars.empty());
|
|
||||||
assert_at_most_one(block_vars);
|
|
||||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_aux_soft.size() - block_vars.size() << ")\n";);
|
|
||||||
return l_false;
|
|
||||||
}
|
|
||||||
|
|
||||||
void assert_at_most_one(expr_ref_vector const& block_vars) {
|
|
||||||
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& has_zero) {
|
|
||||||
SASSERT(n != 0);
|
|
||||||
if (n == 1) {
|
|
||||||
has_one = vars[0];
|
|
||||||
has_zero = m.mk_not(vars[0]);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
unsigned mid = n/2;
|
|
||||||
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: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
|
|
||||||
virtual lbool operator()() {
|
|
||||||
lbool is_sat = l_true;
|
|
||||||
if (m_aux_soft.empty()) {
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
solver::scoped_push _sp(s());
|
|
||||||
expr_ref tmp(m);
|
|
||||||
|
|
||||||
TRACE("opt",
|
|
||||||
tout << "soft constraints:\n";
|
|
||||||
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
|
|
||||||
tout << mk_pp(m_aux_soft[i].get(), m) << "\n";
|
|
||||||
});
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
|
|
||||||
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
|
|
||||||
m_fm.insert(to_app(m_aux.back())->get_decl());
|
|
||||||
tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
|
|
||||||
s().assert_expr(tmp);
|
|
||||||
}
|
|
||||||
|
|
||||||
do {
|
|
||||||
is_sat = step();
|
|
||||||
--m_upper;
|
|
||||||
}
|
|
||||||
while (is_sat == l_false);
|
|
||||||
|
|
||||||
if (is_sat == l_true) {
|
|
||||||
// Get a list satisfying m_aux_soft
|
|
||||||
s().get_model(m_model);
|
|
||||||
m_lower = m_upper;
|
|
||||||
m_assignment.reset();
|
|
||||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
|
||||||
expr_ref val(m);
|
|
||||||
if (!m_model->eval(m_soft[i], val)) return l_undef;
|
|
||||||
TRACE("opt", tout << val << "\n";);
|
|
||||||
m_assignment.push_back(m.is_true(val));
|
|
||||||
}
|
|
||||||
TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";
|
|
||||||
model_smt2_pp(tout, m, *m_model, 0););
|
|
||||||
}
|
|
||||||
// We are done and soft_constraints has
|
|
||||||
// been updated with the max-sat assignment.
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual void get_model(model_ref& mdl) {
|
|
||||||
mdl = m_model.get();
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual rational get_lower() const {
|
|
||||||
return rational(m_aux_soft.size())-m_upper;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual rational get_upper() const {
|
|
||||||
return rational(m_aux_soft.size())-m_lower;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
maxsmt_solver_base* mk_fu_malik(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft) {
|
|
||||||
return alloc(fu_malik, c, ws, soft);
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
@ -1,37 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2013 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
fu_malik.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Fu&Malik built-in optimization method.
|
|
||||||
Adapted from sample code in C.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Anh-Dung Phan (t-anphan) 2013-10-15
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
Takes solver with hard constraints added.
|
|
||||||
Returns a maximal satisfying subset of soft_constraints
|
|
||||||
that are still consistent with the solver state.
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#ifndef OPT_FU_MALIK_H_
|
|
||||||
#define OPT_FU_MALIK_H_
|
|
||||||
|
|
||||||
#include "opt_solver.h"
|
|
||||||
#include "maxsmt.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
|
|
||||||
maxsmt_solver_base* mk_fu_malik(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
|
|
||||||
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif
|
|
||||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,52 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
hitting_sets.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Hitting set approximations.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-06-06
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#ifndef HITTING_SETS_H_
|
|
||||||
#define HITTING_SETS_H_
|
|
||||||
|
|
||||||
#include "rational.h"
|
|
||||||
#include "statistics.h"
|
|
||||||
#include "lbool.h"
|
|
||||||
#include "rlimit.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
|
|
||||||
class hitting_sets {
|
|
||||||
struct imp;
|
|
||||||
imp* m_imp;
|
|
||||||
public:
|
|
||||||
hitting_sets(reslimit& lim);
|
|
||||||
~hitting_sets();
|
|
||||||
void add_weight(rational const& w);
|
|
||||||
void add_exists_true(unsigned sz, unsigned const* elems);
|
|
||||||
void add_exists_false(unsigned sz, unsigned const* elems);
|
|
||||||
lbool compute_lower();
|
|
||||||
lbool compute_upper();
|
|
||||||
void set_upper(rational const& r);
|
|
||||||
rational get_lower();
|
|
||||||
rational get_upper();
|
|
||||||
bool get_value(unsigned idx);
|
|
||||||
void set_cancel(bool f);
|
|
||||||
void collect_statistics(::statistics& st) const;
|
|
||||||
void reset();
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif
|
|
||||||
|
|
@ -1,556 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
maxhs.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
maxhs based MaxSAT.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-4-17
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include "optsmt.h"
|
|
||||||
#include "hitting_sets.h"
|
|
||||||
#include "stopwatch.h"
|
|
||||||
#include "ast_pp.h"
|
|
||||||
#include "model_smt2_pp.h"
|
|
||||||
#include "uint_set.h"
|
|
||||||
#include "maxhs.h"
|
|
||||||
#include "opt_context.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
|
|
||||||
class scoped_stopwatch {
|
|
||||||
double& m_time;
|
|
||||||
stopwatch m_watch;
|
|
||||||
public:
|
|
||||||
scoped_stopwatch(double& time): m_time(time) {
|
|
||||||
m_watch.start();
|
|
||||||
}
|
|
||||||
~scoped_stopwatch() {
|
|
||||||
m_watch.stop();
|
|
||||||
m_time += m_watch.get_seconds();
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
// ----------------------------------
|
|
||||||
// MaxSatHS+MSS
|
|
||||||
// variant of MaxSAT-HS (Algorithm 9)
|
|
||||||
// that also refines upper bound during progressive calls
|
|
||||||
// to the underlying optimization solver for the soft constraints.
|
|
||||||
//
|
|
||||||
|
|
||||||
class maxhs : public maxsmt_solver_base {
|
|
||||||
struct stats {
|
|
||||||
stats() { reset(); }
|
|
||||||
void reset() { memset(this, 0, sizeof(*this)); }
|
|
||||||
unsigned m_num_iterations;
|
|
||||||
unsigned m_num_core_reductions_success;
|
|
||||||
unsigned m_num_core_reductions_failure;
|
|
||||||
unsigned m_num_model_expansions_success;
|
|
||||||
unsigned m_num_model_expansions_failure;
|
|
||||||
double m_core_reduction_time;
|
|
||||||
double m_model_expansion_time;
|
|
||||||
double m_aux_sat_time;
|
|
||||||
double m_disjoint_cores_time;
|
|
||||||
};
|
|
||||||
|
|
||||||
hitting_sets m_hs;
|
|
||||||
expr_ref_vector m_aux; // auxiliary (indicator) variables.
|
|
||||||
obj_map<expr, unsigned> m_aux2index; // expr |-> index
|
|
||||||
unsigned_vector m_core_activity; // number of times soft constraint is used in a core.
|
|
||||||
svector<bool> m_seed; // clause selected in current model.
|
|
||||||
svector<bool> m_aux_active; // active soft clauses.
|
|
||||||
ptr_vector<expr> m_asms; // assumptions (over aux)
|
|
||||||
stats m_stats;
|
|
||||||
bool m_at_lower_bound;
|
|
||||||
|
|
||||||
|
|
||||||
public:
|
|
||||||
maxhs(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
|
|
||||||
maxsmt_solver_base(c, ws, soft),
|
|
||||||
m_hs(m.limit()),
|
|
||||||
m_aux(m),
|
|
||||||
m_at_lower_bound(false) {
|
|
||||||
}
|
|
||||||
virtual ~maxhs() {}
|
|
||||||
|
|
||||||
virtual void collect_statistics(statistics& st) const {
|
|
||||||
maxsmt_solver_base::collect_statistics(st);
|
|
||||||
m_hs.collect_statistics(st);
|
|
||||||
st.update("maxhs-num-iterations", m_stats.m_num_iterations);
|
|
||||||
st.update("maxhs-num-core-reductions-n", m_stats.m_num_core_reductions_failure);
|
|
||||||
st.update("maxhs-num-core-reductions-y", m_stats.m_num_core_reductions_success);
|
|
||||||
st.update("maxhs-num-model-expansions-n", m_stats.m_num_model_expansions_failure);
|
|
||||||
st.update("maxhs-num-model-expansions-y", m_stats.m_num_model_expansions_success);
|
|
||||||
st.update("maxhs-core-reduction-time", m_stats.m_core_reduction_time);
|
|
||||||
st.update("maxhs-model-expansion-time", m_stats.m_model_expansion_time);
|
|
||||||
st.update("maxhs-aux-sat-time", m_stats.m_aux_sat_time);
|
|
||||||
st.update("maxhs-disj-core-time", m_stats.m_disjoint_cores_time);
|
|
||||||
}
|
|
||||||
|
|
||||||
lbool operator()() {
|
|
||||||
ptr_vector<expr> hs;
|
|
||||||
init();
|
|
||||||
init_local();
|
|
||||||
if (!disjoint_cores(hs)) {
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
seed2assumptions();
|
|
||||||
while (m_lower < m_upper) {
|
|
||||||
++m_stats.m_num_iterations;
|
|
||||||
trace_bounds("maxhs");
|
|
||||||
TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
|
|
||||||
if (m.canceled()) {
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
|
|
||||||
lbool core_found = generate_cores(hs);
|
|
||||||
switch(core_found) {
|
|
||||||
case l_undef:
|
|
||||||
return l_undef;
|
|
||||||
case l_true: {
|
|
||||||
lbool is_sat = next_seed();
|
|
||||||
switch(is_sat) {
|
|
||||||
case l_true:
|
|
||||||
seed2hs(false, hs);
|
|
||||||
break;
|
|
||||||
case l_false:
|
|
||||||
TRACE("opt", tout << "no more seeds\n";);
|
|
||||||
IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-seeds)\n";);
|
|
||||||
m_lower = m_upper;
|
|
||||||
return l_true;
|
|
||||||
case l_undef:
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
case l_false:
|
|
||||||
IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-cores)\n";);
|
|
||||||
TRACE("opt", tout << "no more cores\n";);
|
|
||||||
m_lower = m_upper;
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
|
|
||||||
unsigned num_soft() const { return m_soft.size(); }
|
|
||||||
|
|
||||||
void init_local() {
|
|
||||||
unsigned sz = num_soft();
|
|
||||||
app_ref fml(m), obj(m);
|
|
||||||
expr_ref_vector sum(m);
|
|
||||||
m_asms.reset();
|
|
||||||
m_seed.reset();
|
|
||||||
m_aux.reset();
|
|
||||||
m_aux_active.reset();
|
|
||||||
m_aux2index.reset();
|
|
||||||
m_core_activity.reset();
|
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
|
||||||
bool tt = is_true(m_model, m_soft[i]);
|
|
||||||
m_seed.push_back(tt);
|
|
||||||
m_aux. push_back(mk_fresh(m.mk_bool_sort()));
|
|
||||||
m_aux_active.push_back(false);
|
|
||||||
m_core_activity.push_back(0);
|
|
||||||
m_aux2index.insert(m_aux.back(), i);
|
|
||||||
if (tt) {
|
|
||||||
m_asms.push_back(m_aux.back());
|
|
||||||
ensure_active(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
|
||||||
m_hs.add_weight(m_weights[i]);
|
|
||||||
}
|
|
||||||
TRACE("opt", print_seed(tout););
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void hs2seed(ptr_vector<expr> const& hs) {
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
m_seed[i] = true;
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < hs.size(); ++i) {
|
|
||||||
m_seed[m_aux2index.find(hs[i])] = false;
|
|
||||||
}
|
|
||||||
TRACE("opt",
|
|
||||||
print_asms(tout << "hitting set: ", hs);
|
|
||||||
print_seed(tout););
|
|
||||||
}
|
|
||||||
|
|
||||||
void seed2hs(bool pos, ptr_vector<expr>& hs) {
|
|
||||||
hs.reset();
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (pos == m_seed[i]) {
|
|
||||||
hs.push_back(m_aux[i].get());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
TRACE("opt",
|
|
||||||
print_asms(tout << "hitting set: ", hs);
|
|
||||||
print_seed(tout););
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
void seed2assumptions() {
|
|
||||||
seed2hs(true, m_asms);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
//
|
|
||||||
// Find disjoint cores for soft constraints.
|
|
||||||
//
|
|
||||||
bool disjoint_cores(ptr_vector<expr>& hs) {
|
|
||||||
scoped_stopwatch _sw(m_stats.m_disjoint_cores_time);
|
|
||||||
m_asms.reset();
|
|
||||||
svector<bool> active(num_soft(), true);
|
|
||||||
rational lower(0);
|
|
||||||
update_assumptions(active, lower, hs);
|
|
||||||
SASSERT(lower.is_zero());
|
|
||||||
while (true) {
|
|
||||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
|
||||||
switch (is_sat) {
|
|
||||||
case l_true:
|
|
||||||
if (lower > m_lower) {
|
|
||||||
m_lower = lower;
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
case l_false:
|
|
||||||
if (!shrink()) return false;
|
|
||||||
block_up();
|
|
||||||
update_assumptions(active, lower, hs);
|
|
||||||
break;
|
|
||||||
case l_undef:
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void update_assumptions(svector<bool>& active, rational& lower, ptr_vector<expr>& hs) {
|
|
||||||
rational arg_min(0);
|
|
||||||
expr* e = 0;
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
unsigned index = m_aux2index.find(m_asms[i]);
|
|
||||||
active[index] = false;
|
|
||||||
if (arg_min.is_zero() || arg_min > m_weights[index]) {
|
|
||||||
arg_min = m_weights[index];
|
|
||||||
e = m_asms[i];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (e) {
|
|
||||||
hs.push_back(e);
|
|
||||||
lower += arg_min;
|
|
||||||
}
|
|
||||||
m_asms.reset();
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (active[i]) {
|
|
||||||
m_asms.push_back(m_aux[i].get());
|
|
||||||
ensure_active(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// Auxiliary Algorithm 10 for producing cores.
|
|
||||||
//
|
|
||||||
lbool generate_cores(ptr_vector<expr>& hs) {
|
|
||||||
bool core = !m_at_lower_bound;
|
|
||||||
while (true) {
|
|
||||||
hs2seed(hs);
|
|
||||||
lbool is_sat = check_subset();
|
|
||||||
switch(is_sat) {
|
|
||||||
case l_undef:
|
|
||||||
return l_undef;
|
|
||||||
case l_true:
|
|
||||||
if (!grow()) return l_undef;
|
|
||||||
block_down();
|
|
||||||
return core?l_true:l_false;
|
|
||||||
case l_false:
|
|
||||||
core = true;
|
|
||||||
if (!shrink()) return l_undef;
|
|
||||||
block_up();
|
|
||||||
find_non_optimal_hitting_set(hs);
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
struct lt_activity {
|
|
||||||
maxhs& hs;
|
|
||||||
lt_activity(maxhs& hs):hs(hs) {}
|
|
||||||
bool operator()(expr* a, expr* b) const {
|
|
||||||
unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)];
|
|
||||||
unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)];
|
|
||||||
return w1 < w2;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
//
|
|
||||||
// produce the non-optimal hitting set by using the 10% heuristic.
|
|
||||||
// of most active cores constraints.
|
|
||||||
// m_asms contains the current core.
|
|
||||||
//
|
|
||||||
void find_non_optimal_hitting_set(ptr_vector<expr>& hs) {
|
|
||||||
std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this));
|
|
||||||
for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) {
|
|
||||||
--i;
|
|
||||||
hs.push_back(m_asms[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// retrieve the next seed that satisfies state of hs.
|
|
||||||
// state of hs must be satisfiable before optimization is called.
|
|
||||||
//
|
|
||||||
lbool next_seed() {
|
|
||||||
scoped_stopwatch _sw(m_stats.m_aux_sat_time);
|
|
||||||
TRACE("opt", tout << "\n";);
|
|
||||||
|
|
||||||
// min c_i*(not x_i) for x_i are soft clauses.
|
|
||||||
// max c_i*x_i for x_i are soft clauses
|
|
||||||
|
|
||||||
m_at_lower_bound = false;
|
|
||||||
|
|
||||||
lbool is_sat = m_hs.compute_upper();
|
|
||||||
|
|
||||||
if (is_sat == l_true) {
|
|
||||||
is_sat = m_hs.compute_lower();
|
|
||||||
}
|
|
||||||
if (is_sat == l_true) {
|
|
||||||
m_at_lower_bound = m_hs.get_upper() == m_hs.get_lower();
|
|
||||||
if (m_hs.get_lower() > m_lower) {
|
|
||||||
m_lower = m_hs.get_lower();
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
m_seed[i] = is_active(i) && !m_hs.get_value(i);
|
|
||||||
}
|
|
||||||
TRACE("opt", print_seed(tout););
|
|
||||||
}
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// check assignment returned by HS with the original
|
|
||||||
// hard constraints.
|
|
||||||
//
|
|
||||||
lbool check_subset() {
|
|
||||||
TRACE("opt", tout << "\n";);
|
|
||||||
m_asms.reset();
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (m_seed[i]) {
|
|
||||||
m_asms.push_back(m_aux[i].get());
|
|
||||||
ensure_active(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return s().check_sat(m_asms.size(), m_asms.c_ptr());
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// extend the current assignment to one that
|
|
||||||
// satisfies as many soft constraints as possible.
|
|
||||||
// update the upper bound based on this assignment
|
|
||||||
//
|
|
||||||
bool grow() {
|
|
||||||
scoped_stopwatch _sw(m_stats.m_model_expansion_time);
|
|
||||||
model_ref mdl;
|
|
||||||
s().get_model(mdl);
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
ensure_active(i);
|
|
||||||
m_seed[i] = false;
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
m_seed[m_aux2index.find(m_asms[i])] = true;
|
|
||||||
}
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (m_seed[i]) {
|
|
||||||
// already an assumption
|
|
||||||
}
|
|
||||||
else if (is_true(mdl, m_soft[i])) {
|
|
||||||
m_seed[i] = true;
|
|
||||||
m_asms.push_back(m_aux[i].get());
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_asms.push_back(m_aux[i].get());
|
|
||||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
|
||||||
switch(is_sat) {
|
|
||||||
case l_undef:
|
|
||||||
return false;
|
|
||||||
case l_false:
|
|
||||||
++m_stats.m_num_model_expansions_failure;
|
|
||||||
m_asms.pop_back();
|
|
||||||
break;
|
|
||||||
case l_true:
|
|
||||||
++m_stats.m_num_model_expansions_success;
|
|
||||||
s().get_model(mdl);
|
|
||||||
m_seed[i] = true;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
rational upper(0);
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (!m_seed[i]) {
|
|
||||||
upper += m_weights[i];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (upper < m_upper) {
|
|
||||||
m_upper = upper;
|
|
||||||
m_hs.set_upper(upper);
|
|
||||||
m_model = mdl;
|
|
||||||
m_assignment.reset();
|
|
||||||
m_assignment.append(m_seed);
|
|
||||||
TRACE("opt",
|
|
||||||
tout << "new upper: " << m_upper << "\n";
|
|
||||||
model_smt2_pp(tout, m, *(mdl.get()), 0););
|
|
||||||
}
|
|
||||||
DEBUG_CODE(
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
SASSERT(is_true(mdl, m_soft[i]) == m_seed[i]);
|
|
||||||
});
|
|
||||||
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// remove soft constraints from the current core.
|
|
||||||
//
|
|
||||||
bool shrink() {
|
|
||||||
scoped_stopwatch _sw(m_stats.m_core_reduction_time);
|
|
||||||
m_asms.reset();
|
|
||||||
s().get_unsat_core(m_asms);
|
|
||||||
TRACE("opt", print_asms(tout, m_asms););
|
|
||||||
obj_map<expr, unsigned> asm2index;
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
asm2index.insert(m_asms[i], i);
|
|
||||||
}
|
|
||||||
obj_map<expr, unsigned>::iterator it = asm2index.begin(), end = asm2index.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
unsigned i = it->m_value;
|
|
||||||
if (i < m_asms.size()) {
|
|
||||||
expr* tmp = m_asms[i];
|
|
||||||
expr* back = m_asms.back();
|
|
||||||
m_asms[i] = back;
|
|
||||||
m_asms.pop_back();
|
|
||||||
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
|
|
||||||
TRACE("opt", tout << "checking: " << mk_pp(tmp, m) << ": " << is_sat << "\n";);
|
|
||||||
switch(is_sat) {
|
|
||||||
case l_true:
|
|
||||||
++m_stats.m_num_core_reductions_failure;
|
|
||||||
// put back literal into core
|
|
||||||
m_asms.push_back(back);
|
|
||||||
m_asms[i] = tmp;
|
|
||||||
break;
|
|
||||||
case l_false:
|
|
||||||
// update the core
|
|
||||||
m_asms.reset();
|
|
||||||
++m_stats.m_num_core_reductions_success;
|
|
||||||
s().get_unsat_core(m_asms);
|
|
||||||
TRACE("opt", print_asms(tout, m_asms););
|
|
||||||
update_index(asm2index);
|
|
||||||
break;
|
|
||||||
case l_undef:
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void print_asms(std::ostream& out, ptr_vector<expr> const& asms) {
|
|
||||||
for (unsigned j = 0; j < asms.size(); ++j) {
|
|
||||||
out << mk_pp(asms[j], m) << " ";
|
|
||||||
}
|
|
||||||
out << "\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
void print_seed(std::ostream& out) {
|
|
||||||
out << "seed: ";
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
out << (m_seed[i]?"1":"0");
|
|
||||||
}
|
|
||||||
out << "\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// must include some literal not from asms.
|
|
||||||
// (furthermore, update upper bound constraint in HS)
|
|
||||||
//
|
|
||||||
void block_down() {
|
|
||||||
uint_set indices;
|
|
||||||
unsigned_vector c_indices;
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
indices.insert(m_aux2index.find(m_asms[i]));
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < num_soft(); ++i) {
|
|
||||||
if (!indices.contains(i)) {
|
|
||||||
c_indices.push_back(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_hs.add_exists_false(c_indices.size(), c_indices.c_ptr());
|
|
||||||
}
|
|
||||||
|
|
||||||
// should exclude some literal from core.
|
|
||||||
void block_up() {
|
|
||||||
unsigned_vector indices;
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
unsigned index = m_aux2index.find(m_asms[i]);
|
|
||||||
m_core_activity[index]++;
|
|
||||||
indices.push_back(index);
|
|
||||||
}
|
|
||||||
m_hs.add_exists_true(indices.size(), indices.c_ptr());
|
|
||||||
}
|
|
||||||
|
|
||||||
void update_index(obj_map<expr, unsigned>& asm2index) {
|
|
||||||
obj_map<expr, unsigned>::iterator it = asm2index.begin(), end = asm2index.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
it->m_value = UINT_MAX;
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
|
||||||
asm2index.find(m_asms[i]) = i;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
app_ref mk_fresh(sort* s) {
|
|
||||||
app_ref r(m);
|
|
||||||
r = m.mk_fresh_const("r", s);
|
|
||||||
m_c.fm().insert(r->get_decl());
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_true(model_ref& mdl, expr* e) {
|
|
||||||
expr_ref val(m);
|
|
||||||
return mdl->eval(e, val) && m.is_true(val);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_active(unsigned i) const {
|
|
||||||
return m_aux_active[i];
|
|
||||||
}
|
|
||||||
|
|
||||||
void ensure_active(unsigned i) {
|
|
||||||
if (!is_active(i)) {
|
|
||||||
expr_ref fml(m);
|
|
||||||
fml = m.mk_implies(m_aux[i].get(), m_soft[i]);
|
|
||||||
s().assert_expr(fml);
|
|
||||||
m_aux_active[i] = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
maxsmt_solver_base* mk_maxhs(
|
|
||||||
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
|
|
||||||
return alloc(maxhs, c, ws, soft);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,29 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
maxhs.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
HS-max based MaxSAT.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-4-17
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#ifndef HS_MAX_H_
|
|
||||||
#define HS_MAX_H_
|
|
||||||
|
|
||||||
#include "maxsmt.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
maxsmt_solver_base* mk_maxhs(maxsat_context& c,
|
|
||||||
weights_t& ws, expr_ref_vector const& soft);
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
@ -19,10 +19,7 @@ Notes:
|
||||||
|
|
||||||
#include <typeinfo>
|
#include <typeinfo>
|
||||||
#include "maxsmt.h"
|
#include "maxsmt.h"
|
||||||
#include "fu_malik.h"
|
|
||||||
#include "maxres.h"
|
#include "maxres.h"
|
||||||
#include "maxhs.h"
|
|
||||||
#include "bcd2.h"
|
|
||||||
#include "wmax.h"
|
#include "wmax.h"
|
||||||
#include "maxsls.h"
|
#include "maxsls.h"
|
||||||
#include "ast_pp.h"
|
#include "ast_pp.h"
|
||||||
|
|
@ -166,19 +163,10 @@ namespace opt {
|
||||||
else if (maxsat_engine == symbol("pd-maxres")) {
|
else if (maxsat_engine == symbol("pd-maxres")) {
|
||||||
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
|
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
|
||||||
}
|
}
|
||||||
else if (maxsat_engine == symbol("bcd2")) {
|
|
||||||
m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
|
|
||||||
}
|
|
||||||
else if (maxsat_engine == symbol("maxhs")) {
|
|
||||||
m_msolver = mk_maxhs(m_c, m_weights, m_soft_constraints);
|
|
||||||
}
|
|
||||||
else if (maxsat_engine == symbol("sls")) {
|
else if (maxsat_engine == symbol("sls")) {
|
||||||
// NB: this is experimental one-round version of SLS
|
// NB: this is experimental one-round version of SLS
|
||||||
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
|
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
|
||||||
}
|
}
|
||||||
else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) {
|
|
||||||
m_msolver = mk_fu_malik(m_c, m_weights, m_soft_constraints);
|
|
||||||
}
|
|
||||||
else {
|
else {
|
||||||
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
|
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
|
||||||
warning_msg("solver %s is not recognized, using default 'wmax'",
|
warning_msg("solver %s is not recognized, using default 'wmax'",
|
||||||
|
|
|
||||||
|
|
@ -2,7 +2,7 @@ def_module_params('opt',
|
||||||
description='optimization parameters',
|
description='optimization parameters',
|
||||||
export=True,
|
export=True,
|
||||||
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
|
params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
|
||||||
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'pd-maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"),
|
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'sls'"),
|
||||||
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
|
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
|
||||||
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
|
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
|
||||||
('print_model', BOOL, False, 'display model for satisfiable constraints'),
|
('print_model', BOOL, False, 'display model for satisfiable constraints'),
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue