§2, p. 96 — at λ_j = c_2j agent i's subproblem on the (PR) pattern has value −Σ_{J_i} p_j + z*_i

Proved

RossSolandGAP.Bound.agent_subproblem_value

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

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

Let $m\ge2$ , let $j\mapsto i_j$ be a cheapest-agent selection and use the notation $J_i$ , $I'$ , $d_i$ , $p_j$ , $c_{2j}$ and (PK $_i$ ) of the paper. Fix an agent $i$ and consider agent $i$ 's part of (PR $_\lambda$ ) at $\lambda=c_2$ , restricted to the (PR) pattern:

\min\ \sum_{j\in J}(c_{ij}-c_{2j})v_j\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}v_j\le b_i,\ v_j\in\{0,1\},\ v_j=0\text{ if }i_j\ne i .

If $i\in I'$ and $y^*_i$ is an optimal solution of (PK $_i$ ) with value $z^*_i$ , the minimum is $-\sum_{j\in J_i}p_j+z^*_i$ (a lower bound on every feasible $v$ , attained by some feasible $v$ ).
If $i\notin I'$ , the minimum is $-\sum_{j\in J_i}p_j$ (attained at $v_j=1$ on $J_i$ ).

Summed over agents and added to $\sum_jc_{2j}$ , this gives $\sum_j c_{i_jj}+\sum_{i\in I'}z^*_i=\mathrm{LB}$ . It is the step "solving (PR) and subsequently solving (PK $_i$ ) for all $i\in I'$ yields a bound equal to that provided by (PR $_\lambda$ )".

Formalization Note $z^*_i$ is the (PK $_i$ ) objective of a given optimal solution y. Agents and tasks are 0-based.

Preamble

import Mathlib
import Definitions.Def_RossSolandGAP_Bound_Model
open Finset

Formal statement

namespace RossSolandGAP.Bound

theorem agent_subproblem_value {m n : ℕ} (hm : 1 < m) (c r : Fin m → Fin n → ℝ)
    (b : Fin m → ℝ) (a : Fin n → Fin m) (ha : IsCheapest c a) (i : Fin m) :
    (i ∈ Iprime r b a → ∀ y, IsOptPK hm c r b a i y →
      (∀ v, KnapFeasible r b i v → (∀ j, a j ≠ i → v j = 0) →
        -(∑ j ∈ Jset a i, pen hm c a j) + pkObj hm c a i y ≤
          ∑ j, (c i j - c2 hm c a j) * v j) ∧
      ∃ v, KnapFeasible r b i v ∧ (∀ j, a j ≠ i → v j = 0) ∧
        ∑ j, (c i j - c2 hm c a j) * v j =
          -(∑ j ∈ Jset a i, pen hm c a j) + pkObj hm c a i y) ∧
    (i ∉ Iprime r b a →
      (∀ v, KnapFeasible r b i v → (∀ j, a j ≠ i → v j = 0) →
        -(∑ j ∈ Jset a i, pen hm c a j) ≤ ∑ j, (c i j - c2 hm c a j) * v j) ∧
      ∃ v, KnapFeasible r b i v ∧ (∀ j, a j ≠ i → v j = 0) ∧
        ∑ j, (c i j - c2 hm c a j) * v j = -(∑ j ∈ Jset a i, pen hm c a j)) := by sorry

end RossSolandGAP.Bound

Source

Ross & Soland, A Branch and Bound Algorithm for the Generalized Assignment Problem, Mathematical Programming 8, 1975, p. 96, §2, second paragraph, second and third sentences

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