[Rule] ILP/i32 to ILP/bool

[isPANN]

Source

ILP/i32 (Integer Linear Programming with non-negative integer variables)

Target

ILP/bool (Integer Linear Programming with binary variables)

Motivation

ILP/i32 is a dead-end node with 0 outgoing reductions and 27 incoming reductions. This reduction connects ILP/i32 to ILP/bool, which has paths to QUBO — making all 27 upstream problems transitively solvable via quantum annealing.

The reduction uses truncated binary encoding with automatic Feasibility-Based Bound Tightening (FBBT) to infer per-variable upper bounds from constraints. No changes to the ILP model or upstream reductions are needed.

Reference

• Achterberg, Bixby, Gu, Rothberg & Weninger (2020). "Presolve Reductions in Mixed Integer Programming." INFORMS Journal on Computing, 32(2), 473–506. — Comprehensive catalog of presolve techniques including FBBT.
• Savelsbergh (1994). "Preprocessing and Probing Techniques for Mixed Integer Programming Problems." ORSA Journal on Computing, 6(4), 445–454. — Foundational paper on MIP presolve.
• Belotti, Lee, Liberti, Margot & Wächter (2009). "Branching and Bounds Tightening Techniques for Non-convex MINLP." Optimization Methods and Software, 24(4–5), 597–634. — FBBT and OBBT in detail.
• Glover, Kochenberger & Du (2019). "Quantum Bridge Analytics I: A Tutorial on Formulating and Using QUBO Models." Annals of Operations Research, 314, 141–183. — Binary expansion for QUBO.
• Karimi & Rosenberg (2017). "Practical integer-to-binary mapping for quantum annealers." Quantum Information Processing, 16, 166. — Truncated binary encoding.

Reduction Algorithm

Given an ILP/i32 instance with n non-negative integer variables x₀, ..., x_{n−1}, m constraints, a linear objective, and an optimization sense.

Step 0: Bound inference via FBBT

Feasibility-Based Bound Tightening (Savelsbergh 1994, Achterberg et al. 2020) — the standard MIP presolve algorithm used by SCIP, Gurobi, and CPLEX.

Core idea: For a constraint Σ aₖxₖ ≤ b, the maximum value of aᵢxᵢ is bounded by b minus the minimum possible value of all other terms. With all variables non-negative, positive-coefficient terms contribute 0 at minimum, and negative-coefficient terms contribute their most negative value (using the variable's current upper bound).

Algorithm:

Initialize: L[i] = 0, U[i] = +∞ for all i

Repeat (at most n + 1 iterations):
  changed = false
  For each constraint (terms, sense, rhs):
    Compute activity bounds:
      act_min = Σ_k (a_k > 0 ? a_k * L[k] : a_k * U[k])
      act_max = Σ_k (a_k > 0 ? a_k * U[k] : a_k * L[k])

    Infeasibility check:
      If sense=Le and act_min > rhs: INFEASIBLE
      If sense=Ge and act_max < rhs: INFEASIBLE

    For each variable x_i with coefficient a_i:
      // Residual = activity without x_i's contribution
      my_min = (a_i > 0 ? a_i * L[i] : a_i * U[i])
      res_min = act_min - my_min

      my_max = (a_i > 0 ? a_i * U[i] : a_i * L[i])
      res_max = act_max - my_max

      // From Le constraint (or Eq):
      If sense ∈ {Le, Eq} and res_min is finite:
        If a_i > 0: new_U = ⌊(rhs - res_min) / a_i⌋
                    If new_U < U[i]: U[i] = new_U, changed = true
        If a_i < 0: new_L = ⌈(rhs - res_min) / a_i⌉
                    If new_L > L[i]: L[i] = new_L, changed = true

      // From Ge constraint (or Eq):
      If sense ∈ {Ge, Eq} and res_max is finite:
        If a_i > 0: new_L = ⌈(rhs - res_max) / a_i⌉
                    If new_L > L[i]: L[i] = new_L, changed = true
        If a_i < 0: new_U = ⌊(rhs - res_max) / a_i⌋
                    If new_U < U[i]: U[i] = new_U, changed = true

      If L[i] > U[i]: INFEASIBLE

  If not changed: break

If any U[i] = +∞: return UNBOUNDED error

Properties:

• Complexity: O(nnz × iterations), typically 2–5 iterations
• Guaranteed termination: bounds only tighten, integer steps ≥ 1
• Handles all constraint types (Le, Ge, Eq) and mixed-sign coefficients
• Iteration handles chains (e.g., z ≤ x, x ≤ n−1 → z ≤ n−1 after 2 passes)
• Implementation note: use saturating arithmetic for +∞ sentinel values; use floor_div/ceil_div that round toward −∞/+∞ (not truncation toward zero)

Why FBBT suffices for this codebase: All 27 ILP/i32 reductions produce instances with explicit capacity/bound constraints or all-positive-coefficient aggregates. FBBT finds finite bounds in all cases. If it fails (returns UNBOUNDED), the upstream reduction is missing a bound constraint and should be fixed.

Step 1: Truncated binary encoding

For each variable xᵢ with inferred bound Uᵢ:

• Let Kᵢ = ⌈log₂(Uᵢ + 1)⌉
• Create Kᵢ binary variables y_{i,0}, ..., y_{i,Kᵢ−1}
• Weights: w_{i,j} = 2ʲ for j < Kᵢ − 1, and w_{i,Kᵢ−1} = Uᵢ − 2^{Kᵢ−1} + 1
• Substitution: xᵢ = Σⱼ w_{i,j} · y_{i,j}

The last weight is adjusted so the maximum representable value is exactly Uᵢ (Karimi & Rosenberg 2017). When Uᵢ = 2^Kᵢ − 1, no adjustment needed.

Total binary variables: N = Σᵢ Kᵢ.

Step 2: Transform constraints

For each constraint Σₖ aₖ · xₖ {≤, ≥, =} b, substitute xₖ = Σⱼ w_{k,j} · y_{k,j}. Each term aₖ · xₖ becomes Kₖ terms with coefficients aₖ · w_{k,j}.

Step 3: Transform objective

For each objective term cₖ · xₖ, substitute to get Kₖ terms: cₖ · w_{k,j} · y_{k,j}.

Step 4: Preserve sense

Optimization direction is unchanged.

Solution extraction

Given binary solution (y_{i,j}), recover xᵢ = Σⱼ w_{i,j} · y_{i,j}.

Correctness Argument

FBBT correctness: Each bound tightening is sound — it only removes values that are provably infeasible under the given constraint. Therefore any feasible solution to the original ILP satisfies the inferred bounds.

Encoding correctness: The truncated binary encoding is a bijection between [0, Uᵢ] and Kᵢ-bit patterns. Maximum: Σⱼ w_{i,j} = (2^{Kᵢ−1} − 1) + (Uᵢ − 2^{Kᵢ−1} + 1) = Uᵢ. Every feasible integer assignment has a unique binary encoding, and vice versa. Objective values are preserved exactly.

Size Overhead

Target metric	Formula
num_vars	Σᵢ ⌈log₂(Uᵢ + 1)⌉ where Uᵢ = FBBT-inferred bound
num_constraints	num_constraints (unchanged)

Validation Method

Closed-loop test: construct a small ILP/i32 instance with tight bounds (variables bounded ≤ 10), reduce to ILP/bool, solve with BruteForce, extract solution, verify optimality matches brute-force on the original ILP/i32. Total binary variables must stay ≤ 16.

Example

Source (ILP/i32): Minimize −5x₀ − 6x₁, subject to x₀ + x₁ ≤ 5, 4x₀ + 7x₁ ≤ 28.

FBBT trace:

• Init: L = [0, 0], U = [∞, ∞]
• Pass 1, constraint 1 (x₀ + x₁ ≤ 5):
  • x₀: res_min = 0, new_U = ⌊5/1⌋ = 5 → U₀ = 5
  • x₁: res_min = 0, new_U = ⌊5/1⌋ = 5 → U₁ = 5
• Pass 1, constraint 2 (4x₀ + 7x₁ ≤ 28):
  • x₀: res_min = 0, new_U = ⌊28/4⌋ = 7 → no change (7 > 5)
  • x₁: res_min = 0, new_U = ⌊28/7⌋ = 4 → U₁ = 4
• Pass 2: no changes → converged.
• Result: U = [5, 4]

Binary expansion:

• x₀ ∈ [0, 5]: K₀ = 3, weights = (1, 2, 2). x₀ = y₀ + 2y₁ + 2y₂.
• x₁ ∈ [0, 4]: K₁ = 3, weights = (1, 2, 1). x₁ = y₃ + 2y₄ + y₅.

Target (ILP/bool): 6 binary variables.

• Objective: minimize −5y₀ − 10y₁ − 10y₂ − 6y₃ − 12y₄ − 6y₅
• Constraint 1: y₀ + 2y₁ + 2y₂ + y₃ + 2y₄ + y₅ ≤ 5
• Constraint 2: 4y₀ + 8y₁ + 8y₂ + 7y₃ + 14y₄ + 7y₅ ≤ 28

Solution: y = (1, 1, 0, 0, 1, 0) → x₀ = 3, x₁ = 2. Objective = −27. ✅

Search space: 2⁶ = 64 configs (brute-force feasible), vs 2⁶² with naive 31-bit expansion.

BibTeX

@article{Achterberg2020,
  author  = {Achterberg, Tobias and Bixby, Robert E. and Gu, Zonghao and Rothberg, Edward and Weninger, Dieter},
  title   = {Presolve Reductions in Mixed Integer Programming},
  journal = {INFORMS Journal on Computing},
  volume  = {32},
  number  = {2},
  pages   = {473--506},
  year    = {2020},
  doi     = {10.1287/ijoc.2018.0857}
}
@article{Savelsbergh1994,
  author  = {Savelsbergh, Martin W. P.},
  title   = {Preprocessing and Probing Techniques for Mixed Integer Programming Problems},
  journal = {ORSA Journal on Computing},
  volume  = {6},
  number  = {4},
  pages   = {445--454},
  year    = {1994},
  doi     = {10.1287/ijoc.6.4.445}
}
@article{Belotti2009,
  author  = {Belotti, Pietro and Lee, Jon and Liberti, Leo and Margot, Fran{\c{c}}ois and W{\"a}chter, Andreas},
  title   = {Branching and Bounds Tightening Techniques for Non-convex {MINLP}},
  journal = {Optimization Methods and Software},
  volume  = {24},
  number  = {4--5},
  pages   = {597--634},
  year    = {2009},
  doi     = {10.1080/10556780903087124}
}
@article{Glover2019,
  author  = {Glover, Fred and Kochenberger, Gary and Du, Yu},
  title   = {Quantum Bridge Analytics {I}: A Tutorial on Formulating and Using {QUBO} Models},
  journal = {Annals of Operations Research},
  volume  = {314},
  pages   = {141--183},
  year    = {2019},
  doi     = {10.1007/s10479-022-04634-2}
}
@article{Karimi2017,
  author  = {Karimi, Sahar and Rosenberg, Gili},
  title   = {Practical integer-to-binary mapping for quantum annealers},
  journal = {Quantum Information Processing},
  volume  = {16},
  pages   = {166},
  year    = {2017},
  doi     = {10.1007/s11128-017-1620-6}
}

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing path ILP/i32 → ILP/bool; unlocks QUBO access for 27+ upstream problems
Non-trivial	✅ Pass	FBBT bound inference + truncated binary encoding is a substantial algorithmic transformation
Correctness	✅ Pass	All references verified; algorithm is well-established (SCIP/Gurobi presolve); both ILP/i32 and ILP/bool exist
Well-written	✅ Pass	Complete, detailed, implementable; all sections present with correct notation

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

pred path ILP/i32 ILP/bool returns "no path." ILP/i32 currently has 0 outgoing reductions and 28 incoming reductions — it is a dead-end node. ILP/bool has a path to QUBO/f64. This single reduction would transitively enable all 28 upstream problems (FlowShopScheduling, OptimalLinearArrangement, SteinerTree, TravelingSalesman, etc.) to reach QUBO, unlocking quantum annealing solvers. This is extremely high-value. Pass.

Non-trivial

The reduction involves two distinct algorithmic components:

1. FBBT (Feasibility-Based Bound Tightening): An iterative constraint propagation algorithm that infers finite upper bounds on integer variables from the constraint system. This is a standard MIP presolve technique with non-trivial convergence analysis.
2. Truncated binary encoding: Converts bounded integer variables to binary using adjusted weights for the most significant bit. This is more than a simple binary expansion — the truncation ensures exact representability of the bound.

Neither component is a relabeling or identity transformation. Pass.

Correctness

• Both models exist: ILP/i32 ✅ (28 incoming reductions, 0 outgoing). ILP/bool ✅ (58 incoming, 2 outgoing including QUBO/f64).
• References verified:
  • Achterberg et al. (2020), "Presolve Reductions in Mixed Integer Programming," INFORMS JoC 32(2) — real paper, DOI 10.1287/ijoc.2018.0857 ✅
  • Savelsbergh (1994), "Preprocessing and Probing Techniques for MIP," ORSA JoC 6(4) — foundational presolve paper ✅
  • Karimi & Rosenberg (2017), "Practical integer-to-binary mapping for quantum annealers," QIP 16:166 — truncated binary encoding ✅
  • Glover, Kochenberger & Du (2019), "Quantum Bridge Analytics I" — QUBO formulation reference ✅
  • Belotti et al. (2009), "Branching and Bounds Tightening Techniques for Non-convex MINLP" — FBBT reference ✅
• Algorithm soundness: FBBT is a well-studied technique used in production solvers. The pseudocode handles Le/Ge/Eq constraints, positive and negative coefficients, and includes infeasibility detection. The truncated binary encoding preserves the feasible set exactly. The correctness argument (bijection between [0,U_i] and K_i-bit patterns) is valid.
• Overhead check: num_vars = sum of ceil(log2(U_i + 1)) is data-dependent (depends on FBBT-inferred bounds, not just source size fields). num_constraints = unchanged. The issue acknowledges this correctly — the overhead is instance-dependent, which is unusual but acceptable since the bound inference is deterministic.

Well-written

Sections present: Source ✅, Target ✅, Motivation ✅, Reference ✅, Reduction Algorithm ✅ (with detailed FBBT pseudocode), Size Overhead ✅, Validation Method ✅, Example ✅, Correctness Argument ✅, BibTeX ✅.

Quality highlights:

• The FBBT algorithm is specified in complete pseudocode with convergence guarantee, edge cases, and implementation notes (saturating arithmetic, floor_div/ceil_div).
• The example traces through FBBT iteration-by-iteration and shows the full binary expansion.
• Solution extraction is clearly defined.
• The example produces 6 binary variables (brute-force feasible at 64 configs) vs naive 31-bit expansion.
• Symbol usage is consistent across all sections.

This is an exceptionally well-written issue.

Recommendations

• The overhead num_vars expression is instance-dependent and cannot be expressed purely in terms of source size getters. Consider documenting a worst-case bound (e.g., num_vars <= num_vars * ceil(log2(max_bound + 1))) for the #[reduction(overhead)] macro.