METADATA
# LHS
Ramon benchmark for Z3
-
Job description: lll_cube branch (bed5324) lex+monotone guard with lp.enable_lll_cube=true on QF_LIA
Job tag: lll-cube-on-rs-lex-mono
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: bed532442b3378de9ff1455eb322b690eef3fb95
Z3 branch: lll_cube
Z3 options: "-T:200 lp.enable_lll_cube=true smt.random_seed=25"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: lll-cube: restore C(B) monotonicity, hoist invariants, cap candidate q
Three combined fixes to the lexicographic basis-reduction heuristic.
1. Monotonicity guard. The lexicographic scoring in reduce_pair can
accept moves with cost > cost(B=I) if they reduce the bound-collapse
excess. Across passes this lets the basis drift to C(B) > C(I), which
then bloats compute_deltas and triggers bail_tighten or wastes work in
find_feasible_solution. We maintain an unweighted running C(B) and
compare against the C(I) baseline taken right after build_matrix; if
the basis search did not strictly improve, operator() bails as
lia_move::undef. Restores the pre-lex 'never worse than plain
int_cube' invariant noted in the header.
2. Candidate magnitude cap. The new candidate set includes values of
the form floor((a +/- (width - base)) / b), where 'width' is the
raw bound interval. Wide-box columns (e.g. width = 1e6) produced
q values far outside the breakpoint range, seeding basis growth
that overflowed too_big() downstream. Add an explicit 64-bit
bitsize ceiling on candidates, well below LLL_CUBE_BITSIZE_LIMIT.
3. Hoist invariants out of reduce_pair. Eligibility, width, and
integral_unit are computed once per operator() call (init_pair_-
invariants). Row 1-norms are cached in m_row_sum_H/m_row_sum_B
and maintained incrementally on each accepted move; the inner
base = sum_{c != j} |M[r][c]| computation collapses from O(n) per
risk row per pair to O(1) (row_sum - |entry|). Per-pair cost in
the risk-row build drops from O((m+n)*n) to O(m+n); at the limits
(m=75, n=150, 8 passes, ~27 candidates) this is ~6-7x fewer mpq
ops per compute_basis call, with the dominant savings being the
per-row 'mpq base(0); base += abs(...)' GMP allocations.
Soundness is unchanged: the moves applied are still unimodular
column ops, and the rounding path still uses B^{-1} and B as before.
Signed-off-by: Lev Nachmanson
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# RHS
Ramon benchmark for Z3
-
Job description: lll_cube branch (bed5324) lex+monotone guard with lp.enable_lll_cube=true on QF_LIA
Job tag: lll-cube-on-rs-lex-mono
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: bed532442b3378de9ff1455eb322b690eef3fb95
Z3 branch: lll_cube
Z3 options: "-T:200 lp.enable_lll_cube=true smt.random_seed=25"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: lll-cube: restore C(B) monotonicity, hoist invariants, cap candidate q
Three combined fixes to the lexicographic basis-reduction heuristic.
1. Monotonicity guard. The lexicographic scoring in reduce_pair can
accept moves with cost > cost(B=I) if they reduce the bound-collapse
excess. Across passes this lets the basis drift to C(B) > C(I), which
then bloats compute_deltas and triggers bail_tighten or wastes work in
find_feasible_solution. We maintain an unweighted running C(B) and
compare against the C(I) baseline taken right after build_matrix; if
the basis search did not strictly improve, operator() bails as
lia_move::undef. Restores the pre-lex 'never worse than plain
int_cube' invariant noted in the header.
2. Candidate magnitude cap. The new candidate set includes values of
the form floor((a +/- (width - base)) / b), where 'width' is the
raw bound interval. Wide-box columns (e.g. width = 1e6) produced
q values far outside the breakpoint range, seeding basis growth
that overflowed too_big() downstream. Add an explicit 64-bit
bitsize ceiling on candidates, well below LLL_CUBE_BITSIZE_LIMIT.
3. Hoist invariants out of reduce_pair. Eligibility, width, and
integral_unit are computed once per operator() call (init_pair_-
invariants). Row 1-norms are cached in m_row_sum_H/m_row_sum_B
and maintained incrementally on each accepted move; the inner
base = sum_{c != j} |M[r][c]| computation collapses from O(n) per
risk row per pair to O(1) (row_sum - |entry|). Per-pair cost in
the risk-row build drops from O((m+n)*n) to O(m+n); at the limits
(m=75, n=150, 8 passes, ~27 candidates) this is ~6-7x fewer mpq
ops per compute_basis call, with the dominant savings being the
per-row 'mpq base(0); base += abs(...)' GMP allocations.
Soundness is unchanged: the moves applied are still unimodular
column ops, and the rounding path still uses B^{-1} and B as before.
Signed-off-by: Lev Nachmanson
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>