From 380ad825e66f2b57ba7658d8ec101c2f00471968 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 5 Jul 2026 01:49:29 -0700 Subject: [PATCH] lp: restore deterministic integer heuristic gates by default (random_hammers=false) Commit 57fb71900 (#9958) introduced `lp.random_hammers` (default true), which changed the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) from a deterministic `calls % period == 0` schedule to a randomized draw seeded from `smt.random_seed` (default 0). The randomized schedule has unbounded per-instance variance. On the dillig-family NIA benchmark iss-3072/bug-1.smt2 (Z3Prover/bench snapshot corpus) the default seed produces a pathological schedule: z3 no longer converges within the 20s budget (regressing from `sat` in ~5s to timeout), even though other seeds solve it in ~0.1s. The result is still correct when found, so this is a heuristic-scheduling regression, not a soundness issue. Restore the previously shipped deterministic gate schedule as the default by flipping `random_hammers` to false. The randomized mode remains fully available as an opt-in via `lp.random_hammers=true`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/lp_params_helper.pyg | 2 +- src/math/lp/lp_settings.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 29a10c2d52..4eaf718535 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -14,6 +14,6 @@ def_module_params(module_name='lp', ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'), ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'), ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'), - ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), + ('random_hammers', BOOL, False, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), )) diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index bc1f2044f5..5bd3bf4461 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -267,7 +267,7 @@ private: unsigned m_dio_calls_period = 4; unsigned m_dio_calls_period_decrease = 2; bool m_dio_run_gcd = true; - bool m_random_hammers = true; + bool m_random_hammers = false; bool m_lcube = true; unsigned m_lcube_flips = 16; public: