From 2dfed1d96cb3aecc3f47fc08a570674fd369750c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Fri, 3 Jul 2026 02:01:38 -0700 Subject: [PATCH] Batch fixed-column bound-witness linearization per row explain_fixed_in_row explained each fixed column of a row independently via explain_fixed_column, re-traversing and re-inserting the shared bound-witness dependency sub-DAGs once per column. Collect the lower and upper witnesses of all fixed columns in the row and linearize them in a single u_dependency_manager pass, so each shared sub-DAG node and each distinct leaf constraint is handled once. explanation is a set, so the result is identical. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/lar_solver.cpp | 19 +++++++++++++++++++ src/math/lp/lar_solver.h | 1 + src/math/lp/lp_bound_propagator.h | 16 +++++----------- 3 files changed, 25 insertions(+), 11 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 9e9d1add14..d743c5342d 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -63,6 +63,7 @@ namespace lp { unsigned_vector m_row_bounds_to_replay; u_dependency_manager m_dependencies; svector m_tmp_dependencies; + ptr_vector m_tmp_witnesses; u_dependency* m_crossed_bounds_deps = nullptr; lpvar m_crossed_bounds_column = null_lpvar; @@ -1132,6 +1133,24 @@ namespace lp { ex.push_back(ci); } + // Linearize the bound witnesses of all fixed columns in the row together, so the + // mark bits walk each dependency sub-DAG shared between columns only once. + void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) { + auto& witnesses = m_imp->m_tmp_witnesses; + witnesses.reset(); + for (auto const& c : get_row(row)) { + if (!column_is_fixed(c.var())) + continue; + const column& ul = m_imp->m_columns[c.var()]; + witnesses.push_back(ul.lower_bound_witness()); + witnesses.push_back(ul.upper_bound_witness()); + } + m_imp->m_tmp_dependencies.reset(); + m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies); + for (auto ci : m_imp->m_tmp_dependencies) + ex.push_back(ci); + } + void lar_solver::remove_fixed_vars_from_base() { // this will allow to disable and restore the tracking of the touched rows flet f(get_core_solver().m_r_solver.m_touched_rows, nullptr); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 79c729e5d1..4588f1772f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -521,6 +521,7 @@ public: } void explain_fixed_column(unsigned j, explanation& ex); + void explain_fixed_in_row(unsigned row, explanation& ex); u_dependency* join_deps(u_dependency* a, u_dependency *b) { return dep_manager().mk_join(a, b); } const constraint_set & constraints() const; void push(); diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 2568c51fbd..3df2fbf741 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -248,22 +248,16 @@ public: void explain_fixed_in_row(unsigned row, explanation& ex) { TRACE(eq, tout << lp().get_row(row) << std::endl); - for (const auto& c : lp().get_row(row)) - if (lp().column_is_fixed(c.var())) - lp().explain_fixed_column(c.var(), ex); + lp().explain_fixed_in_row(row, ex); } unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) { - unsigned base = UINT_MAX; TRACE(eq, tout << lp().get_row(row) << std::endl); - for (const auto& c : lp().get_row(row)) { - if (lp().column_is_fixed(c.var())) { - lp().explain_fixed_column(c.var(), ex); - } - else if (lp().is_base(c.var())) { + lp().explain_fixed_in_row(row, ex); + unsigned base = UINT_MAX; + for (const auto& c : lp().get_row(row)) + if (!lp().column_is_fixed(c.var()) && lp().is_base(c.var())) base = c.var(); - } - } return base; }