Theorem 3.2 — clause-based rounding is a $1/(1-(1-1/n)^n)$ -approximation for XOS bidders

Proved

ComplementFreeCA.XOSRounding.xos_rounding_approximation

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

approximation-algorithmscombinatorial-auctionsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1randomized-roundingxos-valuations

Consider a combinatorial auction with $n\ge1$ bidders and items $M=\{1,\dots,m\}$ , in which every bidder $i$ has an XOS valuation $v_i$ given by an admissible clause set $W_i$ (nonnegative clause values). Let $x$ be an optimal solution of the LP relaxation. The algorithm of §3.2

draws a preallocation $S_1,\dots,S_n$ by randomized rounding from $x$ ;
lets $p^i=\mathrm{cl}_i(S_i)$ be the maximizing clause for $S_i$ in $v_i$ ;
allocates each item $j$ to a bidder $i$ with $p^i_j\ge p^{i'}_j$ for all $i'\in N$ .

Let $\mathrm{ALG}$ be the welfare of the resulting allocation. Then, for every XOS oracles $\mathrm{cl}_i$ , every tie-breaking in step 3 and every allocation $(O_1,\dots,O_n)$ ,

\Big(1-\Big(1-\frac1n\Big)^n\Big)\sum_{i}v_i(O_i)\ \le\ \mathbb E[\mathrm{ALG}] .

That is, the algorithm is a $1/(1-(1-1/n)^n)$ -approximation to the optimal allocation; the ratio is at most $e/(e-1)$ .

Formalization Note The algorithm is randomized, and "approximation" is read in expectation over the rounding, as the paper's proof establishes. The expectation is the finite sum over preallocation profiles with independent per-bidder laws. The goal quantifies over every XOS oracle and every highest-clause tie-breaking rule. Running time and oracle access are out of scope.

Preamble

import Mathlib
import Definitions.Def_ComplementFreeCA_XOSRounding_Model
import Definitions.Def_ComplementFreeCA_XOSRounding_Rounding
import Definitions.Def_ComplementFreeCA_XOSRounding_Algorithm

Formal statement

namespace ComplementFreeCA.XOSRounding

theorem xos_rounding_approximation {n m : ℕ} (hn : 0 < n)
    (W : Fin n → Finset (Fin m → ℝ)) (v : Fin n → Finset (Fin m) → ℝ)
    (hv : ∀ i, IsXOSWith (v i) (W i))
    (cl : Fin n → Finset (Fin m) → Fin m → ℝ) (hcl : ∀ i, IsXOSOracle (v i) (W i) (cl i))
    (win : (Fin n → Finset (Fin m)) → Fin m → Fin n) (hwin : IsHighestClauseRule cl win)
    (x : Fin n → Finset (Fin m) → ℝ) (hx : IsLPOptimal v x)
    (O : Fin n → Finset (Fin m)) (hO : IsAllocation O) :
    (1 - (1 - 1 / (n : ℝ)) ^ n) * welfare v O ≤
      roundingExpectation x (algWelfare v win) := by sorry

end ComplementFreeCA.XOSRounding

Source

Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, p. 7, §3.2, Theorem 3.2

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 3.2 — clause-based rounding is a 1/(1−(1−1/n)n)1/(1-(1-1/n)^n)1/(1−(1−1/n)n)-approximation for XOS bidders

Theorem 3.2 — clause-based rounding is a $1/(1-(1-1/n)^n)$ -approximation for XOS bidders