mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

lp: restore deterministic integer heuristic gates by default (random_hammers=false)

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-07-05 01:49:29 -07:00 • committed by GitHub
parent 557a0cadab
commit 380ad825e6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lp_params_helper.pyg
View file

@ -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'),
))

2
src/math/lp/lp_settings.h
View file

@ -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: