METADATA
# LHS
Ramon benchmark for Z3
-
Job description: lll_cube branch with lp.enable_lll_cube=false on QF_LIA
Job tag: lll-cube-off
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 2ba7d7ed702cd059809af7173f2a63fcfc2499be
Z3 branch: lll_cube
Z3 options: "-T:200 lp.enable_lll_cube=false"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: lll-cube: weight C(B) by column tightness to favor tight-box rows
Replace the unweighted greedy with a weighted cube cost
C(B) = sum_j w_j * delta_j(B) + sum_i delta_i(B)
where w_j = max(1, 2/width(j)) for columns with finite [lb, ub] and 1
elsewhere. compute_col_weights() runs once after build_matrix(); the
breakpoint pairing in reduce_pair() now carries a combined weight and
sorts/medians/evaluates with it.
Soundness is unchanged: weights only steer the choice of B; the actual
delta_col(j) = (1/2)||row_j(B)||_1 used to tighten bounds is recomputed
from the resulting B.
On the QF_LIA Bromberger CAV_2009 family this enables the rounding path
to fire for the first time: v45_problem_2__028.slack solves in 0.88s
(LLL on) vs 7.05s (LLL off), with arith-lll-cube-success = 1.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# RHS
Ramon benchmark for Z3
-
Job description: lll_cube branch with lp.enable_lll_cube=false on QF_LIA
Job tag: lll-cube-off
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 2ba7d7ed702cd059809af7173f2a63fcfc2499be
Z3 branch: lll_cube
Z3 options: "-T:200 lp.enable_lll_cube=false"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: lll-cube: weight C(B) by column tightness to favor tight-box rows
Replace the unweighted greedy with a weighted cube cost
C(B) = sum_j w_j * delta_j(B) + sum_i delta_i(B)
where w_j = max(1, 2/width(j)) for columns with finite [lb, ub] and 1
elsewhere. compute_col_weights() runs once after build_matrix(); the
breakpoint pairing in reduce_pair() now carries a combined weight and
sorts/medians/evaluates with it.
Soundness is unchanged: weights only steer the choice of B; the actual
delta_col(j) = (1/2)||row_j(B)||_1 used to tighten bounds is recomputed
from the resulting B.
On the QF_LIA Bromberger CAV_2009 family this enables the rounding path
to fire for the first time: v45_problem_2__028.slack solves in 0.88s
(LLL on) vs 7.05s (LLL off), with arith-lll-cube-success = 1.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>