mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
fixes in branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
236edad8dc
commit
530f77281c
9 changed files with 20 additions and 40 deletions
|
|
@ -442,12 +442,7 @@ int gomory::find_basic_var() {
|
|||
}
|
||||
|
||||
lia_move gomory::operator()() {
|
||||
if (lra.move_non_basic_columns_to_bounds()) {
|
||||
lp_status st = lra.find_feasible_solution();
|
||||
(void)st;
|
||||
lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
|
||||
}
|
||||
|
||||
lra.move_non_basic_columns_to_bounds();
|
||||
int j = find_basic_var();
|
||||
if (j == -1) return lia_move::undef;
|
||||
unsigned r = lia.row_of_basic_column(j);
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ namespace lp {
|
|||
lia.m_k = mpq(0);
|
||||
}
|
||||
else {
|
||||
lia.m_upper = lra.settings().branch_flip()? lia.random() % 2 : left_branch_is_more_narrow_than_right(j);
|
||||
lia.m_upper = lia.random() % 2;
|
||||
lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));
|
||||
}
|
||||
|
||||
|
|
@ -55,23 +55,6 @@ namespace lp {
|
|||
return lia_move::branch;
|
||||
}
|
||||
|
||||
bool int_branch::left_branch_is_more_narrow_than_right(unsigned j) {
|
||||
switch (lra.get_column_type(j)) {
|
||||
case column_type::fixed:
|
||||
return false;
|
||||
case column_type::boxed: {
|
||||
auto k = floor(lia.get_value(j));
|
||||
return k - lia.lower_bound(j).x < lia.upper_bound(j).x - (k + mpq(1));
|
||||
}
|
||||
case column_type::lower_bound:
|
||||
return true;
|
||||
case column_type::upper_bound:
|
||||
return false;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
int int_branch::find_inf_int_base_column() {
|
||||
unsigned inf_int_count = 0;
|
||||
int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
|
||||
|
|
@ -93,8 +76,9 @@ namespace lp {
|
|||
}
|
||||
|
||||
int int_branch::find_inf_int_nbasis_column() const {
|
||||
|
||||
for (unsigned j : lra.r_nbasis())
|
||||
if (!lia.column_is_int_inf(j)) {
|
||||
if (lia.column_is_int_inf(j)) {
|
||||
return j;
|
||||
}
|
||||
return -1;
|
||||
|
|
|
|||
|
|
@ -28,7 +28,6 @@ namespace lp {
|
|||
class int_solver& lia;
|
||||
class lar_solver& lra;
|
||||
lia_move create_branch_on_column(int j);
|
||||
bool left_branch_is_more_narrow_than_right(unsigned j);
|
||||
int find_inf_int_base_column();
|
||||
int get_kth_inf_int(unsigned k) const;
|
||||
int find_inf_int_nbasis_column() const;
|
||||
|
|
|
|||
|
|
@ -42,8 +42,8 @@ namespace lp {
|
|||
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
|
||||
TRACE("cube", tout << "cannot find a feasiblie solution";);
|
||||
lra.pop();
|
||||
lra.set_status(lp_status::OPTIMAL);
|
||||
lra.move_non_basic_columns_to_bounds();
|
||||
find_feasible_solution();
|
||||
// it can happen that we found an integer solution here
|
||||
return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -445,8 +445,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
|
|||
void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
|
||||
TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
|
||||
m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
|
||||
if (move_non_basic_columns_to_bounds())
|
||||
find_feasible_solution();
|
||||
move_non_basic_columns_to_bounds();
|
||||
auto & rslv = m_mpq_lar_core_solver.m_r_solver;
|
||||
rslv.set_using_infeas_costs(false);
|
||||
lp_assert(costs_are_zeros_for_r_solver());
|
||||
|
|
@ -464,17 +463,26 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
|
|||
lp_assert(rslv.reduced_costs_are_correct_tableau());
|
||||
}
|
||||
|
||||
bool lar_solver::move_non_basic_columns_to_bounds() {
|
||||
bool feasible(lp_status st) {
|
||||
return st == lp_status::FEASIBLE || st == lp_status::OPTIMAL;
|
||||
}
|
||||
|
||||
void lar_solver::move_non_basic_columns_to_bounds() {
|
||||
auto & lcs = m_mpq_lar_core_solver;
|
||||
bool change = false;
|
||||
bool feas = feasible(get_status());
|
||||
for (unsigned j : lcs.m_r_nbasis) {
|
||||
if (move_non_basic_column_to_bounds(j))
|
||||
change = true;
|
||||
}
|
||||
|
||||
if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs)
|
||||
if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change)
|
||||
update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
|
||||
return change;
|
||||
|
||||
if (feas && change) {
|
||||
find_feasible_solution();
|
||||
SASSERT(feasible(get_status()));
|
||||
}
|
||||
}
|
||||
|
||||
bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {
|
||||
|
|
|
|||
|
|
@ -421,7 +421,7 @@ public:
|
|||
inline int_solver * get_int_solver() { return m_int_solver; }
|
||||
inline const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; }
|
||||
lp_status find_feasible_solution();
|
||||
bool move_non_basic_columns_to_bounds();
|
||||
void move_non_basic_columns_to_bounds();
|
||||
bool move_non_basic_column_to_bounds(unsigned j);
|
||||
inline bool r_basis_has_inf_int() const {
|
||||
for (unsigned j : r_basis()) {
|
||||
|
|
|
|||
|
|
@ -200,7 +200,6 @@ public:
|
|||
unsigned limit_on_columns_for_hnf_cutter;
|
||||
bool m_enable_hnf;
|
||||
bool m_print_external_var_name;
|
||||
bool m_branch_flip;
|
||||
#ifdef Z3DEBUG
|
||||
unsigned m_counter_for_debug;
|
||||
#endif
|
||||
|
|
@ -271,15 +270,12 @@ public:
|
|||
limit_on_rows_for_hnf_cutter(75),
|
||||
limit_on_columns_for_hnf_cutter(150),
|
||||
m_enable_hnf(true),
|
||||
m_print_external_var_name(false),
|
||||
m_branch_flip(false)
|
||||
m_print_external_var_name(false)
|
||||
#ifdef Z3DEBUG
|
||||
, m_counter_for_debug(0)
|
||||
#endif
|
||||
{}
|
||||
|
||||
bool branch_flip() const { return m_branch_flip; }
|
||||
void set_branch_flip(bool f) { m_branch_flip = f; }
|
||||
void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }
|
||||
bool get_cancel_flag() const { return m_resource_limit->get_cancel_flag(); }
|
||||
|
||||
|
|
|
|||
|
|
@ -62,7 +62,6 @@ def_module_params(module_name='smt',
|
|||
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
|
||||
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
|
||||
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
|
||||
('arith.branch_flip', BOOL, False, 'flip branches randomly'),
|
||||
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
|
||||
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
|
||||
|
|
|
|||
|
|
@ -396,7 +396,6 @@ class theory_lra::imp {
|
|||
lp().settings().print_statistics = lpar.arith_print_stats();
|
||||
|
||||
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
|
||||
lp().settings().set_branch_flip(lpar.arith_branch_flip());
|
||||
unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
|
||||
lp().set_cut_strategy(branch_cut_ratio);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue