From a75c860899752a96cd8bdf05fdeccd0903b65ecf Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 18 Jun 2026 16:10:55 -0700 Subject: [PATCH] lp: randomize the Gomory-cut gate to break period resonance should_gomory_cut used a deterministic schedule (m_number_of_calls % m_int_gomory_cut_period == 0). On some UNSAT QF_LIA families (e.g. rings_preprocessed, cut_lemmas) this fixed period phase-locks with the search: the solver drowns in theory conflicts (~32k vs ~2k) while the Diophantine tightening that would close the proof is starved, causing timeouts that vanish when the period is changed (4 vs 5). Replace the modulus with a random draw of the same expected rate (random_next(period) == 0). This breaks the deterministic resonance while preserving the average cut frequency. Locally this turns the whole regressing band from timeouts / ~23s into sub-second-to-seconds solves, with no slowdown observed on a regression sample and lp unit tests passing. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/int_solver.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index aec275b77..9e392678f 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -220,7 +220,12 @@ namespace lp { bool should_gomory_cut() { bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() || m_dio.some_terms_are_ignored(); - return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0; + // Draw the decision at random instead of using a fixed "every k-th + // call" modulus. A deterministic period can phase-lock with the + // search on some UNSAT families and drown the solver in theory + // conflicts while the Diophantine handler is starved; randomizing + // the gate (same 1/period expected rate) breaks that resonance. + return dio_allows_gomory && settings().random_next(settings().m_int_gomory_cut_period) == 0; } bool should_solve_dioph_eq() {