MILP/Gurobi state bounds ignore the input state #69

High: spurious failures. The k and coefficient bounds of the intermediate states (and, for Classic, the bound of states created past the preallocated depth) are derived from the depth only, not from the input vectors. Inputs with k >= 3, coefficients > 2 or only superposition amplitudes make every depth infeasible on MILP/Gurobi, while SMT finds the circuit.

Found in a code review of master at 66b41d9. Every item below was reproduced; the IDs (F1, G2, ...) are the review's.

Items: F4, F19

F4

MILP/Gurobi intermediate-state k and coefficient bounds ignore the input state, so inputs with k >= 3 or coefficients > 2 are infeasible at every depth

Location: src/synth.py:1067 · severity: high

Layer states are declared with k_bound = 2*(d+1) and coefficient bound bounds[d] = 2^(d+1) (lines 1042-1046, 1067/1069), and the states created past self.d use 2*(curr_depth+1) and self.bound (lines 1168/1170). This assumes the input has k = 0 and coefficients <= 1. I__0 is asserted equal to In, so in milp and gurobi, where declared bounds are enforced, any input with k >= 3 or a coefficient > 2 makes the model infeasible at layer 0 and at every later depth. SMT ignores declared bounds and works, so the backends disagree. Reachable inputs: -v jamiolkowski on >= 3 qubits (input k = q), -v rus -T >= 3 (|+>^T has k = T, sim.py:409), custom input_vectors (#44) and vector_pairs. Gurobi is the CLI default backend. Without --max-depth, incremental mode never terminates.

Reproduction. -v jamiolkowski -s milp -a cbc on the 3-qubit circuit t q[0]; returns False; SMT returns t. vectors=custom with input H*SX|0> (k=3) or H T H T H|0>, circuit t or x: Gurobi and CBC return False, yices2 returns the circuit. |+++> input with z q[0] and gate set {z,x}: CBC False. |+> written with k=3: Gurobi/CBC False, yices2 h. An input with k=4 and coefficient 4 still fails after widening only k_bound, because the coefficient bound is also too small.

encode-gates dbg7: jamiolkowski 3-qubit 't q[0]', max_depth=1: smt True [t q[0];]; milp False None; milp with k_bound+10: True [t q[0];]. dbg2/kin.py (k=3 input): smt True [t], gurobi False, cbc False; kin_patch.py (k_bound+10): gurobi True [t]. k=4 SX SX|0> input, only k_bound patched: gurobi False.
numbers/kb: run_kb.py smt -> True [x]; gurobi -> False; cbc -> False; run_kb_patch.py (k_bound += 3) -> True for both.
semantics customk3.py: milp cbc False, yices2 True [z q[0];]; ub=20 for I_*_k -> True.
differential kb.py: |+> with k=1 gurobi True [h]; k=3 gurobi False, smt True, cbc False; k=5 needs the coefficient bound scaled too.

Suggested fix. Bound intermediate states relative to the inputs: k_bound(d) = max_in_k + 2*(d+1) and coefficient bound(d) = max(1, max_in_coeff) * 2^(d+1) (or sqrt2^k_bound from sum coeff^2 = 2^k). Compute both once from the vector pairs and use a single state-declaration helper for the preallocated (1067/1069) and the incremental (1168/1170) states. Add MILP/Gurobi tests with custom inputs of k = 3 and 4 and jamiolkowski on 3 qubits.

F19

Classic states created past the preallocated depth are bounded by the largest input amplitude instead of 1, so MILP/Gurobi cannot go beyond d for superposition inputs

Location: src/synth.py:1170 · severity: medium

self.bound is the largest coefficient of any input vector (synth.py:941-948). For Classic it is never replaced, and incremental mode uses it as the [-bound, bound] range of every state created when curr_depth > self.d (lines 1168/1170), which Gurobi/PuLP enforce. If all inputs are superpositions the bound is < 1 (0.707 for |+>), so outputs with an amplitude of 1 cannot be represented beyond d; the search fails, or loops forever without max_depth. Preallocated states (<= d) use bound 1, which is why d=1 works. SMT ignores declared bounds.

Reproduction. Custom Classic pair |+> -> |0>, gate set {h}, Gurobi incremental: d=1 returns h, d=0 returns False up to max_depth=3. vector_pairs=[(|+>, |1>)], q=1, d=1, gate set {h,x,z}, max_depth=3: yices2 returns h; x, Gurobi and CBC return False.

synth-flow exp_classic_bound.py 0 -> d = 0 res False, self.bound = 0.7071; exp_classic_bound.py 1 -> d = 1 res True [h q[0];].
numbers/cb run_cb.py: smt yices2 True ['h q[0];', 'x q[0];']; gurobi False; milp cbc False; bound used beyond d: 0.7071067811865476.

Suggested fix. For Classic, bound every state amplitude by 1 (unitary evolution of normalised states). Keep self.bound only for FiveTuple coefficient growth (or give the two uses separate attributes) and use one state-declaration helper for preallocated and incremental states (F4).