mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

better branching with usage_in_terms()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-27 12:48:30 -07:00
parent 3bbf1474f3
commit ba40a5752f
4 changed files with 28 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/math/lp/int_branch.cpp
View file

@ -25,13 +25,9 @@ namespace lp {
int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
lia_move int_branch::operator()() {
int j = find_any_inf_int_column_basis_first();
return j == -1? lia_move::sat : create_branch_on_column(j);
}
int int_branch::find_any_inf_int_column_basis_first() {
lra.move_non_basic_columns_to_bounds();
int j = find_inf_int_base_column();
return j != -1 ? j : find_inf_int_nbasis_column();
return j == -1? lia_move::sat : create_branch_on_column(j);
}
lia_move int_branch::create_branch_on_column(int j) {
@ -55,22 +51,6 @@ lia_move int_branch::create_branch_on_column(int j) {
}
int int_branch::find_inf_int_nbasis_column() const {
unsigned n = 0;
int r = -1;
for (unsigned j : lra.r_nbasis()) {
SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
if (lia.column_is_int_inf(j)) {
if (n == 0) {
r = j;
n = 1;
} else if (lia.random() % (++n) == 0) {
r = j;
}
}
}
return r;
}
int int_branch::find_inf_int_base_column() {
int result = -1;
@ -80,15 +60,17 @@ int int_branch::find_inf_int_base_column() {
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
bool small = false;
unsigned prev_usage;
for (unsigned j : lra.r_basis()) {
SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
if (!lia.column_is_int_inf(j))
continue;
bool boxed = lia.is_boxed(j);
unsigned usage = 2 * lra.usage_in_terms(j);
if (small) {
if (!boxed)
continue;
new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage);
if (new_range <= small_range_thresold) {
if (new_range < range) {
n = 1;
@ -98,16 +80,17 @@ int int_branch::find_inf_int_base_column() {
result = j;
}
}
} else if (boxed &&
(range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x)
<= small_range_thresold) {
} else if (boxed && (
(range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage))
<= small_range_thresold)) {
small = true;
result = j;
n = 1;
} else if (result == -1) {
} else if (result == -1 || prev_usage < usage) {
result = j;
prev_usage = usage;
n = 1;
} else if (lia.random() % (++n) == 0) {
} else if (prev_usage == usage && lia.random() % (++n) == 0) {
result = j;
}
}

2
src/math/lp/int_branch.h
View file

@ -29,8 +29,6 @@ namespace lp {
class lar_solver& lra;
lia_move create_branch_on_column(int j);
int find_inf_int_base_column();
int find_inf_int_nbasis_column() const;
int find_any_inf_int_column_basis_first();
public:
int_branch(int_solver& lia);

12
src/math/lp/lar_solver.cpp
View file

@ -323,6 +323,7 @@ void lar_solver::push() {
m_term_count = m_terms.size();
m_term_count.push();
m_constraints.push();
m_usage_in_terms.push();
}
void lar_solver::clean_popped_elements(unsigned n, u_set& set) {
@ -380,6 +381,7 @@ void lar_solver::pop(unsigned k) {
m_settings.simplex_strategy() = m_simplex_strategy;
lp_assert(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
m_usage_in_terms.pop(k);
set_status(lp_status::UNKNOWN);
}
@ -1599,14 +1601,17 @@ unsigned lar_solver::external_to_column_index(unsigned ext_j) const {
var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;);
var_index local_j;
var_index local_j;
SASSERT(!m_term_register.external_is_used(ext_j));
lp_assert(!tv::is_term(ext_j));
if (m_var_register.external_is_used(ext_j, local_j))
return local_j;
return local_j;
lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
local_j = A_r().column_count();
m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX));
while (m_usage_in_terms.size() <= ext_j) {
m_usage_in_terms.push_back(0);
}
add_non_basic_var_to_core_fields(ext_j, is_int);
lp_assert(sizes_are_correct());
return local_j;
@ -1775,6 +1780,9 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned
m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1));
if (use_lu())
fill_last_row_of_A_d(A_d(), term);
for (const auto & c : *term)
m_usage_in_terms[c.column()] = m_usage_in_terms[c.column()] + 1;
}
void lar_solver::add_basic_var_to_core_fields() {

9
src/math/lp/lar_solver.h
View file

@ -101,6 +101,7 @@ class lar_solver : public column_namer {
std::unordered_map<lar_term, std::pair<mpq, unsigned>, term_hasher, term_comparer>
m_normalized_terms_to_columns;
vector<impq> m_backup_x;
stacked_vector<unsigned> m_usage_in_terms;
// end of fields
////////////////// methods ////////////////////////////////
@ -467,9 +468,13 @@ public:
return -1;
}
}
unsigned usage_in_terms(column_index j) const {
if (j >= m_usage_in_terms.size())
return 0;
return m_usage_in_terms[j];
}
friend int_solver;
friend int_branch;
};
}