mirror of
https://github.com/Z3Prover/z3
synced 2026-07-18 13:05:46 +00:00
2d17f0428a
The Diophantine-handler scheduler in int_solver applies an exponential backoff: solve_dioph_eq() doubles dio_calls_period on every unproductive (undef) dio call to "throttle dio scheduling on failure", letting the solver escalate to Gomory cuts / branching once dio is persistently unproductive. should_solve_dioph_eq() additionally decreased dio_calls_period by a fixed amount (dio_calls_period_decrease, default 2) on every final_check where dio did not fire. Because non-firing calls vastly outnumber firing calls once the period grows, this linear per-call decrease overwhelms the geometric backoff and pins the period near its initial small value, so an unproductive dio keeps firing and the handoff to Gomory/branching never durably engages. On the nonlinear mixed Int/Real benchmark iss-8418/3.smt2 this causes a 20s timeout where the instance was previously solved as sat. Removing the linear recovery (and the now-unused dio_calls_period_decrease parameter) restores the intended backoff; the benchmark is solved sat in ~0.03s. The dio-before-Gomory ordering and the dio_gomory_enable_period gating are left unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
18 lines
2.2 KiB
Text
18 lines
2.2 KiB
Text
def_module_params(module_name='lp',
|
|
class_name='lp_params_helper',
|
|
description='linear programming parameters',
|
|
export=True,
|
|
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_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'),
|
|
))
|
|
|