mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 10:52:02 +00:00
use approximate hitting set implementation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
960e8ea1d5
commit
5427964c54
15 changed files with 273 additions and 156 deletions
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
#include "simplex.h"
|
||||
#include "sparse_matrix_def.h"
|
||||
#include "simplex_def.h"
|
||||
#include "sat_solver.h"
|
||||
|
||||
typedef simplex::simplex<simplex::mpz_ext> Simplex;
|
||||
typedef simplex::sparse_matrix<simplex::mpz_ext> sparse_matrix;
|
||||
|
|
@ -38,15 +39,26 @@ namespace opt {
|
|||
rational m_max_weight;
|
||||
rational m_denominator;
|
||||
vector<set> m_S;
|
||||
vector<set> m_T;
|
||||
svector<lbool> m_value;
|
||||
svector<lbool> m_value_saved;
|
||||
unsigned_vector m_value_trail;
|
||||
unsigned_vector m_value_lim;
|
||||
vector<unsigned_vector> m_use_list;
|
||||
vector<unsigned_vector> m_tuse_list;
|
||||
vector<unsigned_vector> m_fuse_list;
|
||||
unsynch_mpz_manager m;
|
||||
Simplex m_simplex;
|
||||
unsigned m_weights_var;
|
||||
|
||||
imp():m_cancel(false) {}
|
||||
params_ref m_params;
|
||||
sat::solver m_solver;
|
||||
svector<sat::bool_var> m_vars;
|
||||
|
||||
imp():
|
||||
m_cancel(false),
|
||||
m_max_weight(0),
|
||||
m_weights_var(0),
|
||||
m_solver(m_params,0) {}
|
||||
~imp() {}
|
||||
|
||||
void add_weight(rational const& w) {
|
||||
|
|
@ -57,28 +69,56 @@ namespace opt {
|
|||
m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0)));
|
||||
m_weights.push_back(w);
|
||||
m_value.push_back(l_undef);
|
||||
m_use_list.push_back(unsigned_vector());
|
||||
m_tuse_list.push_back(unsigned_vector());
|
||||
m_fuse_list.push_back(unsigned_vector());
|
||||
m_max_weight += w;
|
||||
m_vars.push_back(m_solver.mk_var());
|
||||
}
|
||||
|
||||
void add_set(unsigned sz, unsigned const* S) {
|
||||
if (sz == 0) {
|
||||
return;
|
||||
}
|
||||
void add_exists_false(unsigned sz, unsigned const* S) {
|
||||
SASSERT(sz > 0);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
m_use_list[S[i]].push_back(m_S.size());
|
||||
m_fuse_list[S[i]].push_back(m_T.size());
|
||||
}
|
||||
init_weights();
|
||||
m_T.push_back(unsigned_vector(sz, S));
|
||||
add_simplex_row(false, sz, S);
|
||||
// Add clause to SAT solver:
|
||||
svector<sat::literal> lits;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
lits.push_back(sat::literal(m_vars[S[i]], true));
|
||||
}
|
||||
m_solver.mk_clause(lits.size(), lits.c_ptr());
|
||||
}
|
||||
|
||||
void add_exists_true(unsigned sz, unsigned const* S) {
|
||||
SASSERT(sz > 0);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
m_tuse_list[S[i]].push_back(m_S.size());
|
||||
}
|
||||
init_weights();
|
||||
m_S.push_back(unsigned_vector(sz, S));
|
||||
add_simplex_row(sz, S);
|
||||
add_simplex_row(true, sz, S);
|
||||
|
||||
// Add clause to SAT solver
|
||||
svector<sat::literal> lits;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
lits.push_back(sat::literal(m_vars[S[i]], false));
|
||||
}
|
||||
m_solver.mk_clause(lits.size(), lits.c_ptr());
|
||||
}
|
||||
|
||||
bool compute_lower() {
|
||||
lbool compute_lower() {
|
||||
m_lower.reset();
|
||||
return L1() && L2() && L3();
|
||||
if (L1() && L2() && L3()) {
|
||||
return l_true;
|
||||
}
|
||||
else {
|
||||
return l_undef;
|
||||
}
|
||||
}
|
||||
|
||||
bool compute_upper() {
|
||||
lbool compute_upper() {
|
||||
m_upper = m_max_weight;
|
||||
return U1();
|
||||
}
|
||||
|
|
@ -91,18 +131,30 @@ namespace opt {
|
|||
return m_upper/m_denominator;
|
||||
}
|
||||
|
||||
void set_upper(rational const& r) {
|
||||
m_max_weight = r;
|
||||
}
|
||||
|
||||
bool get_value(unsigned idx) {
|
||||
return
|
||||
idx < m_value_saved.size() &&
|
||||
m_value_saved[idx] == l_true;
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
m_simplex.set_cancel(f);
|
||||
m_solver.set_cancel(f);
|
||||
}
|
||||
|
||||
void collect_statistics(::statistics& st) const {
|
||||
m_simplex.collect_statistics(st);
|
||||
m_solver.collect_statistics(st);
|
||||
}
|
||||
|
||||
void reset() {
|
||||
m_lower.reset();
|
||||
m_upper = m_max_weight;
|
||||
m_upper = m_max_weight;
|
||||
}
|
||||
|
||||
void init_weights() {
|
||||
|
|
@ -135,6 +187,25 @@ namespace opt {
|
|||
m_simplex.add_row(m_weights_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
|
||||
}
|
||||
|
||||
void display(std::ostream& out) const {
|
||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
||||
out << i << ": " << m_value_saved[i]<< " " << m_weights[i] << "\n";
|
||||
}
|
||||
for (unsigned i = 0; i < m_S.size(); ++i) {
|
||||
display(out << "+ ", m_S[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < m_T.size(); ++i) {
|
||||
display(out << "- ", m_T[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void display(std::ostream& out, set const& S) const {
|
||||
for (unsigned i = 0; i < S.size(); ++i) {
|
||||
out << S[i] << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
struct scoped_select {
|
||||
imp& s;
|
||||
unsigned sz;
|
||||
|
|
@ -164,9 +235,67 @@ namespace opt {
|
|||
}
|
||||
};
|
||||
|
||||
lbool U1() {
|
||||
scoped_select _sc(*this);
|
||||
while (true) {
|
||||
if (!compute_U1()) return l_undef;
|
||||
unsigned i = 0, j = 0;
|
||||
set_undef_to_false();
|
||||
if (values_satisfy_Ts(i)) {
|
||||
return l_true;
|
||||
}
|
||||
|
||||
//
|
||||
// pick some unsatisfied clause from m_T,
|
||||
// and set the value of the most expensive
|
||||
// literal to true.
|
||||
//
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << "\n";);
|
||||
set const& T = m_T[i];
|
||||
rational max_value(0);
|
||||
j = 0;
|
||||
for (i = 0; i < T.size(); ++i) {
|
||||
SASSERT(m_value_saved[T[i]] == l_true);
|
||||
if (max_value < m_weights[T[i]]) {
|
||||
max_value = m_weights[T[i]];
|
||||
j = T[i];
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(hs.unselect " << j << ")\n";);
|
||||
unselect(j);
|
||||
for (i = 0; i < m_S.size(); ++i) {
|
||||
set const& S = m_S[i];
|
||||
for (j = 0; j < S.size(); ++j) {
|
||||
if (l_false != selected(S[j])) break;
|
||||
}
|
||||
if (j == S.size()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "approximation failed, fall back to SAT\n";);
|
||||
return compute_U2();
|
||||
}
|
||||
}
|
||||
TRACE("opt", display(tout););
|
||||
}
|
||||
}
|
||||
|
||||
lbool compute_U2() {
|
||||
lbool is_sat = m_solver.check();
|
||||
if (is_sat == l_true) {
|
||||
sat::model const& model = m_solver.get_model();
|
||||
m_value_saved.reset();
|
||||
m_upper.reset();
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
m_value_saved.push_back(model[m_vars[i]]);
|
||||
if (model[m_vars[i]] == l_true) {
|
||||
m_upper += m_weights[i];
|
||||
}
|
||||
}
|
||||
}
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
// compute upper bound for hitting set.
|
||||
bool U1() {
|
||||
bool compute_U1() {
|
||||
rational w(0);
|
||||
scoped_select _sc(*this);
|
||||
|
||||
|
|
@ -177,7 +306,7 @@ namespace opt {
|
|||
|
||||
//
|
||||
// Sort indices.
|
||||
// The least literals are those where -score/w is minimized.
|
||||
// The least literals are those where score/w is maximized.
|
||||
//
|
||||
unsigned_vector indices;
|
||||
for (unsigned i = 0; i < m_value.size(); ++i) {
|
||||
|
|
@ -194,8 +323,11 @@ namespace opt {
|
|||
select(idx);
|
||||
w += m_weights[idx];
|
||||
}
|
||||
if (w < m_upper) {
|
||||
m_upper = w;
|
||||
m_upper = w;
|
||||
m_value_saved.reset();
|
||||
m_value_saved.append(m_value);
|
||||
if (m_upper > m_max_weight) {
|
||||
IF_VERBOSE(0, verbose_stream() << "got worse upper bound\n";);
|
||||
}
|
||||
return !m_cancel;
|
||||
}
|
||||
|
|
@ -209,19 +341,23 @@ namespace opt {
|
|||
set const& S = m_S[i];
|
||||
if (!has_selected(S)) {
|
||||
for (unsigned j = 0; j < S.size(); ++j) {
|
||||
scores[S[j]]++;
|
||||
if (selected(S[j]) != l_false) {
|
||||
scores[S[j]]++;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void update_scores(unsigned_vector& scores, unsigned v) {
|
||||
unsigned_vector const& v_uses = m_use_list[v];
|
||||
unsigned_vector const& v_uses = m_tuse_list[v];
|
||||
for (unsigned i = 0; i < v_uses.size(); ++i) {
|
||||
set const& S = m_S[v_uses[i]];
|
||||
if (!has_selected(S)) {
|
||||
for (unsigned j = 0; j < S.size(); ++j) {
|
||||
--scores[S[j]];
|
||||
if (selected(S[j]) != l_false) {
|
||||
--scores[S[j]];
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -300,20 +436,26 @@ namespace opt {
|
|||
return true;
|
||||
}
|
||||
|
||||
void add_simplex_row(unsigned sz, unsigned const* S) {
|
||||
void add_simplex_row(bool is_some_true, unsigned sz, unsigned const* S) {
|
||||
unsigned_vector vars;
|
||||
scoped_mpz_vector coeffs(m);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
vars.push_back(S[i]);
|
||||
coeffs.push_back(mpz(1));
|
||||
}
|
||||
unsigned base_var = m_S.size() + m_weights.size();
|
||||
unsigned base_var = m_T.size() + m_S.size() + m_weights.size();
|
||||
m_simplex.ensure_var(base_var);
|
||||
vars.push_back(base_var);
|
||||
coeffs.push_back(mpz(-1));
|
||||
// S - base_var = 0
|
||||
// base_var >= 1
|
||||
m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0)));
|
||||
if (is_some_true) {
|
||||
// base_var >= 1
|
||||
m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0)));
|
||||
}
|
||||
else {
|
||||
// base_var <= sz-1
|
||||
m_simplex.set_upper(base_var, mpq_inf(mpq(sz-1),mpq(0)));
|
||||
}
|
||||
m_simplex.add_row(base_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
|
||||
}
|
||||
|
||||
|
|
@ -334,7 +476,6 @@ namespace opt {
|
|||
return result;
|
||||
}
|
||||
|
||||
|
||||
lbool selected(unsigned j) const {
|
||||
return m_value[j];
|
||||
}
|
||||
|
|
@ -343,10 +484,58 @@ namespace opt {
|
|||
m_value[j] = l_true;
|
||||
m_value_trail.push_back(j);
|
||||
}
|
||||
|
||||
void unselect(unsigned j) {
|
||||
m_value[j] = l_false;
|
||||
m_value_trail.push_back(j);
|
||||
}
|
||||
|
||||
bool have_selected(lbool val, vector<set> const& Sets, unsigned& i) {
|
||||
for (i = 0; i < Sets.size(); ++i) {
|
||||
if (!has_selected(val, Sets[i])) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void set_undef_to_false() {
|
||||
for (unsigned i = 0; i < m_value_saved.size(); ++i) {
|
||||
if (m_value_saved[i] == l_undef) {
|
||||
m_value_saved[i] = l_false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool values_satisfy_Ts(unsigned& i) {
|
||||
unsigned j = 0;
|
||||
for (i = 0; i < m_T.size(); ++i) {
|
||||
set const& T = m_T[i];
|
||||
for (j = 0; j < T.size(); ++j) {
|
||||
if (m_value_saved[T[j]] == l_false) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (T.size() == j) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
return i == m_T.size();
|
||||
}
|
||||
|
||||
bool has_selected(set const& S) {
|
||||
return has_selected(l_true, S);
|
||||
}
|
||||
|
||||
bool has_unselected(set const& S) {
|
||||
return has_selected(l_false, S);
|
||||
}
|
||||
|
||||
bool has_unset(set const& S) {
|
||||
return has_selected(l_undef, S);
|
||||
}
|
||||
|
||||
bool has_selected(lbool val, set const& S) {
|
||||
for (unsigned i = 0; i < S.size(); ++i) {
|
||||
if (l_true == selected(S[i])) {
|
||||
if (val == selected(S[i])) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -357,11 +546,14 @@ namespace opt {
|
|||
hitting_sets::hitting_sets() { m_imp = alloc(imp); }
|
||||
hitting_sets::~hitting_sets() { dealloc(m_imp); }
|
||||
void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); }
|
||||
void hitting_sets::add_set(unsigned sz, unsigned const* elems) { m_imp->add_set(sz, elems); }
|
||||
bool hitting_sets::compute_lower() { return m_imp->compute_lower(); }
|
||||
bool hitting_sets::compute_upper() { return m_imp->compute_upper(); }
|
||||
void hitting_sets::add_exists_true(unsigned sz, unsigned const* elems) { m_imp->add_exists_true(sz, elems); }
|
||||
void hitting_sets::add_exists_false(unsigned sz, unsigned const* elems) { m_imp->add_exists_false(sz, elems); }
|
||||
lbool hitting_sets::compute_lower() { return m_imp->compute_lower(); }
|
||||
lbool hitting_sets::compute_upper() { return m_imp->compute_upper(); }
|
||||
rational hitting_sets::get_lower() { return m_imp->get_lower(); }
|
||||
rational hitting_sets::get_upper() { return m_imp->get_upper(); }
|
||||
void hitting_sets::set_upper(rational const& r) { return m_imp->set_upper(r); }
|
||||
bool hitting_sets::get_value(unsigned idx) { return m_imp->get_value(idx); }
|
||||
void hitting_sets::set_cancel(bool f) { m_imp->set_cancel(f); }
|
||||
void hitting_sets::collect_statistics(::statistics& st) const { m_imp->collect_statistics(st); }
|
||||
void hitting_sets::reset() { m_imp->reset(); }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue