Answer: \(\mathrm{P}\)
Proposition 6 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThe MIN-ESW-C2 and MIN-USW-C2 problems are NP-complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(M\) resource categories and a finite set of types \(\theta=(\succ_\theta,e_\theta)\), each with rational mass \(\mu_\theta>0\) summing to \(1\), let category supplies be \(\beta_r=\sum_{\theta:e_\theta=r}\mu_\theta\) and initial allocation be \(x^0_{\theta,e_\theta}=\mu_\theta\). A move chooses types \(\theta,\theta'\), categories \(r,s\), and \(\delta>0\) with \(x_{\theta,r},x_{\theta',s}\ge\delta\), \(s\succ_\theta r\), and \(r\succ_{\theta'}s\), then exchanges mass \(\delta\) between those cells. Given a rational threshold \(q\), does a finite sequence of such moves reach an allocation \(x\) with \(\sum_{\theta,r}x_{\theta,r}(M+1-\operatorname{rank}_\theta(r))\ge q\)?
Let \(R=\{1,\ldots,m\}\), with \(m\ge1\). A society is given by its support: a list of \(\tau\) types \(\theta=(\succ_\theta,e_\theta)\), where \(\succ_\theta\) is a strict total order on \(R\), \(e_\theta\in R\), and each mass \(\mu_\theta>0\) is a binary rational, with \(\sum_\theta\mu_\theta=1\). Here \(\tau\) is the support size, not the number of possible types.
Set \(\beta_r=\sum_{\theta:e_\theta=r}\mu_\theta\). An allocation has real entries \(x_{\theta,r}\ge0\), row sums \(\mu_\theta\), and column sums \(\beta_r\); initially \(x^0_{\theta,e_\theta}=\mu_\theta\) and all other entries are zero.
A move chooses distinct types \(\theta,\theta'\), distinct categories \(r,s\), and real \(0<\delta\le\min\{x_{\theta,r},x_{\theta',s}\}\), with \(s\succ_\theta r\) and \(r\succ_{\theta'}s\). It subtracts \(\delta\) from those two cells and adds \(\delta\) to \(x_{\theta,s}\) and \(x_{\theta',r}\), leaving other entries unchanged.
Given a binary rational \(q\), the decision problem asks whether a finite sequence of moves, possibly empty, reaches \(x\) with \(\sum_{\theta,r}x_{\theta,r}(m+1-\operatorname{rank}_\theta(r))\ge q\), where rank one is best. Only allocations reached after finitely many moves count.
Is this decision problem in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard, where \(L\) is the total input bit length?
For discrete societies with one distinct resource per agent, the corresponding utilitarian threshold reachability problem under strictly improving bilateral swaps is NP-complete ([Damamme et al., 2015](https://www.ifaamas.org/Proceedings/aamas2015/aamas/p625.pdf)). No result settling the exact mass problem above was identified in the literature search.
The decision problem is in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\). The proof reduces the exact threshold question to finite reachability in a continuous Petri net.
A continuous Petri net has finitely many places and transitions, with nonnegative integer input and output matrices \(\mathrm{Pre}\) and \(\mathrm{Post}\). A marking \(a\) assigns a nonnegative real number to each place. Transition \(t\) can fire by a real amount \(\delta>0\) when \(a_p\ge\delta\,\mathrm{Pre}_{p,t}\) for every place \(p\); its resulting marking is \(a+\delta(\mathrm{Post}_{\cdot,t}-\mathrm{Pre}_{\cdot,t})\).
Known theorem (Fraca–Haddad). Given such a net and nonnegative rational initial and target markings, deciding whether a finite sequence of real-valued firings reaches the target is polynomial-time in the binary encoding size. This is the reachability result in Proposition 27, using Algorithm 2; Definitions 4–5 specify precisely the firing and finite-reachability semantics above. [Fraca and Haddad, *Complexity Analysis of Continuous Petri Nets*](https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/FH-fundi15.pdf).
We apply this theorem to an explicitly constructed net.
Write \(w_{\theta,r}=m+1-\operatorname{rank}_\theta(r)\) and \(W(x)=\sum_{\theta,r}w_{\theta,r}x_{\theta,r}\). Each weight is an integer satisfying \(1\le w_{\theta,r}\le m\).
Compute \(W(x^0)\). If \(q\le W(x^0)\), return yes, witnessed by the empty sequence. Henceforth assume \(q>W(x^0)\), which implies \(q>0\).
Construct a continuous Petri net with one place \(p_{\theta,r}\) for every allocation cell and one additional utility place \(z\). Its transitions are as follows.
\(p_{\theta,r}+p_{\theta',s}\longrightarrow p_{\theta,s}+p_{\theta',r}\).
All four arc weights are one. Firing this transition by \(\delta\) is exactly the corresponding society move.
\(p_{\theta,r}\longrightarrow w_{\theta,r}z\).
Firing by \(\delta\) consumes \(\delta\) from that cell and produces \(w_{\theta,r}\delta\) in \(z\).
The initial marking \(a^0\) has \(a^0_{p_{\theta,r}}=x^0_{\theta,r}\) and \(a^0_z=0\). The fixed target marking \(b\) has \(b_{p_{\theta,r}}=0\) for every cell and \(b_z=q\).
Claim. The society instance is a yes-instance if and only if \(b\) is finitely reachable from \(a^0\).
Suppose finitely many society moves reach an allocation \(x\) satisfying \(W(x)\ge q\).
Execute the corresponding swap transitions in the net. Next, for each positive cell \(x_{\theta,r}\), fire its collection transition by exactly \(x_{\theta,r}\). Every such firing is enabled, since it consumes only that cell.
After these finitely many collection firings, all cell places are zero and the utility place contains exactly \(W(x)\). If \(W(x)>q\), fire the disposal transition by \(W(x)-q\). If \(W(x)=q\), no disposal is needed.
Thus the target \(b\) is reached after finitely many firings.
Conversely, suppose a finite auxiliary firing sequence reaches \(b\). Remove all collection and disposal firings, retaining the swap firings in their original order and with their original amounts.
We first prove that this retained sequence is executable in the society.
Process the auxiliary sequence from its beginning. Let \(a\) be its current vector of cell markings, and let \(X\) be the allocation obtained by executing only the swaps encountered so far. Initially, \(X=a=x^0\). Maintain the coordinatewise inequality \(X\ge a\).
This induction proves that every retained swap is legal. Consequently, the retained finite sequence reaches a valid society allocation \(X\): its row and column sums remain those of \(x^0\).
It remains to compute its utility. Let \(d_{\theta,r}\) be the total amount consumed by collection transitions from cell \(p_{\theta,r}\), and let \(h\ge0\) be the total amount removed from \(z\) by disposal firings.
Throughout the preceding induction, the difference \(X-a\) equals the vector of amounts collected so far: swaps preserve this difference, and collection increases the corresponding coordinate by its firing amount. At the auxiliary target, every cell marking is zero. Therefore \(X_{\theta,r}=d_{\theta,r}\) for every cell.
Only collection produces utility tokens, and only disposal consumes them. Since the initial utility marking is zero and the final one is \(q\), we obtain
\(q=\sum_{\theta,r}w_{\theta,r}d_{\theta,r}-h\).
Hence
\(W(X)=\sum_{\theta,r}w_{\theta,r}d_{\theta,r}=q+h\ge q\).
The retained society sequence therefore witnesses a yes-instance. This proves the claim.
The net has \(\tau m+1\) places, at most \(\tau^2m^2\) swap transitions, \(\tau m\) collection transitions, and one disposal transition. Every arc weight is a nonnegative integer at most \(m\). Its initial and target markings contain only the input masses, \(q\), and zeros.
Thus the net and both markings have binary encoding size polynomial in \(m,\tau,L\), and they can be constructed within that bound. All hypotheses of the finite-reachability theorem hold. Applying its polynomial-time algorithm decides the society problem.
The equivalence preserves finite sequences in both directions and includes threshold equality exactly. No passage to a limit or assumption that a welfare supremum is attained is used.
⟨structured verdict parsed — rendered above⟩
The reduction is correct and establishes polynomial-time decidability of the exact mass problem. The only issue is a minor mismatch between the cited paper’s firing convention and the prover’s description: the paper permits zero-amount firings. This does not affect reachability, but the write-up should acknowledge it.
I checked the cited [Fraca–Haddad paper](https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/FH-fundi15.pdf). Definition 1 permits arbitrary nonnegative integer input and output matrices, including transitions with no outputs. Definition 3 specifies rational initial markings for computational inputs. Definition 5 defines reachability using finite firing sequences. Proposition 26 establishes the correctness of Algorithm 2 for that reachability relation, and Proposition 27 establishes polynomial running time.
Thus the citation concerns exact finite reachability, rather than only limit reachability. No consistency, conservation, or positive-marking assumption is imposed by Proposition 27.
Minor issue: Definition 4 permits firing amounts \(\alpha\ge0\), whereas the prover describes amounts \(\delta>0\) and says the definitions specify “precisely” those semantics. The minimum clarification is to state that zero-amount firings may be omitted when comparing the two conventions.
The weights satisfy \(1\le w_{\theta,r}\le m\), and the initial total mass is one. Consequently, \(W(x^0)>0\).
If \(q\le W(x^0)\), the empty sequence is a valid witness, including when \(q\) is negative. Otherwise, \(q>0\), so the proposed target marking is nonnegative. This correctly handles the domain restriction needed by the reachability theorem.
Distinct types and distinct categories ensure that the four cell places in a swap transition are distinct. Its enabling condition is exactly
\(\delta\le\min\{x_{\theta,r},x_{\theta',s}\}\), and its marking update matches the society move.
The preference conditions are imposed when constructing transitions. Therefore every retained swap has the required strict improvements. The construction neither introduces forbidden swaps nor omits allowed ones.
Collection and disposal also satisfy the stated Petri-net requirements: their arc weights are nonnegative integers, and the disposal transition may have no outputs.
After a successful society sequence, the corresponding net marking has cell entries \(x_{\theta,r}\) and utility marking zero.
Each positive cell can then be collected in its entirety, since that transition consumes only its own cell. There are at most \(\tau m\) such firings. The resulting utility marking is exactly \(W(x)\).
Disposal is enabled for amount \(W(x)-q\) whenever this amount is positive. Equality requires no disposal. Thus the target is reached exactly after finitely many firings.
The vectors \(X\) and \(a\) both refer to cell coordinates. Initially they agree. Collection decreases \(a\), disposal changes neither vector, and a swap applies the same increment vector to both.
Consequently, the coordinatewise invariant \(X\ge a\) is preserved. Whenever an auxiliary swap is enabled, its input cells in \(X\) contain sufficient mass for the same amount. This verifies each retained society move individually, even when collection firings are interleaved with swaps.
The retained swaps preserve nonnegativity, row sums, and column sums. Hence their final marking \(X\) is a valid allocation. No conservation property of the auxiliary collection transitions is needed.
The stronger invariant \(X-a=d\), with \(d\) the cumulative collection vector, follows from the updates described in the write-up. At the target, the cell vector \(a\) is zero, giving \(X=d\).
The utility place is affected only by collection and disposal. Since the sequence is finite, the totals \(d\) and \(h\) are well-defined, and the final utility balance is
\(q=\sum_{\theta,r}w_{\theta,r}d_{\theta,r}-h\).
Therefore \(W(X)=q+h\ge q\). This establishes the required reverse implication without assuming that collections occurred after all swaps.
The stated bounds on places and transitions are correct. Repeated descriptions of an identical swap, if included, do not invalidate the bound or the reduction.
Arc weights require polynomial encoding length, and the markings use only input rationals and zeros. Even a dense matrix representation has polynomial size in \(m,\tau,L\). Rank lookup, transition enumeration, exact evaluation of \(W(x^0)\), and rational comparison can all be performed within a polynomial bound.
Thus the external theorem is applied to a polynomial-size instance with all required hypotheses satisfied.
The argument remains valid for \(m=1\), a single supported type, zero-supply categories, and instances with no eligible swaps. The reverse implication prevents auxiliary collection or disposal from creating a false positive.
Both directions preserve finite witnesses. Threshold equality is handled explicitly, so the proof does not substitute a supremum or a limiting allocation for a reachable allocation.
The prover resolves the assigned question in substance. Only the firing-convention clarification is needed; no additional mathematical argument is missing.
⟨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.