mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-29 18:23:49 +00:00
Code Activity

Fix branching selection in int_solver to prefer smallest absolute value (#10255)

Browse source 
Fixes #10241

Among columns with a large value, the branching selection now prefers
the one whose absolute value is smallest. This avoids branching on ever
larger integers when better (smaller) options are available.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 1b264f0c-4bcc-4790-a3b8-5f038cc71f89
This commit is contained in:
Nikolaj Bjorner 2026-07-27 14:22:02 -07:00 • committed by GitHub
parent aa0ebc6efc
commit 7e3f948c5c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/int_solver.cpp
View file

@ -334,6 +334,7 @@ namespace lp {
mpq range;
mpq new_range;
mpq small_value(1024);
mpq min_any_value;
unsigned prev_usage = 0;
auto add_column = [&](bool improved, int& result, unsigned& n, unsigned j) {
@ -369,9 +370,21 @@ namespace lp {
continue;
}
TRACE(int_solver, tout << "any j" << j << "\n");
add_column(usage >= prev_usage, r_any_value, n_any_value, j);
if (usage > prev_usage)
// Among columns with a large value, prefer the one whose
// absolute value is smallest to avoid branching on ever
// larger integers when better (smaller) options are available.
mpq const abs_value = abs(value.x);
if (r_any_value == -1 || abs_value < min_any_value) {
r_any_value = j;
min_any_value = abs_value;
n_any_value = 1;
prev_usage = usage;
}
else if (abs_value == min_any_value) {
add_column(usage >= prev_usage, r_any_value, n_any_value, j);
if (usage > prev_usage)
prev_usage = usage;
}
}
if (r_small_box != -1 && (random() % 3 != 0))