← back to the atlas

d4-conf-ijcai-2017-0719 (d4-conf-ijcai-2017-0719)

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

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateThe decision problem associated with the uncapped generalized clearing problem is NP-complete.

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

The continuous mirror question, as graded

Given finitely many club types \(T\) with rational masses \(\mu_t\ge0\), \(\sum_t\mu_t=1\), finite donor and patient slots per type, parameters \(\alpha_t\ge1,\gamma_t\ge0\), and rational compatibility and weights for allowed donor-slot/patient-slot type pairs, does there exist a measurable allocation of trades in an atomless population of clubs with total weight at least \(B\), where each slot is used at most once and almost every type-\(t\) club has integral external-trade counts \(d_c,p_c\) satisfying \(d_c\le\alpha_t p_c+\gamma_t\)?

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

A society is given by its support: the list of \(\tau\) club types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types.
Each type has explicitly listed, possibly empty donor and patient slot sets \(D_t,P_t\), and binary-rational parameters \(\alpha_t\ge1,\gamma_t\ge0\). Input compatibility is an explicit set \(E\) of allowed donor-slot/patient-slot type pairs, with weights \(w_e\in\mathbb Q\); the threshold is \(B\in\mathbb Q\).
Realize type \(t\) clubs as a tagged interval \(X_t=[0,\mu_t)\) with Lebesgue measure. Each club owns its own copies of its slots. Donor and patient slot spaces carry club measure times counting measure.
An allocation is a measurable, measure-preserving bijection between measurable subsets of the donor and patient slot spaces, with measurable inverse, using only pairs in \(E\). Each slot is used at most once; compatible donations within a club are allowed and contribute weight.
For almost every club \(c\) of type \(t\), the integral counts \(d_c,p_c\) of donations to, and receipts from, other clubs satisfy \(d_c\le\alpha_t p_c+\gamma_t\). Different clubs of the same type count as other clubs. All trades occur simultaneously, without length or scheduling caps.
Total weight is the integral of matched-edge weights over used donor slots. Let \(m=\sum_t(|D_t|+|P_t|)\) and let \(L\) be the total binary input length.

Is deciding whether such an allocation has total weight at least \(B\) solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

Finite uncapped club clearing is claimed NP-complete, but the published hardness construction uses \(\alpha=1/|S|\), so it does not establish hardness under the stated restriction \(\alpha\ge1\). [Discrete result and construction](https://www.ijcai.org/proceedings/2017/0029.pdf)
No result settling this exact atomless problem was located in the literature search.

Modeling choices made when packaging the task

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

Result

The decision problem is solvable in polynomial time in \(m,\tau,L\).

The proof gives an exact polynomial-size rational linear program. Its essential ingredients are:

In fact, the proof works for all nonnegative rational multipliers \(\alpha_t\), including those below \(1\).

1. Local configurations

Write \(n_t=|D_t|\) and \(q_t=|P_t|\). A compatibility edge has the form \(e=((t,i),(s,j))\), where \(i\in D_t\) and \(j\in P_s\).

Define the allowed internal edges of type \(t\) by

\[ \]
\(I_t=\{(i,j)\in D_t\times P_t:((t,i),(t,j))\in E\}.\)

Here “internal” means a donation within the very same club. A donation between distinct clubs of type \(t\) is external.

A local configuration specifies:

Let \(d\) and \(p\) be the sizes of the latter two subsets. The permitted count pairs are

\(R_t=\{(d,p)\in\mathbb Z_{\ge0}^2:d\le n_t,\ p\le q_t,\ d\le\alpha_t p+\gamma_t\}.\)

There are at most \((n_t+1)(q_t+1)\) such pairs, and they can be enumerated using exact rational arithmetic. In particular, this enumeration is polynomial even when the numerators or denominators of \(\alpha_t,\gamma_t\) are large.

Lemma 1: fixed-count local configurations have an integral description

For fixed \((d,p)\in R_t\), introduce nonnegative variables:

Let \(Q_t^{d,p}\) be the polytope defined by

\(a_i+\sum_{j:(i,j)\in I_t}h_{ij}\le1\quad(i\in D_t),\)

\(b_j+\sum_{i:(i,j)\in I_t}h_{ij}\le1\quad(j\in P_t),\)

\(\sum_{i\in D_t}a_i=d,\qquad \sum_{j\in P_t}b_j=p.\)

Then \(Q_t^{d,p}\) is exactly the convex hull of the local configurations having external counts \((d,p)\).

Proof. Construct a bipartite graph with left vertices \(D_t\cup\{\ell\}\) and right vertices \(P_t\cup\{r\}\). Its edges are:

Each real slot vertex has degree at most \(1\), while \(r\) has degree exactly \(d\) and \(\ell\) has degree exactly \(p\). These are precisely the constraints above.

The vertex-edge incidence matrix of a bipartite graph is totally unimodular: multiplying the rows on one side by \(-1\) produces a directed incidence matrix. To verify total unimodularity, consider any square submatrix. If some column has at most one nonzero entry, expand its determinant along that column and use induction. Otherwise every column has one \(+1\) and one \(-1\), so the rows sum to zero and the determinant vanishes. Adding slack-variable columns preserves total unimodularity.

All right-hand sides are integral. Consequently, every vertex of \(Q_t^{d,p}\) is integral. Each variable is bounded above by \(1\), since its edge touches a real slot vertex. Thus every vertex specifies an internal matching and disjoint external slot subsets of the required sizes.

Conversely, every such local configuration satisfies the constraints. The polytope is bounded, so it equals the convex hull of its vertices. This proves the lemma. \(\square\)

2. A polynomial-size LP

For each type \(t\) and each \((d,p)\in R_t\), introduce a variable \(\lambda_{t,d,p}\ge0\). It represents the measure of clubs assigned those external counts. Require

\(\sum_{(d,p)\in R_t}\lambda_{t,d,p}=\mu_t.\)

For each such count pair, introduce nonnegative variables \(a_{t,d,p,i}\), \(b_{t,d,p,j}\), and \(h_{t,d,p,ij}\), satisfying the scaled local constraints

\(a_{t,d,p,i}+\sum_{j:(i,j)\in I_t}h_{t,d,p,ij}\le\lambda_{t,d,p},\)

\(b_{t,d,p,j}+\sum_{i:(i,j)\in I_t}h_{t,d,p,ij}\le\lambda_{t,d,p},\)

\(\sum_{i\in D_t}a_{t,d,p,i}=d\lambda_{t,d,p},\qquad \sum_{j\in P_t}b_{t,d,p,j}=p\lambda_{t,d,p}.\)

When \(\lambda_{t,d,p}>0\), dividing these variables by \(\lambda_{t,d,p}\) gives a point of \(Q_t^{d,p}\). When \(\lambda_{t,d,p}=0\), the slot inequalities and nonnegativity force all its local variables to vanish.

For each \(e\in E\), introduce \(y_e\ge0\), representing the measure of external matches using that edge. This includes external matches between distinct clubs of the same type. Impose the donor and patient balance equations

\(\sum_{\substack{e\in E\\e=((t,i),(s,j))}}y_e =\sum_{(d,p)\in R_t}a_{t,d,p,i} \quad(t,\ i\in D_t),\)

\(\sum_{\substack{e\in E\\e=((s,i),(t,j))}}y_e =\sum_{(d,p)\in R_t}b_{t,d,p,j} \quad(t,\ j\in P_t).\)

In each left-hand sum, all unspecified endpoints range over the relevant types and slots.

The LP objective is

\(W=\sum_{e\in E}w_e y_e+ \sum_t\sum_{(d,p)\in R_t}\sum_{(i,j)\in I_t} w_{((t,i),(t,j))}h_{t,d,p,ij}.\)

For the decision problem, add the constraint \(W\ge B\).

We next prove that this LP is exact in both directions.

3. Every allocation gives a feasible LP point

Let a feasible allocation be given.

For each club, record its internal matching, externally used donor slots, and externally used patient slots. These form a local configuration. Almost every type-\(t\) club has its external count pair in \(R_t\), by the stated participation constraint.

These records are measurable. Indeed, the allocation and its inverse are measurable, and an internal match is characterized by equality of the donor’s and patient’s tagged club coordinates. There are only finitely many slot and configuration possibilities.

Define \(\lambda_{t,d,p}\) as the measure of clubs with external counts \((d,p)\). Define the corresponding \(a,b,h\) variables by integrating their configuration indicators over those clubs. The local inequalities hold pointwise, so their integrals satisfy the scaled local constraints. Any exceptional set of clubs has measure zero and does not affect these equations.

Define \(y_e\) as the measure of donor slots externally matched using compatibility edge \(e\). Measure preservation implies that the corresponding matched patient set has the same measure. Therefore both families of balance equations hold.

Finally, splitting the used donor slots into internal and external matches shows that the allocation’s weight is exactly \(W\).

Thus every allocation of weight at least \(B\) yields a feasible LP point with \(W\ge B\).

4. Matching same-type clubs without self-matches

The converse requires ensuring that an external edge between two slots of the same type never becomes an internal donation.

Lemma 2: equal-measure interval sets admit a fixed-point-free matching

Let \(A,B\) be finite unions of half-open intervals in a common real interval, both of measure \(z>0\). There is a measurable, measure-preserving bijection \(f:A\to B\), with measurable inverse, satisfying \(f(x)\ne x\) for every \(x\in A\).

Proof. Listing each set’s intervals in order gives measure-preserving bijections

\(a:[0,z)\to A,\qquad b:[0,z)\to B.\)

Each is a translation on each of finitely many pieces. Write their translation constants as \(\eta_i\) and \(\zeta_j\), respectively.

For \(\theta\in[0,z)\), define the circular shift

\(\rho_\theta(u)=(u+\theta)\bmod z\)

and set \(f=b\circ\rho_\theta\circ a^{-1}\). This is a measure-preserving bijection with measurable inverse.

If \(f(a(u))=a(u)\), then on the relevant pieces, for some \(k\in\{0,1\}\),

\(u+\theta-kz+\zeta_j=u+\eta_i.\)

Hence necessarily

\(\theta=\eta_i-\zeta_j+kz.\)

There are only finitely many such forbidden values. Choose \(\theta\in[0,z)\) outside that finite set. Then \(f\) has no fixed points. \(\square\)

For sets belonging to different tagged types, the same interval parametrizations provide a measure-preserving bijection without needing this additional condition: different tags already identify different clubs.

5. Every feasible LP point gives an allocation

Take any feasible LP point.

Step 1: realize the local mixtures

For every positive \(\lambda_{t,d,p}\), the normalized local variables belong to \(Q_t^{d,p}\). By Lemma 1, they are a finite convex combination of local configurations.

Partition \(X_t=[0,\mu_t)\) into finitely many half-open intervals whose lengths are the masses assigned to these configurations. Assign the indicated configuration to every club in each interval.

Perform each designated internal match by mapping a donor slot at coordinate \(x\) to the designated patient slot of the same club, also at coordinate \(x\).

This realizes all the prescribed internal-match masses. It also produces:

Their measures are

\(|A_{t,i}|=\sum_{(d,p)\in R_t}a_{t,d,p,i},\qquad |C_{t,j}|=\sum_{(d,p)\in R_t}b_{t,d,p,j}.\)

Here \(|\cdot|\) denotes Lebesgue measure.

Step 2: partition external slots by compatibility edge

For each donor slot \((t,i)\), partition \(A_{t,i}\) among its outgoing edges \(e\in E\), giving edge \(e\) a source set \(A_e\) of measure \(y_e\).

This is possible by the donor balance equation. Cutting finitely many intervals at the required cumulative measures gives finite unions of half-open intervals.

Independently, partition each \(C_{s,j}\) among its incoming edges, producing target sets \(C_e\) with measure \(y_e\). The patient balance equation guarantees this is possible.

Thus, for every edge \(e\),

\(|A_e|=|C_e|=y_e.\)

Step 3: perform the external matches

For every edge with \(y_e>0\), match its source and target sets by a measure-preserving bijection.

If the endpoint types differ, use their interval parametrizations. If the endpoint types agree, apply Lemma 2 to their club-coordinate sets. This guarantees that the donor and patient belong to different clubs.

The source sets are disjoint within each donor slot, and the target sets are disjoint within each patient slot. Local configurations also keep externally used slots disjoint from internally used slots. Consequently, the union of all these maps and the internal maps is a bijection between the used donor and patient subsets.

This union is measurable, measure preserving, and has measurable inverse, because it consists of finitely many such maps.

Step 4: verify the constraints and weight

Every club assigned a configuration indexed by \((d,p)\) makes exactly \(d\) external donations and receives exactly \(p\) external donations. The same-type external maps have no self-matches, so these counts are indeed external counts. Since \((d,p)\in R_t\),

\(d\le\alpha_t p+\gamma_t.\)

Every used slot is used once, every match is compatible, and the resulting weight is exactly the LP objective \(W\).

This proves the converse and therefore establishes exact equivalence between LP feasibility with \(W\ge B\) and existence of the requested allocation.

6. Polynomial running time

Let \(r_t=n_t+q_t\), so \(\sum_t r_t=m\).

For type \(t\), there are at most \((r_t+1)^2\) count pairs. Each pair contributes at most \((r_t+1)^2\) local variables, including its \(\lambda\) variable. Hence the total number of local variables is at most

\(\sum_t(r_t+1)^4\le(m+\tau)^4.\)

There are additionally \(|E|\le m^2\) external-edge variables. The number of constraints is polynomial as well.

The sets \(R_t\) are computed by polynomially many exact comparisons involving the input rationals. After this enumeration, all LP coefficients come from:

Thus the LP’s total rational encoding length is polynomial in \(m,\tau,L\). The standard polynomial-time theorem for rational linear-programming feasibility applies: it decides feasibility in time polynomial in the dimensions and total coefficient encoding length.

Importantly, the construction enumerates only the supplied support types and their bounded count pairs. It never enumerates the space of possible types.

7. Relation to the discrete construction

The cited discrete reduction uses \(\alpha=1/|S|\) to require all patients of a set-club to receive before its donor can donate, as stated in its proof of Theorem 1. [Farina, Dickerson, and Sandholm, IJCAI 2017](https://www.ijcai.org/proceedings/2017/0029.pdf)

The argument above establishes polynomial-time solvability of the present atomless problem independently of that discrete claim. Atomlessness permits exact mixtures of local configurations and unrestricted matching of their external slot masses. No step of the proof uses \(\alpha_t\ge1\); nonnegative rational multipliers suffice.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the assigned atomless decision problem. The LP equivalence is correct, its size and encoding length are polynomial, and the realization argument satisfies the required measurable-bijection conditions. I found no substantive gaps or false steps.

1. Local configurations and count enumeration

The definition of a local configuration correctly separates internal matches from external slot uses. An internal matching uses each donor and patient slot at most once, and the external subsets use only remaining slots.

The permitted set \(R_t\) imposes the participation constraint on integer counts for individual clubs. This avoids replacing the pointwise constraint with an insufficient constraint on average counts.

The enumeration bound \((n_t+1)(q_t+1)\) is correct. Testing \(d\le\alpha_t p+\gamma_t\) for these bounded integers requires rational arithmetic with polynomial bit complexity. Large binary-encoded parameter values do not enlarge the enumeration range.

Finding: Correct.

2. Lemma 1: integrality of the fixed-count polytope

The auxiliary bipartite graph represents every stated constraint:

The total-unimodularity argument is valid. After signing one side’s rows, every edge column has one positive and one negative entry. In a square submatrix, determinant expansion applies when a column has at most one nonzero entry; otherwise every column has two opposite entries, making the rows linearly dependent. Slack columns preserve this property.

The right-hand sides are integral, including the prescribed auxiliary degrees. Thus the usual total-unimodularity integrality conclusion applies to the mixed equality and inequality system. Every edge variable is bounded by a real slot’s capacity, so integral vertices have only zero-or-one coordinates.

These vertices are precisely valid fixed-count local configurations. Boundedness justifies the convex-hull conclusion.

Empty donor or patient sets cause no failure: the corresponding sums and permitted counts are interpreted correctly.

Finding: Correct; no additional matching lemma is needed.

3. LP formulation

The scaled constraints correctly encode mixtures of fixed-count configurations. For positive \(\lambda_{t,d,p}\), normalization gives a point in \(Q_t^{d,p}\). For zero \(\lambda_{t,d,p}\), nonnegativity and the slot inequalities force all associated slot and internal-edge variables to vanish.

The balance equations equate each externally designated slot mass with its incident external-edge masses. Same-type edges are correctly included among external edges, while internal use has separate variables.

The objective counts every matched donor slot once, with the weight of its compatibility edge. Internal and external use of the same compatibility type are distinguished without double counting.

Finding: Correct.

4. Allocation-to-LP direction

A given allocation determines a local configuration at each club. Internal matches are recognizable by equality of the tagged club coordinates; the finite slot sets make the resulting configuration indicators measurable.

Integrating these indicators gives the scaled local constraints. The almost-everywhere participation requirement is sufficient: exceptional clubs form a null set, and the finite counting factor on slot spaces preserves nullity.

Measure preservation supplies both donor and patient balance equations. Splitting matched donor slots into internal and external parts gives exactly the stated objective.

Finding: Correct, including the handling of exceptional clubs.

5. Lemma 2: avoiding same-club matches

The finite-union-of-intervals hypothesis is sufficient for the stated piecewise-translation parametrizations.

The fixed-point calculation is correct. For each pair of translation pieces and each possible wrap value \(k\in\{0,1\}\), a fixed point forces

\[ \theta=\eta_i-\zeta_j+kz. \]

There are finitely many such values. Since \(z>0\), a shift outside this finite set exists. That choice excludes every fixed point, including interval endpoints, rather than merely excluding fixed points almost everywhere.

The composition remains a measurable, measure-preserving bijection with measurable inverse. The proof invokes this lemma only for positive edge masses, so its positive-measure hypothesis is satisfied.

Finding: Correct.

6. LP-to-allocation direction

Lemma 1 supplies finite convex decompositions of the normalized local variables. The resulting finite interval partitions realize the prescribed local configurations and internal matches exactly.

The external source and target partitions have the required masses by the balance equations. Cutting finitely many half-open intervals preserves the finite-union structure required by Lemma 2.

Different type tags ensure that cross-type matches connect different clubs. For same-type edges, Lemma 2 ensures the same property by excluding equal club coordinates.

The disjointness argument is sufficient: partitions prevent repeated use within a slot, local configurations separate internal and external use, and different slot labels denote different slot-space points. Consequently, the finite union of the maps is a bijection between measurable used subsets, is measure preserving, and has measurable inverse.

Every configured club retains exactly its prescribed external counts. No additional scheduling or cycle condition is required by the task.

Finding: Correct; the converse realizes every feasible LP point.

7. Polynomial complexity and boundary cases

The variable bound is valid:

\[ \sum_t(r_t+1)^4\le(m+\tau)^4. \]

There are at most \(m^2\) compatibility edges. The number of constraints and their explicit encoding length are also polynomial.

After count enumeration, the LP uses bounded integer counts and supplied rational masses, weights, and threshold. The stated rational-LP feasibility theorem therefore applies with polynomial dimensions and coefficient encoding length.

The decision procedure requires only LP feasibility; it does not require computing or outputting the interval realization.

The argument also handles empty slot sets, absent compatibility edges, negative weights, arbitrary rational thresholds, and equality at the threshold. All inequalities are non-strict, and both directions preserve weight exactly.

Finding: Correct.

8. Discrete construction and scope

The cited reduction indeed assigns a set-club multiplier equal to the reciprocal of its set size, as described in Section 7. Thus that construction does not establish hardness under the stated multiplier restriction. [Farina, Dickerson, and Sandholm, Theorem 1](https://www.ijcai.org/proceedings/2017/0029.pdf)

The atomless proof is independent of that reduction. Its claimed extension to nonnegative rational multipliers is supported: the multiplier enters only the enumeration of permitted count pairs, and the remaining argument does not require it to be at least one.

Finding: Correct.

No additional mathematical 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.