← back to the atlas

d4-conf-ijcai-2011-0204 (d4-conf-ijcai-2011-0204)

Answer: Polynomial-time solvable in \(m,\tau,|E|,L\).

The anchor (named result in the paper)

Theorem 3.2 (Main) — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe final assignment Y = (yij) can be computed in time O(|A|4 + |A||B|) and has the following properties: 1. Stability: There are no blocking pairs in the original marketplace M = (A, B). 2. Pareto efficiency: No agent in M can be made better off without making some other agent in M strictly worse off. 3. (Weak) envy-freeness: No borrower envies the allocation of any other borrower in its category. 4.

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

The continuous mirror question, as graded

Given finite lenders \(A\) and borrower types \(T\) with rational masses \(\nu_t\) summing to \(1\), per-capita demands \(d_t\), lender budgets normalized per unit of population, and the paper’s weak preference orders, compute a feasible flow \(x_{it}\ge 0\) with \(\sum_t x_{it}\le B_i\) and \(\sum_i x_{it}\le \nu_t d_t\). Distribute each type’s flow uniformly across its mass. Is there an algorithm polynomial in \(|A|\), \(|T|\), the acceptability graph size, and the input bit length that returns a flow whose induced allocation is stable and Pareto efficient under type-level rank-prefix comparisons?

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

A society is given by its support: the list of the \(\tau\) borrower types with positive mass, each mass \(\nu_t\) a binary rational, with \(\sum_t\nu_t=1\). Here \(\tau=|T|\) is the support size, not the number of possible types. There are \(m=|A|\) lenders, nonnegative binary-rational budgets \(B_i\) per unit of population and per-capita demands \(d_t\), and an acceptability graph \(E\subseteq A\times T\). Let \(L\) be the total input bit length.
Each lender has a weak order over its acceptable types and is indifferent among borrowers of the same type. Each type has a common weak order over its acceptable lenders, preferring lower offered interest rates and tying equal rates. Every acceptable partner is strictly preferred to leaving capacity unused; ties are retained. Write \(r_i(t)\) and \(r_t(i)\) for ranks, with smaller ranks better.
A feasible flow has \(x_{it}\geq0\), vanishes outside \(E\), and satisfies \(\sum_t x_{it}\leq B_i\) and \(\sum_i x_{it}\leq\nu_t d_t\). Its uniform per-capita allocation to type \(t\) is \(q_{it}=x_{it}/\nu_t\); there are no additional pair capacities.
An acceptable pair \((i,t)\) blocks precisely when both conditions hold: lender \(i\) has unused budget or some \(x_{is}>0\) with \(r_i(t)<r_i(s)\); type \(t\) has unmet aggregate demand or some \(x_{jt}>0\) with \(r_t(i)<r_t(j)\). This applies even when \(x_{it}>0\). A flow is stable if no pair blocks.
Define lender prefixes \(F_{i,k}(x)=\sum_{t:r_i(t)\leq k}x_{it}\) and type prefixes \(G_{t,k}(x)=\sum_{i:r_t(i)\leq k}q_{it}\). A flow is Pareto efficient if no feasible flow weakly increases every prefix on both sides and strictly increases at least one.

Is computing a stable, Pareto-efficient flow for every such instance solvable in polynomial time in \(m,\tau,|E|,L\), or is this search problem \(\mathrm{NP}\)-hard?

For finite borrower populations, [Chen and Ghosh (2011)](https://www.ijcai.org/Proceedings/11/Papers/037.pdf) give a polynomial-time market-clearing algorithm with stability and Pareto efficiency; its aggregate assignment stage is strongly polynomial.
No result settling exactly the distribution-supported problem defined here was identified in the literature search.

Modeling choices made when packaging the task

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

Result

The search problem is polynomial-time solvable in \(m,\tau,|E|,L\).

The proof uses a polynomial-time algorithm for an integer-capacity stable assignment, followed by a linear program. The linear program establishes Pareto efficiency against all real-valued feasible flows, so the argument does not assume that efficiency among integer assignments implies efficiency among divisible flows.

1. Remove the per-capita normalization

Put \(C_t=\nu_t d_t\), the aggregate capacity of type \(t\), and define its aggregate prefixes by
\(H_{t,k}(x)=\sum_{i:r_t(i)\leq k}x_{it}\).

Since every supported type has \(\nu_t>0\), we have
\(H_{t,k}(x)=\nu_t G_{t,k}(x)\).
Consequently, weak or strict improvement of a type prefix is equivalent under \(H\) and \(G\).

Thus it suffices to work with the finite bipartite graph on \(A\) and \(T\), vertex capacities \(B_i\) and \(C_t\), and prefixes \(F_{i,k}\) and \(H_{t,k}\). This graph has one vertex per supported type; no individual borrowers are introduced.

Only prefixes at ranks occurring in a preference list need to be considered. Every other prefix is either identically zero or identical to one of these prefixes. There are at most \(2|E|\) relevant prefixes across both sides.

2. Proven lemma: prefix dominance preserves stability

Lemma. Suppose \(x\) is stable and \(y\) is feasible. If
\(F_{i,k}(y)\geq F_{i,k}(x)\) and
\(H_{t,k}(y)\geq H_{t,k}(x)\)
for every relevant prefix, then \(y\) is stable.

Proof. Fix an acceptable pair \((i,t)\), and write \(a=r_i(t)\), \(b=r_t(i)\).

The lender’s blocking condition is false precisely when its budget is fully used and it assigns nothing to types strictly worse than \(t\). By feasibility and nonnegativity, this is equivalent to
\(F_{i,a}(x)=B_i\).

Indeed, this equality forces the lender’s entire allocation to lie within that prefix. Conversely, full budget use with no worse assignment gives the equality.

Similarly, the type’s blocking condition is false precisely when
\(H_{t,b}(x)=C_t\).

Because \(x\) is stable, at least one of these equalities holds for the fixed pair.

If \(F_{i,a}(x)=B_i\), then dominance and feasibility give
\(B_i=F_{i,a}(x)\leq F_{i,a}(y)\leq B_i\).
Hence \(F_{i,a}(y)=B_i\), and the lender’s blocking condition remains false.

If instead \(H_{t,b}(x)=C_t\), the same argument gives
\(C_t=H_{t,b}(x)\leq H_{t,b}(y)\leq C_t\).
Thus the type’s blocking condition remains false.

In either case, \((i,t)\) does not block \(y\). Since the pair was arbitrary, \(y\) is stable. This argument also covers zero capacities and pairs with positive allocation. \(\square\)

3. Compute a stable rational seed

We use the following consequence of Chen and Ghosh’s abstract assignment theorem: a finite bipartite market with integer vertex capacities, incomplete weak preference lists, and unrestricted nonnegative integer quantities on acceptable edges admits a stable assignment computable in strongly polynomial time. Their stability definition is exactly the conjunction of the two willingness conditions in this question. See [Chen and Ghosh (2011), Section 4 and Theorem 4.7](https://www.ijcai.org/Proceedings/11/Papers/037.pdf).

Here are the reduction and hypothesis checks.

First compute the rational capacities \(B_i\) and \(C_t=\nu_t d_t\). Write them with positive integer denominators, and let \(D\) be the product of those denominators. Then
\(\widehat B_i=DB_i\) and \(\widehat C_t=DC_t\)
are nonnegative integers.

The scaled market has:

These are the hypotheses of the cited abstract theorem. Zero-capacity vertices may be removed before invoking it: every incident pair has that vertex’s blocking condition false, and feasibility forces every incident allocation to be zero. The remaining empty-market cases have the zero flow as their solution.

Apply the theorem to obtain an integer stable assignment \(\widehat x^0\), and set
\(x^0_{it}=\widehat x^0_{it}/D\).

This is feasible for the original capacities. Positive scaling preserves unused-capacity tests and positivity of every edge allocation; preference comparisons are unchanged. Therefore a pair blocks \(x^0\) exactly when it blocks \(\widehat x^0\). Hence \(x^0\) is stable under the question’s real-valued blocking definition.

We use only the stability of this seed.

4. Compute a Pareto-efficient dominating flow

Let \(K_i\) and \(K_t\) be the sets of ranks occurring in lender \(i\)’s and type \(t\)’s lists, respectively. Solve the following linear program over real variables \(y_{it}\), one for each \((i,t)\in E\).

Its objective is
\(\displaystyle \max \Phi(y)=\sum_{i\in A}\sum_{k\in K_i}F_{i,k}(y)+\sum_{t\in T}\sum_{k\in K_t}H_{t,k}(y)\).

Its constraints are:

The feasible region is nonempty because it contains \(x^0\). It is closed and bounded: each variable is nonnegative and at most its lender’s finite budget. Thus an optimum \(x^*\) exists.

Stability. The dominance constraints and the lemma imply that \(x^*\) is stable.

Pareto efficiency. Suppose a feasible real flow \(z\) weakly increases every original prefix of \(x^*\), and strictly increases at least one.

By the normalization equivalence, \(z\) weakly increases every aggregate prefix \(F,H\), with at least one strict increase. That strict increase also occurs at a relevant prefix, because omitted prefixes are zero or duplicates.

Since \(x^*\) dominates \(x^0\), transitivity implies that \(z\) satisfies every dominance constraint of the linear program. Thus \(z\) belongs to its feasible region.

Every summand in \(\Phi(z)\) is at least its counterpart in \(\Phi(x^*)\), and at least one is strictly larger. Therefore
\(\Phi(z)>\Phi(x^*)\),
contradicting optimality. Hence \(x^*\) is Pareto efficient against all feasible real flows.

Finally, its uniform per-capita allocation is \(q^*_{it}=x^*_{it}/\nu_t\). This division is defined because every supported mass is positive.

5. Polynomial bit complexity

Computing the products \(C_t=\nu_t d_t\) gives rational capacities whose total encoding length is \(O(L)\). The bit length of the denominator product \(D\) is at most the sum of the denominator bit lengths, hence \(O(L)\). The scaled integer capacities consequently have \(O(L)\) bits each. Scaling does not expand the graph or create one vertex per capacity unit.

The strongly polynomial integer-market algorithm therefore computes the seed in polynomial bit time. Its output quantities are bounded by the scaled capacities, so \(x^0\) has polynomial encoding length.

The linear program has \(|E|\) variables and \(O(m+\tau+|E|)\) constraints. Its constraint coefficients are \(0,1,-1\). Each objective coefficient counts the relevant prefixes containing an edge and is at most \(m+\tau\). All right-hand sides have polynomial encoding length.

The polynomial-time theorem for rational linear programming therefore supplies an exact rational optimum \(x^*\), with polynomial output length, in time polynomial in \(m,\tau,|E|,L\). Dividing by the input masses preserves polynomial encoding length.

This completes the polynomial-time algorithm and its correctness proof.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the task: the argument establishes a polynomial-time algorithm producing a stable flow that is Pareto efficient against all feasible real-valued flows. I found no major or minor issues.

Every supported mass satisfies \(\nu_t>0\). Therefore \(H_{t,k}(x)=\nu_t G_{t,k}(x)\) preserves both weak inequalities and strict inequalities when comparing flows. Lender prefixes require no normalization.

Replacing per-capita demand by aggregate capacity \(C_t=\nu_t d_t\) matches the task’s feasibility constraints exactly. The reduction retains one vertex per supported type and introduces no additional edge constraints.

Restricting attention to occurring ranks is also valid. A prefix at any other threshold is either empty or identical to a prefix at an occurring rank. Each edge contributes to one preference-list entry at each endpoint, so there are at most \(2|E|\) relevant prefixes.

For a feasible flow, the lender’s blocking condition at \((i,t)\) is false exactly when its total allocation equals \(B_i\) and no positive allocation goes to a strictly worse type. These conditions are equivalent to \(F_{i,r_i(t)}(x)=B_i\).

Tied partners belong to this prefix, as required by the task’s strict preference comparisons. The corresponding equivalence on the type side is \(H_{t,r_t(i)}(x)=C_t\).

Stability supplies at least one of these equalities for every acceptable pair. Prefix dominance preserves that equality because feasibility bounds the corresponding prefix above by the same capacity. Thus the proof correctly rules out every blocking pair in the dominating flow.

This reasoning includes zero capacities and already positively allocated pairs; neither requires an exception.

I checked the linked paper. Its model permits nonnegative integer edge quantities subject only to vertex capacities, with incomplete preference lists and ties. Its Section 4 blocking definition matches the task’s conjunction of willingness conditions, including leftover capacity and displacement of strictly worse partners. Theorem 4.7 states that ALG-PS computes a Pareto-stable assignment in strongly polynomial time. Although ALG-PS starts from a stable assignment, Section 4 explicitly supplies efficient initialization through a Gale–Shapley variant. Unequal side sizes are accommodated by isolated dummy vertices. The citation therefore supports the consequence used by the prover. [Chen and Ghosh, Sections 2 and 4, Theorem 4.7](https://www.ijcai.org/Proceedings/11/Papers/037.pdf)

The scaling construction satisfies the integer-capacity hypothesis: the positive denominator product \(D\) makes every \(DB_i\) and \(DC_t\) an integer while retaining the graph and preferences.

Removing zero-capacity vertices is legitimate. Feasibility forces their incident allocations to vanish, and their own blocking condition is always false.

Rescaling the integer assignment by \(1/D\) preserves feasibility, positive edge allocations, and whether capacity is unused. Consequently, the resulting rational seed is stable under the task’s exact blocking definition. The argument does not infer continuous Pareto efficiency from integer Pareto efficiency.

The seed satisfies every constraint, establishing nonemptiness. The feasible region is closed, and every variable satisfies \(0\leq y_{it}\leq B_i\), establishing boundedness. The linear objective therefore attains its maximum.

When there are no acceptable edges, the feasible region consists of the unique empty flow. Stability and Pareto efficiency are vacuous, so this case is covered.

Stability follows directly from the proved lemma and the linear program’s dominance constraints.

The efficiency argument considers an arbitrary feasible real flow \(z\), as required. If it dominates \(x^*\), normalization transfers this dominance to aggregate prefixes, and at least one relevant prefix improves strictly.

Transitivity places \(z\) in the linear program’s feasible region. Every objective summand then weakly increases, and at least one strictly increases. This contradicts optimality. The proof therefore establishes efficiency against all feasible flows, rather than merely against stable flows or rational flows.

Division by \(\nu_t\) is well defined and restores the requested uniform per-capita allocation.

Multiplying the input rationals to obtain \(C_t\) increases encoding length only linearly in their combined input lengths. The denominator product has \(O(L)\) bits, and each scaled capacity has \(O(L)\) bits. No capacity-dependent graph expansion occurs.

The cited strongly polynomial algorithm operates on this compact integer market, and its output quantities are bounded by the capacities. Thus the rational seed has polynomial encoding length.

The linear program has \(|E|\) variables and \(O(m+\tau+|E|)\) constraints. Its constraint coefficients and right-hand sides have the claimed polynomial encoding bounds. An edge occurs in at most \(\tau\) lender prefixes and at most \(m\) type prefixes, validating the objective-coefficient bound \(m+\tau\).

The standard polynomial-time rational linear-programming theorem applies to this nonempty, bounded rational program and supplies an exact rational optimum of polynomial encoding length. Final division by the positive input masses preserves polynomial encoding length.

No additional lemma, hypothesis, or clarification is needed to verify the conclusion.

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