← back to the atlas

d4-conf-ijcai-2020-0821 (d4-conf-ijcai-2020-0821)

Answer: Polynomial-time solvable: \(\mathrm P\), with running time polynomial in \(m,\tau,L\).

The anchor (named result in the paper)

Theorem 3.2 — class: hardness

The continuous mirror question, as graded

Given a finite plot-graph template with rational per-capita plot supplies, rational masses over supported singleton and friend-pair types, and each type's complete valuation profile and friendship value, maximize total welfare (or decide whether it reaches a rational threshold) by assigning mass to feasible whole-bundle allocations. Each singleton unit receives one plot and each pair unit receives two distinct plots; type mass may split among bundles, but every unit receives an integral bundle.

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

Let \(G=(V,E)\) be a finite simple undirected plot template with \(m=|V|\ge1\), and binary-rational supplies \(s_v\ge0\) satisfying \(\sum_v s_v=1\).
A society is given by its support: the list of \(\tau\) singleton or friend-pair types with positive binary-rational masses \(a_t\). Here \(\tau\) is the support size, not the number of possible types. A type has \(k_t\in\{1,2\}\) members; masses count singleton or pair units, normalized by \(\sum_t k_ta_t=1\).
Each member \(r\) of type \(t\) has a complete valuation profile \(u_{t,r}:V\to[0,1]\cap\mathbb Q\). A pair has reciprocal friendship weights \(\phi_{t,12},\phi_{t,21}\in\mathbb Q_{\ge0}\); there are no friendships between units.
A singleton bundle is one vertex; a pair bundle is an ordered pair \((v,w)\) of distinct vertices, assigning them to members one and two. Nonadjacent pair bundles are allowed.
An allocation splits each type's entire mass among its bundles using nonnegative real amounts. Each bundle receives whole plots for its members; aggregate consumption of vertex \(v\) must equal \(s_v\).
Singleton bundle welfare is \(u_{t,1}(v)\); pair bundle welfare is \(u_{t,1}(v)+u_{t,2}(w)+(\phi_{t,12}+\phi_{t,21})\mathbf1_{\{v,w\}\in E}\). Total welfare sums bundle welfare times assigned mass.
Given a positive binary-rational threshold \(T\), decide whether a feasible allocation has welfare at least \(T\); infeasible instances are no-instances. Let \(L\) be the total binary input length.

Is this continuous welfare-threshold problem in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

The discrete welfare-threshold problem is NP-complete even with binary valuations, one common positive directed friendship weight, disjoint friend pairs and singletons, and a plot graph consisting of one path and isolated vertices; it also admits a polynomial-time \(2\)-approximation for disjoint pairs and singletons. [Source](https://www.ijcai.org/proceedings/2020/0045.pdf)
No result settling this exact continuous formulation was identified in the literature search.

Modeling choices made when packaging the task

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

Resolution

The continuous welfare-threshold problem belongs to \(\mathrm P\), with running time polynomial in \(m,\tau,L\). It is exactly a rational linear feasibility problem with at most \(\tau m^2\) variables.

1. Enumerating bundles

Index the listed types by \(t\in\{1,\ldots,\tau\}\). For a singleton type, define
\(\mathcal B_t=\{(v):v\in V\}\).
For a pair type, define
\(\mathcal B_t=\{(v,w):v,w\in V,\ v\ne w\}\).
Thus every permitted bundle is included, including nonadjacent pair bundles.

For \(b\in\mathcal B_t\), let \(d_v(b)\) be \(1\) if vertex \(v\) occurs in \(b\), and \(0\) otherwise. Since pair bundles use distinct vertices, these are precisely the per-unit consumption coefficients. In particular,
\(\sum_{v\in V}d_v(b)=k_t\).

Define the welfare coefficient of each bundle by
\(c_{t,(v)}=u_{t,1}(v)\)
for singletons, and
\(c_{t,(v,w)}=u_{t,1}(v)+u_{t,2}(w)+(\phi_{t,12}+\phi_{t,21})\mathbf1_{\{v,w\}\in E}\)
for pairs. These are fixed rational coefficients: adjacency is determined when the bundle is enumerated.

Let \(\tau_1,\tau_2\) denote the numbers of singleton and pair types. The total number of bundles is
\(n=\tau_1m+\tau_2m(m-1)\le\tau m^2\).
Only the listed support types contribute variables.

2. The linear feasibility system

Introduce a real variable \(x_{t,b}\) for every listed type \(t\) and bundle \(b\in\mathcal B_t\). Its meaning is the mass of type \(t\) assigned to bundle \(b\).

Impose the following constraints.

Nonnegative assigned masses:

\[ \text{This line intentionally omitted} \]

\(x_{t,b}\ge0\qquad(t\in\{1,\ldots,\tau\},\ b\in\mathcal B_t).\)

Allocation of each type’s entire mass:

\(\displaystyle\sum_{b\in\mathcal B_t}x_{t,b}=a_t\qquad(t\in\{1,\ldots,\tau\}).\)

Exact vertex supplies:

\(\displaystyle\sum_{t=1}^{\tau}\sum_{b\in\mathcal B_t}d_v(b)x_{t,b}=s_v\qquad(v\in V).\)

Required welfare:

\(\displaystyle\sum_{t=1}^{\tau}\sum_{b\in\mathcal B_t}c_{t,b}x_{t,b}\ge T.\)

The variables measure singleton or pair units, as required. A pair mass of \(x_{t,b}\) consumes \(x_{t,b}\) at each of its two vertices, rather than twice that amount at either vertex.

3. Proof of equivalence

Suppose a feasible allocation has welfare at least \(T\). Set \(x_{t,b}\) equal to its assigned bundle masses. These variables are nonnegative. Allocation of each type’s entire mass gives the type equations; aggregate consumption gives the supply equations; and the stated welfare formula gives the threshold inequality. Hence the linear system is feasible.

Conversely, suppose the linear system has a real solution. Assign mass \(x_{t,b}\) of each type \(t\) to bundle \(b\). Nonnegativity and the type equations make this an allocation of each type’s entire mass. Every enumerated bundle is permitted, and each pair bundle assigns distinct vertices. The supply equations enforce exactly the prescribed aggregate consumption. Finally, the threshold inequality states that this allocation has welfare at least \(T\).

These implications prove exact equivalence, including rejection of infeasible allocation instances.

The boundary case \(m=1\) is also covered. If a pair type is present, its bundle set is empty, so its type equation becomes \(0=a_t\), which is impossible because listed masses are positive. Otherwise the singleton system applies.

4. Polynomial encoding length and exact decision

Besides nonnegativity, the system has \(\tau+m\) equalities and one inequality. Replacing each equality by two inequalities produces
\(n+2(\tau+m)+1\)
inequalities in \(n\) variables.

Every consumption coefficient belongs to \(\{0,1\}\). Each welfare coefficient is a sum of at most four input rationals. Adding a fixed number of binary-encoded rationals produces a rational of bit length \(O(L+1)\): a common denominator can be formed by multiplying their denominators, whose bit lengths add. The right-hand sides are input rationals.

Consequently, even a dense encoding of the entire system has length
\(O\bigl((n+\tau+m+1)(n+1)(L+1)\bigr)\),
which is polynomial in \(m,\tau,L\). Enumerating the bundles, checking adjacency, and computing their rational coefficients also takes polynomial time.

The standard polynomial-time rational linear-programming theorem decides feasibility of a rational system of linear inequalities over the reals in time polynomial in its binary encoding length. Its hypotheses hold here: the system has finitely many explicitly listed variables and constraints, and every coefficient is rational with the polynomial encoding bound just established. See [Khachiyan’s polynomial-time linear-programming theorem](https://www.mathnet.ru/eng/dan42319).

Applying that theorem decides the original problem exactly. In particular, incorporating the threshold as a constraint handles equality with \(T\) without an approximation tolerance.

5. Relation to discrete hardness

The [cited discrete model](https://www.ijcai.org/proceedings/2020/0045.pdf) requires a bijection between individual agents and plots. The present formulation permits each listed type’s mass to split among bundles and requires aggregate supply equalities. These conditions are precisely the linear constraints above, so the discrete hardness result does not contradict this polynomial-time algorithm.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the intended continuous problem correctly: it gives an exact rational linear feasibility formulation of polynomial encoding length. There are no substantive mathematical gaps. The only issue is an extraneous placeholder in the displayed constraints.

1. Bundle enumeration

The singleton and pair bundle sets match the task exactly. Pair bundles are ordered, exclude repeated vertices, and include nonadjacent vertices. Thus member-specific valuations are preserved without imposing an unintended adjacency restriction.

The count
\(n=\tau_1m+\tau_2m(m-1)\le\tau m^2\)
is correct for every \(m\ge1\). Variables are introduced only for supported types, so the argument uses the specified meaning of \(\tau\).

The consumption coefficient \(d_v(b)\) is correct: each member consumes one vertex, and distinctness ensures that a pair contributes at most one unit of consumption to any vertex. Consequently, \(\sum_v d_v(b)=k_t\).

2. Welfare coefficients and constraints

Both welfare coefficients reproduce the task’s formulas exactly. In particular, the pair coefficient includes both directed friendship weights precisely when the assigned vertices are adjacent. Adjacency is fixed by the enumerated bundle, so this coefficient is constant rather than a function of allocation variables.

The four constraint families correctly enforce:

The variables measure units of a type, rather than individual members. Therefore the type equation has right-hand side \(a_t\), while a pair bundle contributes its assigned mass to each of two vertices. No normalization factor is missing.

Minor issue: Under “Nonnegative assigned masses,” the display containing “This line intentionally omitted” is extraneous. The actual nonnegativity constraints immediately following it are complete, so this does not create a mathematical gap.

Minimum clarification: Delete that placeholder display.

3. Equivalence with the allocation problem

Both implications are valid as written.

An allocation supplies a variable value for every bundle and satisfies all four constraint families. Conversely, any real solution supplies exactly the bundle masses permitted by the allocation definition. The type and supply equations give the required allocation and consumption properties, and the welfare inequality gives the requested threshold.

The task permits real splitting of type masses and imposes aggregate supply constraints. Therefore no integrality condition, global matching condition, or additional compatibility condition is needed.

The equivalence correctly rejects infeasible allocation instances.

4. Boundary cases

The treatment of \(m=1\) is correct. A supported pair type has no bundles, so its type equation becomes \(0=a_t\), contradicting the required positive mass. With only singleton types, the stated formulation remains valid.

Zero supplies, zero valuations, and zero friendship weights cause no problem: the relevant constraints and coefficients still apply exactly. Equality of welfare with \(T\) is included by the non-strict threshold inequality.

No missing boundary case affects the conclusion.

5. Encoding length and running time

The inequality count \(n+2(\tau+m)+1\) is correct after including nonnegativity and replacing each equality by two inequalities.

Each welfare coefficient sums at most four input rationals. The stated denominator-product argument correctly bounds its bit length by \(O(L+1)\); numerator addition introduces only constant additional overhead because the number of summands is bounded.

The dense encoding bound
\(O((n+\tau+m+1)(n+1)(L+1))\)
is a valid polynomial upper bound. Bundle enumeration, adjacency checks, and exact coefficient arithmetic can all be performed within polynomial time.

The invoked theorem is stated sufficiently precisely: feasibility of an explicitly represented rational linear inequality system over the reals is decidable in time polynomial in its binary encoding length. All its hypotheses are checked. The attribution is to [Khachiyan’s polynomial-time linear-programming theorem](https://www.mathnet.ru/eng/dan42319).

This application supplies exact feasibility decision, including lower-dimensional feasible sets and threshold equality; no numerical tolerance assumption is introduced.

6. Relation to discrete hardness

The comparison is accurate: the cited discrete model defines allocations as bijections between agents and plots. [Source, Section 2](https://www.ijcai.org/proceedings/2020/0045.pdf).

That discrete requirement differs from the continuous task’s mass-splitting allocation definition. Its hardness therefore does not invalidate the proved polynomial-time formulation.

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