From 7e3f948c5c7ac14812d52a8382d06975f44c6148 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Jul 2026 14:22:02 -0700 Subject: [PATCH] Fix branching selection in int_solver to prefer smallest absolute value (#10255) 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 --- src/math/lp/int_solver.cpp | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 287a57fd06..df31b9f5e7 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -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))