Prove2Me

§2, p. 95 — (PR_λ) separates into one binary knapsack per agent

Proved
RossSolandGAP.Bound.lagrangean_separates_into_knapsacks

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

generalized-assignmentinteger-programmingknapsacklagrangean-relaxationp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix multipliers λj\lambda_j. For every xx the objective of (PRλ_\lambda) can be written

∑i∈I∑j∈Jcijxij+∑j∈Jλj(1−∑i∈Ixij)=∑j∈Jλj−∑i∈I∑j∈J(λj−cij)xij.\sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)=\sum_{j\in J}\lambda_j-\sum_{i\in I}\sum_{j\in J}(\lambda_j-c_{ij})x_{ij}.

Moreover, a point xx feasible for (PRλ_\lambda) is optimal for (PRλ_\lambda) if and only if, for every agent ii, the row (xij)j∈J(x_{ij})_{j\in J} is optimal for agent ii's binary knapsack problem

max⁡ ∑j∈J(λj−cij)vjs.t.∑j∈Jrijvj≤bi,vj∈{0,1}.\max\ \sum_{j\in J}(\lambda_j-c_{ij})v_j\quad\text{s.t.}\quad \sum_{j\in J}r_{ij}v_j\le b_i,\quad v_j\in\{0,1\}.

So the optimal value of (PRλ_\lambda) is ∑jλj\sum_j\lambda_j minus the sum over agents of their knapsack optima: (PRλ_\lambda) separates into a series of binary knapsack problems, one for each i∈Ii\in I.

Formalization Note The paper writes the "equivalent form of the objective function" as ∑jλj−max⁡[∑j∑i(λj−cij)xij]\sum_j\lambda_j-\max[\sum_j\sum_i(\lambda_j-c_{ij})x_{ij}]; the max⁡\max belongs to the optimal value, not to the objective of a single point. The statement gives the pointwise identity and the separation of optimal solutions, which together give the optimal-value form.

Preamble
import Mathlib
import Definitions.Def_RossSolandGAP_Bound_Model
open Finset
Formal statement
namespace RossSolandGAP.Bound

theorem lagrangean_separates_into_knapsacks {m n : ℕ} (c r : Fin m → Fin n → ℝ)
    (b : Fin m → ℝ) (lam : Fin n → ℝ) :
    (∀ x, lagObj c lam x = ∑ j, lam j - ∑ i, knapObj c lam i (x i)) ∧
    ∀ x, FeasibleLag r b x →
      ((∀ x', FeasibleLag r b x' → lagObj c lam x ≤ lagObj c lam x') ↔
        ∀ i v, KnapFeasible r b i v → knapObj c lam i v ≤ knapObj c lam i (x i)) := by sorry

end RossSolandGAP.Bound
Source
Ross & Soland, A Branch and Bound Algorithm for the Generalized Assignment Problem, Mathematical Programming 8, 1975, p. 95, §2, the display after (PR_λ) and the sentence 'Thus (PR_λ) separates into a series of binary knapsack problems, one for each i ∈ I.'
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph