Theorem Knapsack Relaxations And Dynamic Programming

✓ theorem proved

Lean declarations

def KnapsackAuction.fractionalSocialWelfare EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack
Fractional social welfare for a `U`-valued allocation vector.
```
def fractionalSocialWelfare (b : I → U) (x : I → U) : U :=
  ∑ i, b i * x i
```

def KnapsackAuction.fractionalFeasible EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

def fractionalFeasible (A : KnapsackAuction I U) (x : I → U) : Prop :=
  (∀ i, 0 ≤ x i ∧ x i ≤ 1) ∧
    (∑ i, A.weight i * x i) ≤ A.totalCapacity

def KnapsackAuction.fractionalGreedyAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

noncomputable def fractionalGreedyAllocation
    (A : KnapsackAuction I U) (b : I → U) : I → U :=
  A.fractionalGreedyList b (A.sortedAgentsByRatio b) A.totalCapacity

theorem KnapsackAuction.fractionalGreedyWelfare_ge_zeroOneWelfare_of_optimal EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

theorem fractionalGreedyWelfare_ge_zeroOneWelfare_of_optimal
    (A : KnapsackAuction I U) (b : I → U) (hW : 0 ≤ A.totalCapacity)
    (hgreedyOptimal :
      ∀ x : I → U, A.fractionalFeasible x →
        fractionalSocialWelfare b x ≤
          fractionalSocialWelfare b (A.fractionalGreedyAllocation b)) :
    A.maximalSocialWelfare b hW ≤
      fractionalSocialWelfare b (A.fractionalGreedyAllocation b)

def KnapsackAuction.dpSolveList EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

def dpSolveList (w b : I → Nat) : List I → Nat → BinaryAllocation I
  | [], _ => fun _ => false
  | i :: is, capacity =>
      if w i ≤ capacity then
        let skip

def KnapsackAuction.dynamicProgrammingOptimalAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

noncomputable def dynamicProgrammingOptimalAllocation
    (w b : I → Nat) (capacity : Nat) : BinaryAllocation I :=
  dpSolveList w b ((Finset.univ : Finset I).toList) capacity

def KnapsackAuction.dynamicProgrammingOptimalValue EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack
The social welfare achieved by the dynamic-programming allocation.
```
noncomputable def dynamicProgrammingOptimalValue
    (w b : I → Nat) (capacity : Nat) : Nat :=
  natBinarySocialWelfare b (dynamicProgrammingOptimalAllocation w b capacity)
```

theorem KnapsackAuction.dynamicProgrammingOptimalAllocation_feasible EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

theorem dynamicProgrammingOptimalAllocation_feasible
    (w b : I → Nat) (capacity : Nat) :
    natBinaryLoad w (dynamicProgrammingOptimalAllocation w b capacity) ≤ capacity

theorem KnapsackAuction.dynamicProgrammingOptimalAllocation_optimal EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

theorem dynamicProgrammingOptimalAllocation_optimal
    (w b : I → Nat) (capacity : Nat) {x : BinaryAllocation I}
    (hfeas : natBinaryLoad w x ≤ capacity) :
    natBinarySocialWelfare b x ≤
      natBinarySocialWelfare b (dynamicProgrammingOptimalAllocation w b capacity)

def KnapsackAuction.integralGreedyAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

The ratio-sorted integral greedy allocation.

noncomputable def integralGreedyAllocation (w b : I → Nat) (capacity : Nat) : BinaryAllocation I :=
  integralGreedyList w ((natAuctionData w capacity).sortedAgentsByRatio (realBidOfNat b)) capacity

def KnapsackAuction.integralGreedyValue EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack
Welfare of the ratio-sorted integral greedy allocation.
```
noncomputable def integralGreedyValue (w b : I → Nat) (capacity : Nat) : Nat :=
  natBinarySocialWelfare b (integralGreedyAllocation w b capacity)
```

def KnapsackAuction.natFractionalGreedyAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

The ratio-sorted fractional greedy allocation on natural-number data.

noncomputable def natFractionalGreedyAllocation (w b : I → Nat) (capacity : Nat) : I → ℝ :=
  natFractionalGreedyList w ((natAuctionData w capacity).sortedAgentsByRatio (realBidOfNat b)) capacity

def KnapsackAuction.natFractionalGreedyValue EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

Welfare of the ratio-sorted fractional greedy allocation.

noncomputable def natFractionalGreedyValue (w b : I → Nat) (capacity : Nat) : ℝ :=
  fractionalSocialWelfare (realBidOfNat b) (natFractionalGreedyAllocation w b capacity)

lemma KnapsackAuction.dynamicProgrammingOptimalAllocation_fractionalFeasible EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

lemma dynamicProgrammingOptimalAllocation_fractionalFeasible
    (w b : I → Nat) (capacity : Nat) :
    (natAuctionData w capacity).fractionalFeasible
      (binaryToAllocation (dynamicProgrammingOptimalAllocation w b capacity))

theorem KnapsackAuction.integralGreedy_halfApprox_dpOptimal EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Knapsack

theorem integralGreedy_halfApprox_dpOptimal
    (w b : I → Nat) (capacity : Nat)
    (hwpos : ∀ i, 0 < w i)
    (_hallfit : ∀ i, w i ≤ capacity)
    (hfracOptimal :
      ∀ x : I → ℝ, (natAuctionData w capacity).fractionalFeasible x →
        fractionalSocialWelfare (realBidOfNat b) x ≤
          natFractionalGreedyValue w b capacity) :
    ((dynamicProgrammingOptimalValue w b capacity : ℝ) / 2) ≤
      max (integralGreedyValue w b capacity) (highestBidValue b)

Modules: EconCSLib.MechanismDesign.Auction.Knapsack

Knapsack Relaxations And Dynamic Programming

This node assembles the algorithmic layer of the knapsack auction ([[mechanism_design.auction.knapsack.environment]]): the fractional LP relaxation, the integer dynamic-programming solver, the integral greedy rule, and their quantitative comparisons.

The headline result is a $1/2$-approximation: the integral greedy allocation achieves at least half the welfare of the dynamic-programming optimum.

Fractional relaxation

The LP relaxation drops the 0/1 constraint to $x_i \in [0, 1]$ while keeping the same capacity and welfare:

fractionalSocialWelfare b x : ℝ — the welfare functional applied to a real-valued allocation profile $x : I \to \mathbb{R}$: $\sum_i b_i x_i$.
fractionalFeasible A x — the LP feasibility predicate: $\forall i.\; 0 \le x_i \le 1$ together with $\sum_i w_i x_i \le W$.
fractionalGreedyAllocation A b — the value-density greedy LP solution: sort agents by $b_i / w_i$ in decreasing order, fill capacity, then split the last fractional agent. This is the classical greedy LP optimiser for the fractional knapsack.

The first bridge inequality fractionalGreedyWelfare_ge_zeroOneWelfare_of_optimal establishes that the fractional greedy welfare upper-bounds the integral welfare-maximising 0/1 objective: $$ \mathrm{fractionalSocialWelfare}(b, \mathrm{fractionalGreedyAllocation}(A, b)) \;\ge\; \mathrm{binarySocialWelfare}(b, x^*(b)), $$ i.e. the LP optimum dominates the IP optimum (the standard LP relaxation gap inequality, but explicit on the greedy LP solver).

Dynamic programming (integer 0/1)

For the natural-number specialisation (weights and capacity are nonnegative integers), an explicit dynamic-programming solver:

dpSolveList — table-based DP that runs over a list of items, returning per-capacity optimal selections.
dynamicProgrammingOptimalAllocation A b — the BinaryAllocation reconstructed from the DP table.
dynamicProgrammingOptimalValue A b — the DP objective value.
dynamicProgrammingOptimalAllocation_feasible — the DP output respects the capacity constraint.
dynamicProgrammingOptimalAllocation_optimal — the DP output attains the maximum of binarySocialWelfare b over the feasible 0/1 search space.
dynamicProgrammingOptimalAllocation_fractionalFeasible — bridge lemma certifying that the DP allocation, viewed as a real-valued allocation via binaryToAllocation, is fractionalFeasible.

Combined, these lemmas verify that the DP solver is a correct algorithm for the integer knapsack: it produces the unique-up-to-ties optimum of the same combinatorial problem solved abstractly by [[mechanism_design.auction.knapsack.welfare_maximizing_mechanism]], but constructively and in pseudo-polynomial time.

Integral greedy and the half-approximation

integralGreedyAllocation — round the fractional greedy solution to 0/1 by dropping the split agent.
integralGreedyValue — the welfare of the integral greedy allocation.
natFractionalGreedyAllocation, natFractionalGreedyValue — the natural-number specialisations used in the comparison with the DP optimum.

The headline approximation guarantee is:

Theorem (integralGreedy_halfApprox_dpOptimal). Under the standard sign hypotheses on weights, capacity, and bids, $$ \mathrm{dpOptimalValue}(A, b) \;\le\; 2 \cdot \mathrm{integralGreedyValue}(A, b), $$ i.e. the integral greedy rule achieves at least $1/2$ of the optimal integer welfare.

Proof sketch

The LP optimum upper-bounds the integer optimum (fractionalGreedyWelfare_ge_zeroOneWelfare_of_optimal). The LP optimum is bounded by twice the better of two integer feasible allocations: "the integral greedy prefix" and "the single best item alone". The half-approximation then follows by triangle inequality, taking the better of the two as integralGreedyValue.

Position in the library

These results are the algorithmic counterpart to the truthfulness story in [[mechanism_design.auction.knapsack.welfare_maximizing_mechanism]]: the abstract welfare maximiser is replaced by a constructive (DP) or approximation (integral greedy) algorithm, and the approximation is quantified explicitly. In Myerson terms, both algorithms induce monotone allocation rules (in the value parameter), so they can in principle be combined with Myerson payments to produce DSIC approximation mechanisms in the spirit of AGT Chapter 12.

References

[AGT, Chapter 12, Sections 12.1-12.3] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Fractional LP relaxation, dynamic-programming solvers, and integral greedy half-approximation for single-parameter approximation mechanisms.
[AGT, Chapter 11, Section 11.2] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Greedy allocation rules, critical payments, and approximation analysis in combinatorial auctions.
[Vazirani 2001, Chapter 8] Vijay Vazirani, Approximation Algorithms. Classical $1/2$- and FPTAS-style analyses for the 0/1 knapsack problem.

Provenance

Migrated from EconCSLib pull request 27, old blueprint label thm:auction_knapsack_algorithms in blueprint/src/content.tex.