mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

some fixes in branching

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-26 20:35:22 -07:00
parent 029edcfabd
commit 0499b6b64a
2 changed files with 88 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,20 +1,20 @@
/*++ /*++
Copyright (c) 2020 Microsoft Corporation Copyright (c) 2020 Microsoft Corporation
Module Name: Module Name:
int_branch.cpp int_branch.cpp
Abstract: Abstract:
Branch heuristic Branch heuristic
Author: Author:
Lev Nachmanson (levnach) Lev Nachmanson (levnach)
Nikolaj Bjorner (nbjorner) Nikolaj Bjorner (nbjorner)
Revision History: Revision History:
--*/ --*/
#include "math/lp/int_solver.h" #include "math/lp/int_solver.h"
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
@ -22,98 +22,97 @@ Revision History:
namespace lp { namespace lp {
int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {} int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
lia_move int_branch::operator()() { lia_move int_branch::operator()() {
int j = find_any_inf_int_column_basis_first(); int j = find_any_inf_int_column_basis_first();
return j == -1? lia_move::sat : create_branch_on_column(j); return j == -1? lia_move::sat : create_branch_on_column(j);
}
int int_branch::find_any_inf_int_column_basis_first() {
int j = find_inf_int_base_column();
return j != -1 ? j : find_inf_int_nbasis_column();
}
lia_move int_branch::create_branch_on_column(int j) {
TRACE("check_main_int", tout << "branching" << std::endl;);
lp_assert(lia.m_t.is_empty());
lp_assert(j != -1);
lia.m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j));
if (lia.is_free(j)) {
lia.m_upper = lia.random() % 2;
lia.m_k = mpq(0);
}
else {
lia.m_upper = lia.random() % 2;
lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));
} }
int int_branch::find_any_inf_int_column_basis_first() { TRACE("int_solver",
int j = find_inf_int_base_column(); lia.display_column(tout << "branching v" << j << " = " << lia.get_value(j) << "\n", j);
return j != -1 ? j : find_inf_int_nbasis_column(); tout << "k = " << lia.m_k << std::endl;);
} return lia_move::branch;
}
lia_move int_branch::create_branch_on_column(int j) { int int_branch::find_inf_int_nbasis_column() const {
TRACE("check_main_int", tout << "branching" << std::endl;); unsigned n = 0;
lp_assert(lia.m_t.is_empty()); int r = -1;
lp_assert(j != -1); for (unsigned j : lra.r_nbasis()) {
lia.m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j)); SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
if (lia.is_free(j)) { if (lia.column_is_int_inf(j)) {
lia.m_upper = lia.random() % 2; if (n == 0) {
lia.m_k = mpq(0); r = j;
} n = 1;
else { } else if (lia.random() % (++n) == 0) {
lia.m_upper = lia.random() % 2; r = j;
lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));
}
TRACE("int_solver",
lia.display_column(tout << "branching v" << j << " = " << lia.get_value(j) << "\n", j);
tout << "k = " << lia.m_k << std::endl;);
return lia_move::branch;
}
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);
if (j != -1) {
return j;
}
if (inf_int_count == 0)
return -1;
unsigned k = lia.random() % inf_int_count;
return get_kth_inf_int(k);
}
int int_branch::get_kth_inf_int(unsigned k) const {
for (unsigned j : lra.r_basis())
if (lia.column_is_int_inf(j) && k-- == 0)
return j;
lp_assert(false);
return -1;
}
int int_branch::find_inf_int_nbasis_column() const {
for (unsigned j : lra.r_nbasis())
if (lia.column_is_int_inf(j)) {
return j;
} }
return -1; }
} }
return r;
}
int int_branch::find_inf_int_boxed_base_column_with_smallest_range(unsigned & inf_int_count) { int int_branch::find_inf_int_base_column() {
inf_int_count = 0; int result = -1;
int result = -1; mpq range;
mpq range; mpq new_range;
mpq new_range; mpq small_range_thresold(1024);
mpq small_range_thresold(1024); unsigned n = 0;
unsigned n = 0; lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver; bool small = false;
for (unsigned j : lra.r_basis()) {
for (unsigned j : lra.r_basis()) { SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
if (!lia.column_is_int_inf(j)) if (!lia.column_is_int_inf(j))
continue;
bool boxed = lia.is_boxed(j);
if (small) {
if (!boxed)
continue; continue;
inf_int_count++;
if (!lia.is_boxed(j))
continue;
lp_assert(!lia.is_fixed(j));
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;
if (new_range > small_range_thresold) if (new_range <= small_range_thresold) {
continue; if (new_range < range) {
if (result == -1 || new_range < range) { n = 1;
result = j; result = j;
range = new_range; range = new_range;
n = 1; } else if (new_range == range && lia.random() % (++n) == 0) {
} result = j;
else if (new_range == range && lia.random() % (++n) == 0) { }
lp_assert(n > 1);
result = j;
} }
} else if (boxed &&
(new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x)
<= small_range_thresold) {
small = true;
result = j;
range = new_range;
n = 1;
} else if (result == -1) {
result = j;
n = 1;
} else if (lia.random() % (++n) == 0) {
result = j;
} }
return result;
} }
return result;
}
} }

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

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