mirror of
https://github.com/Z3Prover/z3
synced 2026-07-25 08:22:35 +00:00
lp: gate Gomory-with-dio on genuine dio failures; separate config from runtime state (#9958)
## Summary Improves the Diophantine (`dio`) integer-feasibility controller in `int_solver`, and fixes a latent bug where the user's Gomory-cut configuration could be silently overridden at runtime. Also includes the earlier `lia_w` work: randomized hammer gates, the `int_hammer_period` / `random_hammers` parameters, and the linear `dio_calls_period` recovery. ## Motivation The controller used a **single field** both as the static `lp.dio_cuts_enable_gomory` parameter and as the live "is Gomory running" flag. It started running Gomory (and the gcd test) once `dio_calls_period` crossed a hard-coded `16`. Because `dio_calls_period` is also driven by the randomized hammer gate, on instances where `dio` is only intermittently productive the period could be ratcheted past 16 *by chance*, turning on Gomory + gcd and thrashing — e.g. `dillig/20-14` went from a 100s solve (deterministic) to a 600s timeout (randomized) purely from this spurious activation. ## Changes - **Separate config from runtime state.** Split the shared field into `m_dio_cuts_enable_gomory` (static config, never mutated) and `m_run_gomory_with_dio` (runtime flag). Toggling the runtime state can no longer clobber the user's `dio_cuts_enable_gomory` parameter. - **Trigger on genuine dio failures, not the period proxy.** Running Gomory-with-dio now starts after a count of **consecutive `undef` dio returns** (reset on a dio conflict) rather than when the randomization-inflated period crosses a threshold — robust to `random_hammers` gate variance. - **Parameterize the threshold.** New `lp.dio_gomory_enable_period` (default 16). Set it very large to never auto-start Gomory, so Gomory follows `dio_cuts_enable_gomory` only. - **Try `dio` before Gomory** in `check()` so a productive dio conflict preempts Gomory on dio-dominated instances. ## Evaluation (QF_LIA, full set, 600s, seed 555 paired) - Dio-before-Gomory: **+33** problems across the 6 `random_hammers x int_hammer_period` cells (5/6 cells improve). - New trigger (`dio_gomory_enable_period=32`, random): **6417** vs the period-16 baseline **6409**; no short-cutoff regression. - Linear `dio_calls_period` recovery: keeping it on is worth ~+20 vs off; `decrease=1` slightly ahead of the default 2. Default behavior (`dio_gomory_enable_period=16`) is byte-for-byte equivalent to the previous threshold logic. ## Notes Debug-only tracing used during analysis (the `dio_calls_period_trace` parameter plus per-hammer / period-evolution verbose output) is **not** included. --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
parent
6fd303c4b9
commit
57fb719007
4 changed files with 72 additions and 15 deletions
|
|
@ -5,11 +5,15 @@ def_module_params(module_name='lp',
|
|||
params=(('dio', BOOL, True, 'use Diophantine equalities'),
|
||||
('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
|
||||
('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
|
||||
('dio_gomory_enable_period', UINT, 16, 'number of consecutive unproductive (undef) Diophantine-handler calls after which the controller starts running Gomory cuts and the gcd test alongside dio; a dio conflict resets the count and stops them; set very large to never start them this way so Gomory follows dio_cuts_enable_gomory only'),
|
||||
('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
|
||||
('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
|
||||
('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
|
||||
('dio_calls_period_decrease', UINT, 2, 'Amount by which dio_calls_period is decreased on each final_check() call where the Diophantine handler is not triggered, until it returns to its initial value'),
|
||||
('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
|
||||
('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'),
|
||||
))
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue