3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-19 13:35:48 +00:00
Commit graph

16 commits

Author SHA1 Message Date
Lev Nachmanson
c4ac986c42 lp: add efficacy-augment Gomory mode (keep fractional cut + diversify by efficacy)
Add lp.gomory_efficacy_augment (default false). Unlike gomory_efficacy_select
(which fully replaces fractionality-based row choice), augment keeps one
fractionality-selected cut with priority and fills the remaining cut slots with
the most efficacious cuts built from gomory_candidate_rows random candidate
rows, subject to gomory_cut_efficacy_threshold. This preserves the proven
baseline cut while adding a depth-diversified second cut.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-25 15:50:37 -07:00
Lev Nachmanson
11e95dafeb lp: add best-of-N efficacy-based Gomory row selection
Add lp.gomory_efficacy_select (default false) and lp.gomory_candidate_rows
(default 3). When enabled, Gomory cut rows are no longer chosen by how close
the basic variable is to an integer. Instead, gomory_candidate_rows
integer-infeasible GMI-clean rows are sampled uniformly at random, a cut is
built for each, and the most efficacious cuts whose efficacy
(k - t(x*))/||t||_2 is at least gomory_cut_efficacy_threshold are added (up to
num_cuts of them, best first).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-25 15:24:23 -07:00
Lev Nachmanson
8d1dde407e lp: add optional efficacy filter for Gomory cuts
Add lp.gomory_cut_efficacy_filter (default false) and
lp.gomory_cut_efficacy_threshold (default 0.01). When enabled, a
generated Gomory cut t >= k is discarded if its efficacy
(k - t(x*))/||t||_2, the normalized distance from the LP solution to the
cut hyperplane, is below the threshold. Comparison is done on squared
quantities to stay rational and deterministic.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-25 14:51:32 -07:00
Lev Nachmanson
57fb719007
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>
2026-06-25 14:21:44 -07:00
Lev Nachmanson
f508854fe5
Lcube (#9858)
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-14 16:25:21 -07:00
Lev Nachmanson
f5b8dfc2f1 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases"
This reverts commit bee2b45743.
2026-02-07 10:45:15 -10:00
Lev Nachmanson
73696725e4 Revert "try fixed int patch period"
This reverts commit 3e2027ec11.
2026-02-07 10:45:15 -10:00
Lev Nachmanson
3e2027ec11 try fixed int patch period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-02-06 14:40:04 -10:00
Lev Nachmanson
bee2b45743 optionally throttle patch_basic_columns() especially useful in unsat cases
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-02-06 10:14:39 -10:00
Lev Nachmanson
f680242620 adjust the frequency of dio calls
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-14 08:17:39 -07:00
Lev Nachmanson
ab9f3307d6 change the default of running dio to true, and running gcd to false, remove branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
17af18fe31 make gcd call in dio optional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
1cde40bddb dio_calls_period=4 2025-04-18 18:24:50 -07:00
Lev Nachmanson
8db9f52386 add parameter m_dio_calls_period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
972f80188a throttle dio for big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
3e49d9fcfe reuse dio branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00