METADATA
# LHS
Ramon benchmark for Z3
-
Job description: hnf_cube branch with lp.enable_hnf_cube=true on QF_LIA
Job tag: hnf_cube-enabled
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 0532293d24e66b47e71dc40ba438c0d649a4ed19
Z3 branch: hnf_cube
Z3 options: "-T:200 smt.random_seed=111 lp.enable_hnf_cube=true"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: Add HNF cube heuristic for integer LP (experimental, default off)
Generalize the int_cube heuristic from the unit cube C = [-1/2, 1/2]^n to a
parallelepiped K = U.C, where U is unimodular obtained from column-reducing
the active term-coefficient matrix A to its Hermite Normal Form (A.U = H).
The per-row shrinkage in the lattice basis is delta_t = (1/2) * ||row of H||_1,
which is at most as large as the cube's (1/2) * ||row of A||_1, so the search
body is at least as tight as cube and often strictly tighter on poorly
axis-aligned constraint systems.
Soundness:
* apply_rounding mirrors lar_solver::round_to_integer_solution and uses
impq-aware floor/ceil so it preserves infinitesimal components in x*.
* The delta=0 fast path for rows of L1-norm <= 1 is only used when the
associated column has integer non-strict bounds; otherwise delta = 1/2.
* All work is done on a saved column snapshot and reverted on any bail-out
path, so failures (overflow, LP infeasible, etc.) do not perturb solver
state.
New parameters (both conservative defaults):
* lp.enable_hnf_cube (bool, default false) -- feature gate.
* lp.int_find_hnf_cube_period (uint, default 16, 0 disables) -- the HNF cube
is invoked every Nth final-check call after a plain cube failure, so its
cost is amortized vs. cube (which has period 4).
Statistics: arith-hnf-cube-{calls,success,bail-collect,bail-build,bail-hnf,
bail-tighten,bail-infeasible}.
Resource limits: rows<=75, cols<=150, bitsize<=4096; bail above.
Validation:
* SMT regression suite: 906/907 (same as baseline; the one failure is
pre-existing and unrelated).
* test-z3 /a: 89/89 unit tests pass.
* CAV-2009 50-instance sample, -T:30: sat=40 (matches baseline) with
1 hnf_cube_success and slightly lower wall time.
* QF_LIA random sample (100 instances), -T:10: sat=64 (matches baseline).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# RHS
Ramon benchmark for Z3
-
Job description: hnf_cube branch with lp.enable_hnf_cube=true on QF_LIA
Job tag: hnf_cube-enabled
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 0532293d24e66b47e71dc40ba438c0d649a4ed19
Z3 branch: hnf_cube
Z3 options: "-T:200 smt.random_seed=111 lp.enable_hnf_cube=true"
Z3 inputs: https://zenodo.org/records/11061097/files/QF_LIA.tar.zst?download=1
Z3 commit message: Add HNF cube heuristic for integer LP (experimental, default off)
Generalize the int_cube heuristic from the unit cube C = [-1/2, 1/2]^n to a
parallelepiped K = U.C, where U is unimodular obtained from column-reducing
the active term-coefficient matrix A to its Hermite Normal Form (A.U = H).
The per-row shrinkage in the lattice basis is delta_t = (1/2) * ||row of H||_1,
which is at most as large as the cube's (1/2) * ||row of A||_1, so the search
body is at least as tight as cube and often strictly tighter on poorly
axis-aligned constraint systems.
Soundness:
* apply_rounding mirrors lar_solver::round_to_integer_solution and uses
impq-aware floor/ceil so it preserves infinitesimal components in x*.
* The delta=0 fast path for rows of L1-norm <= 1 is only used when the
associated column has integer non-strict bounds; otherwise delta = 1/2.
* All work is done on a saved column snapshot and reverted on any bail-out
path, so failures (overflow, LP infeasible, etc.) do not perturb solver
state.
New parameters (both conservative defaults):
* lp.enable_hnf_cube (bool, default false) -- feature gate.
* lp.int_find_hnf_cube_period (uint, default 16, 0 disables) -- the HNF cube
is invoked every Nth final-check call after a plain cube failure, so its
cost is amortized vs. cube (which has period 4).
Statistics: arith-hnf-cube-{calls,success,bail-collect,bail-build,bail-hnf,
bail-tighten,bail-infeasible}.
Resource limits: rows<=75, cols<=150, bitsize<=4096; bail above.
Validation:
* SMT regression suite: 906/907 (same as baseline; the one failure is
pre-existing and unrelated).
* test-z3 /a: 89/89 unit tests pass.
* CAV-2009 50-instance sample, -T:30: sat=40 (matches baseline) with
1 hnf_cube_success and slightly lower wall time.
* QF_LIA random sample (100 instances), -T:10: sat=64 (matches baseline).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>