mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

start gomory cut

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-11 13:38:59 -07:00
parent 69d6b022b8
commit fc6a876845
3 changed files with 64 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -1252,6 +1252,11 @@ namespace smt {
// SAT core assigns a value to
return l_false;
}
case lp::lia_move::bound: {
// todo nikolaj
// Need to set a bound >= k on the only var from the term
return l_false;
}
case lp::lia_move::cut: {
// m_explanation implies term <= k
app_ref b = mk_bound(term, k);

79
src/util/lp/int_solver.cpp
View file

@ -110,26 +110,21 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() {
}
bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
/**
\brief Create bounds for (non base) free vars in the given row.
Return true if at least one variable was constrained.
This method is used to enable the application of gomory cuts.
*/
auto row_it = m_lar_solver->get_iterator_on_row(row_index);
lia_move int_solver::mk_gomory_cut(explanation & ex) {
lp_assert(column_is_int_inf(m_gomory_cut_inf_column));
return lia_move::give_up;
unsigned x_i = m_lar_solver->get_base_column_in_row(row_index);
lp_assert(column_is_int_inf(x_i));
/*
SASSERT(is_int(x_i));
// The following assertion is wrong. It may be violated in mixed-real-interger problems.
// The check is_gomory_cut_target will discard rows where any variable contains infinitesimals.
// SASSERT(m_value[x_i].is_rational()); // infinitesimals are not used for integer variables
SASSERT(!m_value[x_i].is_int()); // the base variable is not assigned to an integer value.
if (constrain_free_vars(r) || !is_gomory_cut_target(r)) {
TRACE("gomory_cut", tout << "failed to apply gomory cut:\n";
tout << "constrain_free_vars(r): " << constrain_free_vars(r) << "\n";);
return false;
}
TRACE("gomory_cut", tout << "applying cut at:\n"; display_row_info(tout, r););
antecedents ante(*this);
@ -287,9 +282,6 @@ bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
return true;
*/
delete row_it;
return true;
}
void int_solver::init_check_data() {
@ -299,9 +291,35 @@ void int_solver::init_check_data() {
m_old_values_data.resize(n);
}
int int_solver::find_next_free_var_in_gomory_row() {
lp_assert(m_iter_on_gomory_row != nullptr);
unsigned j;
while(m_iter_on_gomory_row->next(j)) {
if (is_free(j))
return static_cast<int>(j);
}
return -1;
}
lia_move int_solver::proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& ex) {
int j = find_next_free_var_in_gomory_row();
if (j != -1) {
lp_assert(t.is_empty());
t.add_to_map(j, mpq(1));
k = zero_of_type<mpq>();
return lia_move::bound;
}
delete m_iter_on_gomory_row;
m_iter_on_gomory_row = nullptr;
return mk_gomory_cut(ex);
}
lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
lp_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
lp_assert(is_feasible());
if (m_iter_on_gomory_row != nullptr) {
return proceed_with_gomory_cut(t, k, ex);
}
init_check_data();
lp_assert(inf_int_set_is_correct());
// currently it is a reimplementation of
@ -333,13 +351,12 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
}
int j = find_inf_int_base_column();
if (j != -1) {
// setup the call for gomory cut
TRACE("arith_int", tout << "j = " << j << " does not have an integer assignment: " << get_value(j) << "\n";);
unsigned row_index = m_lar_solver->m_mpq_lar_core_solver.m_r_heading[j];
if (!mk_gomory_cut(row_index, ex)) {
return lia_move::give_up;
// silent failure
}
return lia_move::cut;
m_iter_on_gomory_row = m_lar_solver->get_iterator_on_row(row_index);
m_gomory_cut_inf_column = j;
return check(t, k, ex);
}
}
else {
@ -623,7 +640,8 @@ linear_combination_iterator<mpq> * int_solver::get_column_iterator(unsigned j) {
int_solver::int_solver(lar_solver* lar_slv) :
m_lar_solver(lar_slv),
m_branch_cut_counter(0) {
m_branch_cut_counter(0),
m_iter_on_gomory_row(nullptr) {
lp_assert(m_old_values_set.size() == 0);
m_old_values_set.resize(lar_slv->A_r().column_count());
m_old_values_data.resize(lar_slv->A_r().column_count(), zero_of_type<impq>());
@ -810,6 +828,11 @@ bool int_solver::is_boxed(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
}
bool int_solver::is_free(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
}
lp_settings& int_solver::settings() {
return m_lar_solver->settings();
}

9
src/util/lp/int_solver.h
View file

@ -18,6 +18,7 @@ enum class lia_move {
branch,
cut,
conflict,
bound,
give_up
};
@ -33,6 +34,8 @@ public:
vector<impq> m_old_values_data;
int_set m_inf_int_set;
unsigned m_branch_cut_counter;
linear_combination_iterator<mpq>* m_iter_on_gomory_row;
unsigned m_gomory_cut_inf_column;
// methods
int_solver(lar_solver* lp);
// main function to check that solution provided by lar_solver is valid for integral values,
@ -80,6 +83,7 @@ private:
bool is_int(unsigned j) const;
bool is_base(unsigned j) const;
bool is_boxed(unsigned j) const;
bool is_free(unsigned j) const;
bool value_is_int(unsigned j) const;
void set_value_for_nbasic_column(unsigned j, const impq & new_val);
void fix_non_base_columns();
@ -97,7 +101,10 @@ private:
lp_settings& settings();
void move_non_base_vars_to_bounds();
void branch_infeasible_int_var(unsigned);
bool mk_gomory_cut(unsigned row_index, explanation & ex);
lia_move mk_gomory_cut(explanation & ex);
void init_check_data();
bool constrain_free_vars(linear_combination_iterator<mpq> * r);
lia_move proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& ex);
int find_next_free_var_in_gomory_row();
};
}