← back to the atlas

Price of Anarchy in a Double-Sided Critical Distribution System (aamas23-00075)

Answer: \(\mathrm{P}\): polynomial-time solvable in \(m,\tau,L\) by exact rational linear programming.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateMaximum clearing allocation with average bids can be found efficiently using a linear program.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given finite buyer types \(B\) and seller types \(S\) with rational masses \(\mu_b,\nu_s\), per-agent Good supplies \(q_s\), demands \(d_b\), initial Rights \(r_b^0\), Right capacities, and fixed Good- and Right-bid/ask parameters, choose aggregate Good flows \(x_{bs}\ge0\) and non-self Right flows \(y_{ab}\ge0\), with \(y_{bb}=0\), maximizing \(G=\sum_{b\in B}\sum_{s\in S}x_{bs}\), subject to \(\sum_bx_{bs}\le\nu_sq_s\), \(\sum_sx_{bs}\le\mu_bd_b\), mass-scaled Right capacities, \(\mu_br_b^0-\sum_ay_{ba}+\sum_ay_{ab}\ge G_b\), \(\sum_ay_{ab}\le G_b\), and the average-price constraints \(\sum_sa_s^Gx_{bs}\le p_b^GG_b\) and \(\sum_aa_a^Ry_{ab}\le p_b^RH_b\), where \(G_b=\sum_sx_{bs}\) and \(H_b=\sum_ay_{ab}\).

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: disjoint, nonempty lists of buyer types \(B\) and seller types \(S\), each with a positive binary-rational mass \(\mu_b\) or \(\nu_s\), with \(\sum_b\mu_b+\sum_s\nu_s=1\). Set \(\tau=|B|+|S|\) and \(m=|S|\); \(\tau\) counts supported types, not possible types. Let \(L\) be the total input bit length.
There is one divisible Good and a divisible buying Right. Per-agent inputs are offered Good quantities \(q_s\), declared Good purchase quantities \(d_b\), initial Rights \(r_b^0\), Right sale capacities \(u_b\le r_b^0\), Right purchase capacities \(v_b\), initial money budgets \(M_b\), asks \(a_s^G,a_b^R\), and average-price bids \(p_b^G,p_b^R\); all are nonnegative binary rationals.
Choose aggregate real flows \(x_{bs}\ge0\) and \(y_{ab}\ge0\), where \(y_{ab}\) transfers Rights from buyer type \(a\) to buyer type \(b\), and \(y_{bb}=0\). Define \(G_b=\sum_sx_{bs}\), \(H_b=\sum_ay_{ab}\), and \(O_b=\sum_ay_{ba}\).
Require \(\sum_bx_{bs}\le\nu_sq_s\), \(G_b\le\mu_bd_b\), \(O_b\le\mu_bu_b\), \(H_b\le\mu_bv_b\), \(\mu_br_b^0-O_b+H_b\ge G_b\), and \(H_b\le G_b\).
Trades are paid at the asks. Require \(\sum_sa_s^Gx_{bs}\le p_b^GG_b\), \(\sum_aa_a^Ry_{ab}\le p_b^RH_b\), and \(\sum_sa_s^Gx_{bs}+\sum_aa_a^Ry_{ab}\le\mu_bM_b\). Right-sale proceeds cannot fund purchases in this clearing round; zero-volume price constraints hold without division.
Maximize \(G=\sum_bG_b\). Equivalently, given a nonnegative binary-rational threshold \(K\), decide whether a feasible clearing has \(G\ge K\).
Is this mass-based maximum-clearing decision problem in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For a finite list of traders with divisible quantities, maximum clearing under average-price bids is computable in polynomial time by linear programming ([Sychrovský et al.](https://arxiv.org/pdf/2302.09959)).
No prior result settling this precise support-mass formulation was identified in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Conclusion

The decision problem belongs to \(\mathrm{P}\). The aggregate flows themselves give a rational linear program with polynomially many variables and constraints and polynomial encoding length. This also yields an exact maximum clearing in polynomial time.

Here, the support lists are given explicitly, and \(L\) includes the encoding of \(K\) for the decision problem.

1. A linear program on supported types

Write \(n=|B|=\tau-m\). Introduce one nonnegative variable \(x_{bs}\) for each \((b,s)\in B\times S\), and one nonnegative variable \(y_{ab}\) for each ordered pair of distinct buyers \(a,b\in B\). Set \(y_{bb}=0\) by convention, without introducing diagonal variables.

There are therefore

\(N=nm+n(n-1)=n(\tau-1)\le\tau^2\)

variables. The quantities

\(G_b=\sum_{s\in S}x_{bs},\qquad H_b=\sum_{a\in B\setminus\{b\}}y_{ab},\qquad O_b=\sum_{a\in B\setminus\{b\}}y_{ba}\)

are linear expressions, rather than additional variables.

Impose the following inequalities:

\(\displaystyle \sum_{b\in B}x_{bs}\le\nu_sq_s.\)

\(G_b\le\mu_bd_b,\qquad O_b\le\mu_bu_b,\qquad H_b\le\mu_bv_b.\)

\(G_b+O_b-H_b\le\mu_br_b^0,\qquad H_b-G_b\le0.\)

\(\displaystyle \sum_{s\in S}(a_s^G-p_b^G)x_{bs}\le0,\)

\(\displaystyle \sum_{a\in B\setminus\{b\}}(a_a^R-p_b^R)y_{ab}\le0.\)

\(\displaystyle \sum_{s\in S}a_s^Gx_{bs}+\sum_{a\in B\setminus\{b\}}a_a^Ry_{ab}\le\mu_bM_b.\)

\(\displaystyle -\sum_{b\in B}\sum_{s\in S}x_{bs}\le-K.\)

These give \(m+8n+1\) inequalities, in addition to variable nonnegativity. Every coefficient is a fixed rational determined by the input. In particular, the mass products occur only as constant right-hand sides.

2. Exact equivalence to the clearing problem

Claim. This linear program is feasible if and only if the given society admits a feasible clearing with \(G\ge K\).

Proof. Suppose first that a feasible clearing is given. Use its off-diagonal flows as the linear-program variables. The supply, demand, transfer-capacity, and budget inequalities are unchanged. Rearranging the Rights-balance inequality gives exactly \(G_b+O_b-H_b\le\mu_br_b^0\).

For Good prices, substituting \(G_b=\sum_sx_{bs}\) gives the equivalence

\(\displaystyle \sum_sa_s^Gx_{bs}\le p_b^GG_b\quad\Longleftrightarrow\quad\sum_s(a_s^G-p_b^G)x_{bs}\le0.\)

The same rearrangement applies to Right prices. The clearing therefore satisfies all linear-program constraints, including the threshold.

Conversely, suppose the linear program is feasible. Restore the diagonal entries \(y_{bb}=0\), and define \(G_b,H_b,O_b\) by the stated sums. Reversing these rearrangements gives every clearing constraint in the question. The threshold constraint gives \(G\ge K\).

Neither direction divides by a traded volume. Consequently, the equivalence also holds when \(G_b=0\) or \(H_b=0\). The budget uses only initial money, exactly as stipulated. This proves the claim. \(\square\)

3. Encoding length and polynomial running time

We use the standard rational linear-programming theorem: feasibility of an explicitly encoded system of rational linear inequalities is decidable in time polynomial in its total binary encoding length. Rational linear optimization is also solvable exactly in polynomial time when a finite optimum exists.

Its hypotheses hold here:

Represent a rational input as a binary numerator and a positive binary denominator. Each numerator and denominator has at most \(L\) bits. A product of two input rationals can be represented by multiplying their numerators and denominators, producing \(O(L)\) bits. A difference can be represented by

\(\displaystyle \frac{A}{D}-\frac{C}{E}=\frac{AE-CD}{DE},\)

again with \(O(L)\) bits. Thus every coefficient and right-hand side constructed above has \(O(L+1)\) bits. These arithmetic operations take polynomial time.

Even a dense encoding of the main constraint matrix and right-hand side has size

\(\displaystyle O\!\left((m+8n+1)(N+1)(L+1)\right).\)

Explicitly encoding nonnegativity adds at most \(O(N(N+1))\) bits. Both quantities are polynomial in \(m,\tau,L\).

Constructing the linear program and applying rational linear-programming feasibility therefore decides the clearing question in time polynomial in \(m,\tau,L\). This is a bit-complexity bound: a small positive mass does not require expansion into individual traders.

4. Exact maximum clearing

Remove the threshold inequality and maximize the linear objective \(\sum_{b,s}x_{bs}\).

The resulting feasible set is nonempty: zero flows satisfy every constraint, because all capacities, initial Rights, and budgets are nonnegative.

It is also bounded. Nonnegativity and the supply constraints imply, for every Good-flow variable,

\(0\le x_{bs}\le\nu_sq_s.\)

Likewise, nonnegativity and the outgoing Right capacity imply, for every off-diagonal Right-flow variable,

\(0\le y_{ab}\le\mu_au_a.\)

The feasible set is closed, since it is defined by finitely many non-strict linear inequalities. Hence it is compact, and the linear objective attains a finite maximum. The rational linear-programming theorem therefore computes an exact optimal clearing in polynomial time, with the encoding bound proved above.

This direct construction is consistent with the finite-trader average-bid linear-programming result in [Sychrovský et al., Theorem 2 and Appendix C](https://arxiv.org/pdf/2302.09959). The proof here establishes the complexity of the precise support-mass formulation independently.

Thus the target question is resolved as polynomial-time solvable. Under polynomial-time many-one reductions, an additional claim of \(\mathrm{NP}\)-hardness would imply \(\mathrm{P}=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover resolves the assigned problem correctly. The linear program exactly represents the stated aggregate clearing constraints, its binary encoding has polynomial length, and the invoked rational linear-programming theorem applies. No major or minor mathematical issues were found.

With \(n=|B|=\tau-m\), the formulation introduces \(nm\) Good-flow variables and \(n(n-1)\) off-diagonal Right-flow variables. The count
\(N=nm+n(n-1)=n(\tau-1)\le\tau^2\)
is correct.

Omitting diagonal variables and restoring \(y_{bb}=0\) preserves the task exactly. The definitions of \(H_b\) and \(O_b\) correctly distinguish incoming and outgoing Rights. No expansion of masses into individual traders is required.

Every required constraint is present:

Thus \(m+8n+1\) is correct, excluding variable nonnegativity.

The Rights-balance rearrangement has the correct signs:
\(\mu_br_b^0-O_b+H_b\ge G_b\) is equivalent to
\(G_b+O_b-H_b\le\mu_br_b^0\).

The budget charges incoming Rights at the transferring buyer’s ask \(a_a^R\), as required. It includes no Right-sale proceeds.

Substituting the stated flow sums and moving terms to the left gives exactly the two displayed price inequalities. All asks and bids remain fixed coefficients; no product of decision variables is introduced.

The rearrangements involve no division, so they remain valid at zero volume. Nonnegativity also ensures that \(G_b=0\) forces every associated Good flow to vanish, and \(H_b=0\) forces every associated incoming Right flow to vanish.

A feasible clearing supplies precisely the off-diagonal variables required by the LP. All original constraints either appear unchanged or undergo reversible algebraic rearrangement.

Conversely, restoring zero diagonal flows and using the defined sums recovers every original clearing constraint. The threshold inequality is exactly equivalent to \(G\ge K\).

The argument establishes equivalence for the aggregate-flow problem actually assigned. It does not rely on an unstated realization by a finite population.

The prover explicitly includes \(K\) in the decision input length. This correctly accounts for the threshold’s representation.

Products of two input rationals have numerator and denominator lengths bounded by the sums of the corresponding input lengths. For differences, the displayed common-denominator formula likewise yields \(O(L+1)\)-bit coefficients, including negative coefficients and cancellation to zero. Reduction to lowest terms is unnecessary for the bound.

Each LP entry uses only a constant number of these operations. The stated dense matrix bound and the additional nonnegativity encoding are polynomial in \(m,\tau,L\). Construction therefore takes polynomial time. Small positive masses affect coefficient lengths rather than the number of variables.

The invoked theorem is stated sufficiently precisely for this application: explicitly encoded rational linear-inequality feasibility is decidable in polynomial bit complexity, and rational linear optimization with an attained finite optimum admits exact polynomial-time solution.

The decision formulation satisfies the feasibility theorem’s hypotheses: finitely many variables and inequalities, rational entries, and polynomial total encoding length. No numerical approximation or tolerance is substituted for the exact threshold decision.

After removing the threshold, zero flows satisfy all constraints because the relevant right-hand sides are nonnegative.

The coordinate bounds are correct. Supply bounds each \(x_{bs}\), and the outgoing capacity of buyer \(a\) bounds each \(y_{ab}\) by \(\mu_au_a\). Thus the feasible set is bounded. It is also closed, so the compactness and attainment argument is valid.

This reasoning covers zero quantities, zero budgets, zero capacities, and the single-buyer case, where there are no Right-transfer variables. For \(K=0\), zero flows are feasible; an unattainable positive threshold is handled by LP infeasibility.

The supplementary attribution is accurate: [Sychrovský et al., Theorem 2](https://arxiv.org/pdf/2302.09959) states that maximum clearing with average bids can be computed through linear programming. The prover’s support-mass argument is independent of that result.

The final complexity qualification is also correct: polynomial-time solvability would make NP-hardness under polynomial-time many-one reductions imply \(\mathrm{P}=\mathrm{NP}\).

No additional clarification or repair is needed.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.