[jkhav]

Stacked on #88: it reuses pair_k and the per-depth gap bound. Together with #88 this fixes #65 (F1 there, F15 here). F58 continues in #104.

Problem

add_milp_rescaling took its k bound and both big-Ms from Synthesizer.max_k, which is fixed from the input. Past the input depth, and with custom pairs whose k is not reduced, the correct circuit was infeasible. CBC never returned a wrong circuit here; it missed valid ones:

• X from {sx, z}: no sx;sx
• Z from {h, sx}: no h;sx;sx;h
• custom pair |0⟩ → |1⟩ with the target written as a=4, k=4: no x
• custom input with k=6 (a=1): no x

Fix

• Same bound as the SMT side. max_gap = max(k_in + inc·depth − k_target, k_target − k_in) bounds |k1 − k2|. The rescaling k is in [0, max_gap // 2], the parity big-M is 2·max_gap + 1, and the value big-M is B + R, with B the vectors' entry bound and R = 2B·2^(max_gap // 2) the bound of the Rescaled vectors (no longer 2**max_k).
• Stale PuLP bound. In PuLP the bound belongs to the variable. Incremental search redeclares k{pair} at each depth and gets back the first depth's variable, so its ub stayed stale even after pop(). k has no ub now; the one-hot bounds it.
• Intermediate k bound. Inter's k bound was 2·(d+1), ignoring the input's own k. It is k_in + inc·d now. This is the k half of MILP/Gurobi state bounds ignore the input state #69 F4.
• Per-gate increments. inc is the largest k increment in the gate set, from a k_increments table in gates.py. encode_layer reads the same table, so a new gate that raises k must be added there (KeyError otherwise) instead of silently breaking a hardcoded 2. Gate sets without h/sx get a gap of 0 and smaller big-Ms.

Why it is sound

With Δ = k1 − k2, K = ⌊|Δ|/2⌋ and q = |Δ| mod 2, the equality is v1·2^K·√2^q = v2 (or swapped), and √2·(a,b,c,d) = (b−d, a+c, b+d, c−a), as encoded.

• Each layer holds exactly one gate (ExactlyOne), so |Δ| ≤ max_gap and K ≤ max_gap // 2. A larger gap is infeasible, never unconstrained.
• Parity rows: the relaxed side reaches 2|Δ| ≤ 2·max_gap. The active side forces 2k + q = |Δ|; lb=0 rules out the wrong sleq.
• Value rows: an inactive row is at most c·|expr| + R, with c ≤ 2^(max_gap // 2) and |expr| ≤ 2B. The row multipliers in constrained_rescaling (2·tmp, 2c·tmp, 3c·tmp, with tmp = B + R) cover each case.

This holds in exact arithmetic. MILP solvers accept values within a tolerance, so very large big-Ms are a numerical risk; that is #104.

Testing

• New tests in tests/test_rescaling_bound.py: the four MILP cases above (all fail on Bound the FiveTuple rescaling by the encoded depth, in SMT and MILP (#65) #88's branch), and max_k_increment for four gate sets.
• Full suite: 484 passed.
• The rescaling on its own vs exact values: a script builds only add_milp_rescaling with fixed vectors and compares CBC's feasibility with complex-float ground truth from the definition. 1,848 solves (630 equal pairs, 870 not), with tight, off-by-one-parity and loose max_gap, plus too-small bounds that must be infeasible: 0 mismatches. As a check on the checker, a parity big-M of 2·max_gap − 1 gives 58 mismatches and a value big-M of (B+R)/4 gives 11.
• still needs benchmarking to compare the times after changing big M

Not in this PR

• MILP FiveTuple equivalence relies on big-M rows that solver tolerances can relax #104: numerical robustness of the big-M rows (F58), including PuLP's Gurobi backend running with Gurobi's default IntFeasTol of 1e-5.
• MILP/Gurobi state bounds ignore the input state #69, MILP big-M constants are too small, so CBC results are not gate-count optimal #68: custom inputs with large entries (e.g. a=4, k=4) are still infeasible in MILP, because of the coefficient bound of the intermediate states (MILP/Gurobi state bounds ignore the input state #69 F4) and the per-layer big-M (MILP big-M constants are too small, so CBC results are not gate-count optimal #68 F5), not the rescaling. This PR fixes the k half of MILP/Gurobi state bounds ignore the input state #69 F4.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[ondrik]

Consolidated into #88 at @ondrik's request: this PR's commit is now on #88's branch, rebased onto master, and #88's description includes this one. While rebasing, the MILP test for Z from {h, sx} failed again, because since #67 the target's Rescaled2 vector was first declared at depth 0, with the smallest bound; #88's last commit names it per depth. Closing this one in favour of #88.

🤖 Generated with Claude Code

https://claude.ai/code/session_0177AhE9SXm3iJ1KP8GTSk6o