← back to the atlas

d4-conf-aaai-2021-1199 (d4-conf-aaai-2021-1199)

Answer: polynomial-time solvable

The anchor (named result in the paper)

Lemma 5.1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet ¯S be a projection of S. The optimal value of problems (6) (Lp-norm) and (7) (Maxmin) is equal to their optimal value when restricted to ¯S. In this way, we can adapt both our ILP and CP method- ologies to restrict the enumeration to projections. Note that a projection is a covering, but the reverse does not hold.

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

The continuous mirror question, as graded

Given rational masses for supported patient-donor types and altruist-donor types, together with compatibility data and an exchange-length limit of three, choose feasible exchange masses to maximize total transplanted mass; among those maximizing allocations, maximize the minimum patient-type transplant rate.

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

Let \(P\neq\varnothing\) be the supported incompatible patient-donor types and \(N\) the supported altruist-donor types; write \(m=|P|\). A society is given by its support: the list of \(\tau=|P|+|N|\) types with positive mass \(a_i\), each a binary rational, with \(\sum_i a_i=1\). Thus \(\tau\) is the support size, not the number of possible types; let \(L\) be the total input bit length.
Compatibility is an explicitly given Boolean relation from donor types to patient types, uniform within each type, with no compatibility from a patient-donor type to itself.
An exchange is either a directed cycle containing two or three patient-donor occurrences, or a directed chain containing one altruist followed by one or two patient-donor occurrences. Every successive donation must be compatible, including the closing donation of a cycle. The terminal chain donor leaves the current allocation.
For each exchange \(c\), choose a real mass \(x_c\geq0\). If \(n_i(c)\) counts its occurrences of type \(i\), feasibility means \(\sum_c n_i(c)x_c\leq a_i\) for every supported type; mass may be divided among exchanges.
For \(i\in P\), define transplanted mass \(y_i=\sum_c n_i(c)x_c\) and transplant rate \(r_i=y_i/a_i\). Lexicographically maximize \(\bigl(\sum_{i\in P}y_i,\min_{i\in P}r_i\bigr)\), including patient types with zero attainable rate.

Is this exact lexicographic optimization problem solvable in polynomial time in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

For finite societies, retaining one optimal exchange plan for each distinct set of transplanted patients preserves the optimal maxmin and mean-deviation fairness values; maxmin is computable by an LP once these plans are listed. [Farnadi et al.](https://ojs.aaai.org/index.php/AAAI/article/view/17369)
Recent work also studies fairness through lotteries over finite exchange packings. No result settling the mass-allocation problem defined here was located. [Chang et al.](https://arxiv.org/html/2605.20070v1)

Modeling choices made when packaging the task

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

Exact polynomial-time solvability

The problem is solvable exactly in polynomial time in \(m,\tau,L\). Both stages of the lexicographic objective are linear programs with polynomially many variables and constraints. The proof also establishes that an optimal allocation has a rational representation of polynomial length.

1. Enumerating all permitted exchanges

Write \(h=|N|=\tau-m\), and let \(K(u,v)\) indicate compatibility from the donor of type \(u\) to the patient of type \(v\).

Enumerate the following ordered type tuples, retaining precisely those that pass the indicated compatibility tests:

| Exchange | Candidate tuples | Compatibility tests |
|---|---|---|
| Two-patient cycle | \((i,j)\in P^2\) | \(K(i,j)\) and \(K(j,i)\) |
| Three-patient cycle | \((i,j,k)\in P^3\) | \(K(i,j)\), \(K(j,k)\), and \(K(k,i)\) |
| One-patient chain | \((n,i)\in N\times P\) | \(K(n,i)\) |
| Two-patient chain | \((n,i,j)\in N\times P^2\) | \(K(n,i)\) and \(K(i,j)\) |

There is no closing compatibility test for chains: their terminal donors leave the allocation, as stipulated.

These tuples describe every permitted exchange because compatibility depends only on types. The absence of self-compatibility automatically excludes repeated patient types in these short exchanges: any repetition would require a donation from a patient-donor type to itself.

Cycle rotations may be identified by keeping a canonical representative. This does not change feasibility or either objective, since rotations have identical occurrence counts and their assigned masses can be summed.

Let \(C\) be the resulting exchange list and \(d=|C|\). Then

\[ \]
\(d\le m^2+m^3+hm+hm^2=O(\tau m^2).\)

Each candidate requires at most three compatibility tests, so this list can be constructed in polynomial time. If \(d=0\), the empty allocation is optimal and both objective values are zero. Henceforth assume \(d>0\).

2. A linear program for maximum transplanted mass

Define the occurrence matrix and objective coefficients by

\(A_{ic}=n_i(c)\quad(i\in P\cup N,\ c\in C),\qquad q_c=\sum_{i\in P}n_i(c).\)

Thus \(q_c\in\{1,2,3\}\), and the total transplanted patient mass is

\(T(x)=q^{\mathsf T}x=\sum_{i\in P}y_i.\)

By the problem’s definition, the feasible allocations are exactly

\(F=\{x\in\mathbb R^d:Ax\le a,\ x\ge0\}.\)

In particular, every altruist capacity constraint is included. The first-stage optimum is therefore the linear-programming value

\(\displaystyle T^\star=\max\{q^{\mathsf T}x:Ax\le a,\ x\ge0\}.\)

This maximum exists. Indeed, \(F\) contains the zero allocation and is closed. For every exchange \(c\), choose any type \(i\) occurring in it. Nonnegativity and the corresponding capacity constraint give

\(n_i(c)x_c\le\sum_{c'\in C}n_i(c')x_{c'}\le a_i,\)

so \(0\le x_c\le a_i/n_i(c)\le1\). Consequently, \(F\) is compact.

3. A linear program for maxmin fairness on the optimal face

Every supported patient type has \(a_i>0\). Therefore, for any real \(t\),

\(\displaystyle t\le r_i(x)\quad\Longleftrightarrow\quad \sum_{c\in C}n_i(c)x_c\ge a_i t.\)

After computing \(T^\star\) exactly, solve the second linear program:

\(\displaystyle \max t\)

subject to

\(Ax\le a,\qquad x\ge0,\qquad q^{\mathsf T}x=T^\star,\)

\(\displaystyle \sum_{c\in C}n_i(c)x_c\ge a_i t\quad\text{for every }i\in P,\)

\(0\le t\le1.\)

The bounds on \(t\) lose no relevant solution because every feasible transplant rate lies in \([0,1]\). This LP is feasible: any first-stage optimal allocation together with \(t=0\) satisfies its constraints. Its feasible set is closed and contained in the compact set \(F\times[0,1]\), so an optimum exists.

For any fixed first-stage optimal allocation \(x\), its largest feasible value of \(t\) is exactly

\(\displaystyle \min_{i\in P}r_i(x).\)

Thus, if \((x^\star,t^\star)\) solves the second LP, then

\(\displaystyle t^\star=\max_{\substack{x\in F\\T(x)=T^\star}}\min_{i\in P}r_i(x).\)

This proves lexicographic optimality: no feasible allocation has a larger first coordinate, and among allocations with first coordinate \(T^\star\), none has a larger second coordinate.

Every patient type remains in the fairness constraints. In particular, if a type has zero attainable transplanted mass, its constraint forces \(t=0\); such types are not discarded.

4. Exactness and polynomial bit complexity

We use the classical rational linear-programming theorem: a linear program with explicitly given rational coefficients can be solved exactly in time polynomial in its binary encoding length, returning a rational optimum when the optimum is finite and attained. Polynomial-time solvability in the rational bit model is recalled in [Adler and Beling](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf).

The first LP has \(d\) variables and \(\tau\) capacity constraints, besides nonnegativity. Its matrix and objective entries are bounded integers, and its right-hand side consists of the input masses. Its encoding length is therefore polynomial in \(m,\tau,L\).

For completeness, the exact value \(T^\star\) also has polynomial bit length, so inserting it into the second LP preserves polynomial size. Here is a direct bound.

A linear objective on the nonempty compact polytope \(F\) has an optimal vertex. At such a vertex, choose \(d\) linearly independent active constraints. They give

\(Bx=b,\)

where \(B\) is an invertible integer matrix with entries of absolute value at most \(3\), and each entry of \(b\) is either an input mass or zero.

Let \(D\) be the product of the denominators of all input masses. Its bit length is \(O(L)\), and \(Db\) is an integer vector whose entries have absolute value at most \(D\). Cramer’s rule gives

\(\displaystyle x_j=\frac{\det B_j}{D\det B},\)

where \(B_j\) replaces column \(j\) of \(B\) by \(Db\). Hadamard’s determinant inequality gives

\(\displaystyle |\det B|\le(3\sqrt d)^d,\qquad |\det B_j|\le D\sqrt d\,(3\sqrt d)^{d-1}.\)

Hence these coordinates have a common denominator and numerators of bit length \(O(L+d\log(d+1))\). Since \(q_j\le3\), the same polynomial bound, with an additional \(O(\log(d+1))\) term, holds for \(T^\star=q^{\mathsf T}x\).

The second LP has \(d+1\) variables, \(\tau\) capacity constraints, \(m\) fairness constraints, one equality, and the bounds on \(t\). Its only additional rational coefficients are the input masses and \(T^\star\). It consequently has polynomial encoding length and can also be solved exactly in polynomial time.

5. Why finite-packing enumeration is unnecessary

The cited work concerns lotteries over finite exchange packings: [Farnadi et al.](https://ojs.aaai.org/index.php/AAAI/article/view/17369) enumerate optimal plans, while [Chang et al.](https://arxiv.org/html/2605.20070v1) optimize over marginals of acceptable packings.

The present problem specifies feasibility directly through divisible exchange masses and type capacities. Its LP variables therefore represent individual permitted exchanges, whose number is polynomial because their lengths are bounded by constants. No enumeration of complete exchange plans is needed.

The two LPs above settle the stated mass-allocation problem, returning both objective values and an optimal allocation exactly.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The prover resolves the stated mass-allocation problem by two explicitly constructed rational linear programs of polynomial encoding length. The exchange enumeration, lexicographic reduction, existence arguments, and bit complexity bounds are correct. No mathematical repair is required.

1. Enumeration of exchanges

The four tuple families match the permitted exchanges exactly.

The absence of a closing constraint for chains correctly implements the stipulated departure of the terminal donor.

The claim that repeated patient types are excluded is correct for these particular lengths. A repeated type in a two-patient exchange requires self-compatibility. In a three-patient cycle, any repetition produces equal types at the endpoints of one of its three donation edges, including possibly the closing edge. Thus no permissible exchange is inadvertently excluded.

Uniform compatibility within each type justifies enumerating type tuples rather than individual occurrences. This uses the task’s explicitly defined divisible-mass feasibility model.

Identifying cycle rotations is valid: rotations have identical capacity consumption and objective contributions, and summing their masses preserves both feasibility and objectives.

The count
\(d\leq m^2+m^3+hm+hm^2\)
is correct. Since \(m\geq1\) and \(\tau=m+h\), this is \(O(\tau m^2)\). Each candidate has at most three compatibility tests, so explicit construction is polynomial.

The case \(d=0\) is handled correctly. Every transplanted mass and rate is zero, and the empty allocation attains both objective values.

Finding: correct and complete.

2. First-stage LP

The occurrence matrix includes every supported type, including altruists. Therefore
\(F=\{x\in\mathbb{R}^d:Ax\leq a,\ x\geq0\}\)
is exactly the feasible set specified in the task.

The objective coefficients correctly count patient occurrences rather than all occurrences. Hence
\(q^{\mathsf T}x=\sum_{i\in P}y_i\)
is precisely the first lexicographic coordinate. The inclusion of altruist capacity constraints prevents reuse of altruist mass beyond its supply.

The existence argument is valid:

\(0\leq x_c\leq a_i/n_i(c)\leq1\).

Thus the feasible set is bounded and closed in finite-dimensional space, hence compact. Its linear objective attains a maximum.

Finding: correct and complete.

3. Second-stage LP and lexicographic optimality

All supported patient masses are strictly positive, so multiplying the rate inequality by \(a_i\) preserves its direction. The displayed equivalence between \(t\leq r_i(x)\) and \(y_i(x)\geq a_i t\) is valid.

The equality \(q^{\mathsf T}x=T^\star\) restricts the second stage to first-stage maximizers. This correctly implements the required priority of total transplanted mass over fairness.

The bounds \(0\leq t\leq1\) are harmless because the capacity constraints imply \(0\leq r_i(x)\leq1\) for every patient type. A first-stage optimizer together with \(t=0\) establishes second-stage feasibility. Closedness and containment in \(F\times[0,1]\) establish attainment.

For each fixed first-stage optimizer, the maximum permitted \(t\) is exactly the minimum patient rate. Consequently, maximizing \(t\) over this optimal face maximizes the second lexicographic coordinate.

The argument also correctly retains zero-attainable patient types. Their fairness constraints force \(t=0\), as the task requires. There is no implicit restriction to transplantable types.

The proof establishes existence of a lexicographic optimizer; uniqueness is neither claimed nor needed.

Finding: correct and complete.

4. Polynomial encoding length and exact solution

The rational LP theorem is stated with the relevant computational model: explicitly encoded rational coefficients and running time polynomial in binary encoding length. The cited [Adler–Beling paper](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf) recalls polynomial-time solvability of rational LPs in this model.

Its hypotheses are satisfied for the first LP:

The separate bound on the encoding length of \(T^\star\) is also correct.

A linear objective on a nonempty compact polytope has an optimal vertex. At a vertex in \(\mathbb{R}^d\), the active constraint normals contain \(d\) linearly independent rows, giving an invertible system \(Bx=b\). Its integer coefficients have absolute value at most \(3\), including the nonnegativity constraint rows.

The denominator product \(D\) has bit length \(O(L)\). Every entry of \(Db\) is an integer of absolute value at most \(D\), because each input mass is at most one.

The stated Cramer’s rule formula is correct: replacing a column by \(Db\) multiplies the corresponding determinant with replacement column \(b\) by \(D\). The column form of Hadamard’s inequality gives exactly the two displayed determinant bounds.

These bounds yield polynomial bit lengths for the common denominator and all numerators. Summing \(d\) coordinates weighted by integers at most \(3\) adds only \(O(\log(d+1))\) bits to the numerator bound. Therefore \(T^\star\) has polynomial encoding length.

For the second LP:

The same exact rational LP theorem therefore applies. It also supports the opening claim that an optimal allocation can be returned with polynomial-length rational representation.

Finding: correct and complete. The result concerns polynomial time in the binary input model; no stronger running-time claim is made.

5. Relationship to finite-packing fairness

The contextual comparison is accurate. [Farnadi et al.](https://ojs.aaai.org/index.php/AAAI/article/view/17369) describe randomized selection among optimal finite plans and enumeration of optimal solutions. [Chang et al.](https://arxiv.org/html/2605.20070v1) formulate fairness over achievable marginals of lotteries on acceptable packings.

The prover correctly distinguishes those feasibility models from the task’s direct type-capacity inequalities for divisible exchange masses. No equivalence with a convex hull of finite packings is assumed or needed. The relevant enumeration here is of individual bounded-length exchanges, whose number is polynomial.

Finding: correct. The contextual citations are not needed to establish the two-LP result.

Issues and actionable feedback

No unjustified mathematical step, false statement, missing hypothesis, incorrect computation, or unresolved edge case was found. No additional clarification is needed to verify the claimed result.

⟨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.