Answer: polynomial-time solvable
Theorem 8 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateComputing the optimal partition for the minimum of averages (MoA) objective for a score based compatibility matrix is NP-hard.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finitely many score types \(T\), rational scores \(a_t\ge 0\), rational masses \(\mu_t\ge 0\) summing to one, and trio templates \(g\) with repetition, maximize \(\rho\) over \(q_g\ge 0\) subject to \(\sum_g c_t(g)q_g=3\mu_t\) for every type \(t\), and require every template with \(q_g>0\) to satisfy \(\bigl(\sum_{t\in g}a_t/3\bigr)^2\ge\rho\).
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive masses \(\mu_t\in\mathbb{Q}_{>0}\), encoded in binary, with \(\sum_{t\in T}\mu_t=1\). Each type has a binary rational score \(a_t\ge0\). Here \(\tau\) is the support size, not the number of possible types, and \(L\) is the total input bit length.
Let \(G\) contain all unordered multisets of three types from \(T\), allowing repetition; \(c_t(g)\) is the multiplicity of \(t\) in \(g\). Define \(h(g)=\bigl(\sum_{t\in T}c_t(g)a_t/3\bigr)^2\). This averages product compatibilities over all ordered pairs of group positions, including diagonal pairs.
A grouping assigns real weights \(q_g\ge0\) satisfying \(\sum_{g\in G}c_t(g)q_g=3\mu_t\) for every \(t\in T\); thus \(\sum_{g\in G}q_g=1\). Its value is \(\min_{g:q_g>0}h(g)\). Group size is fixed at three; the discrete number of groups \(m\) is absent after normalization, so running times are measured in \(\tau\) and \(L\).
Is computing the exact maximum grouping value solvable in polynomial time in \(\tau\) and \(L\), or is it NP-hard?
For finite indivisible agents, maximizing the minimum group happiness under product compatibilities is NP-hard even for groups of three and positive integer scores. [Source](https://arxiv.org/pdf/1703.07807).
No result settling this exact mass formulation was located in the literature search.
Computing the exact maximum grouping value is polynomial-time solvable in \(\tau\) and \(L\).
The proof uses the fixed group size: there are only polynomially many possible groups. For each candidate value, feasibility is a rational linear programming problem.
Index the types by \(T=\{1,\ldots,\tau\}\). Every group is uniquely represented by a triple \((i,j,k)\) with \(1\le i\le j\le k\le\tau\). Thus the number of groups is
\(\displaystyle N=|G|=\binom{\tau+2}{3}=O(\tau^3).\)
Compute \(h(g)\) for every group, and sort the distinct values as
\(\displaystyle v_1<v_2<\cdots<v_s,\qquad s\le N.\)
For every feasible grouping, summing its mass constraints gives
\(\displaystyle 3\sum_{g\in G}q_g=\sum_{t\in T}3\mu_t=3.\)
Consequently, its positive support is nonempty. Because that support is finite, its minimum happiness equals \(h(g)\) for some supported group. Hence every grouping value belongs to \(\{v_1,\ldots,v_s\}\).
There is at least one feasible grouping: assign \(q_{\{t,t,t\}}=\mu_t\) for each type and zero weight to every other group. Each type’s constraint then reads \(3q_{\{t,t,t\}}=3\mu_t\).
The set of attained grouping values is therefore a nonempty subset of a finite set. In particular, the maximum exists and is one of the candidate values.
For a rational threshold \(v\), define
\(\displaystyle G_v=\{g\in G:h(g)\ge v\}.\)
Consider the following system, with one real variable \(q_g\) for each \(g\in G_v\):
\(\displaystyle \sum_{g\in G_v}c_t(g)q_g=3\mu_t\quad\text{for every }t\in T,\qquad q_g\ge0\quad\text{for every }g\in G_v.\)
Claim. This system is feasible if and only if there is a grouping with value at least \(v\).
Proof. If a grouping has value at least \(v\), every group with positive weight belongs to \(G_v\). Restricting its variables to \(G_v\) therefore satisfies the system.
Conversely, extend any feasible solution of the system by assigning zero weight to groups outside \(G_v\). This gives all the required mass constraints. Summing those constraints gives total weight one, so some group has positive weight. Every such group has happiness at least \(v\), and therefore the grouping value is at least \(v\). This proves the claim.
All coefficients in the constraint matrix belong to \(\{0,1,2,3\}\), and all right-hand sides are rational. Thus this is an ordinary rational linear feasibility problem. The standard polynomial-time theorem for rational linear programming decides its feasibility exactly in time polynomial in its dimensions and binary encoding length. Equality constraints may equivalently be represented by pairs of non-strict inequalities; no strict positivity constraints are needed.
Threshold feasibility is monotone: if \(v\le w\), then \(G_w\subseteq G_v\), so feasibility at \(w\) implies feasibility at \(v\).
The algorithm is therefore:
The smallest candidate is feasible because it permits every group. Thus the search always returns a candidate.
To check exactness, let \(V^\star\) be the maximum grouping value. Section 1 shows that \(V^\star\) is a candidate. Section 2 shows that a candidate is feasible precisely when some grouping attains at least that value. Accordingly, the largest feasible candidate equals \(V^\star\).
It remains to check the binary encoding sizes:
Since \(N=O(\tau^3)\), every step, including the exact rational arithmetic and linear programming calls, takes time polynomial in \(\tau\) and \(L\). The returned value also has \(O(L)\) bits.
The cited paper’s Theorem 8 proves hardness by reducing from a partition of indivisible items into triples. Its proof requires an actual partition of the finite item set. [Rajkumar, Mukherjee, and Tulabandhula, Theorem 8](https://arxiv.org/pdf/1703.07807).
The formulation here instead permits arbitrary nonnegative real group weights. At a fixed threshold, its constraints are exactly the linear system proved above. Clearing mass denominators would not impose the additional integrality conditions required for a partition of a prescribed finite population.
Thus the finite-agent hardness result is compatible with polynomial-time exact optimization for the stated mass formulation.
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned task correctly: computing the exact maximum grouping value is polynomial-time solvable in \(\tau\) and \(L\). The argument is rigorous, and no repair is needed.
Every unordered multiset of three types has exactly one representation \((i,j,k)\) with \(1\le i\le j\le k\le\tau\). The count
\[
|G|=\binom{\tau+2}{3}=O(\tau^3)
\]
is correct and includes groups with repeated types.
The normalization calculation is valid: each group has total multiplicity three, so summing the type constraints yields
\[
3\sum_{g\in G}q_g=3\sum_{t\in T}\mu_t=3.
\]
Consequently, every feasible grouping has nonempty positive support. Its value is the minimum of a nonempty finite collection of group happiness values and therefore belongs to the enumerated candidate set.
The proposed feasible grouping, assigning weight \(\mu_t\) to \(\{t,t,t\}\), satisfies every constraint. Thus the set of attained values is nonempty and finite. This correctly establishes existence of an attained maximum; no continuity or compactness assertion is required.
Finding: Correct.
Both directions of the equivalence are justified:
Using \(h(g)\ge v\), rather than a strict inequality, correctly includes groups whose happiness equals the threshold. Nonnegativity constraints suffice; the formulation does not require prescribing which permitted groups receive positive weight.
If \(G_v\) is empty, the system is infeasible because its left-hand sides are zero while every \(\mu_t\) is positive. This case creates no exception to the equivalence.
Finding: Correct.
The invoked theorem is stated sufficiently precisely for this application: feasibility of an explicitly represented rational linear system can be decided exactly in time polynomial in its dimensions and binary encoding length. Polynomial-time solvability of rational linear programming in this bit model is established in the literature. [Adler and Beling, *Polynomial Algorithms for Linear Programming over the Algebraic Numbers*](https://doi.org/10.1145/129712.129760).
All relevant hypotheses are satisfied as written:
Thus the use of exact feasibility remains valid even when the feasible region lies entirely in a lower-dimensional affine subspace.
Finding: Correct; no unverified theorem application.
The inclusion \(G_w\subseteq G_v\) whenever \(v\le w\) correctly establishes monotonicity. The smallest candidate permits every group and is feasible.
Binary search therefore identifies the largest feasible candidate. Since the attained optimum is itself a candidate, and threshold feasibility is equivalent to attainability of at least that threshold, the returned candidate equals the exact optimum.
Deduplication handles equal happiness values correctly. The search also works when there is only one distinct candidate.
Finding: Correct.
The stated arithmetic bounds are valid. Each happiness value uses only three input scores, followed by a fixed number of rational additions and multiplications:
\[
h(\{i,j,k\})=\frac{(a_i+a_j+a_k)^2}{9}.
\]
The resulting numerator and denominator have \(O(L)\) bits, including when indices repeat. Exact cross multiplication compares candidates using integers of \(O(L)\) bits.
The threshold matrix has at most \(\tau N\) constant-size entries, and its right-hand sides have total encoding length \(O(L)\). Nonnegativity is a standard variable restriction and does not invalidate this encoding estimate.
Enumeration, sorting, threshold construction, and \(O(\log(N+1))\) exact feasibility calls all have polynomial bit complexity. The returned value has \(O(L)\) bits.
Finding: Correct.
The source attribution is accurate: Theorem 8 reduces from 3-Partition and requires a partition of indivisible items into groups of three. [Rajkumar, Mukherjee, and Tulabandhula, Theorem 8](https://arxiv.org/pdf/1703.07807).
The prover correctly explains that clearing denominators in the mass constraints does not impose integer group counts for a prescribed population. The cited discrete hardness therefore does not contradict the established continuous algorithm.
Finding: Correct.
The proof addresses the exact formulation, including repetitions, rational input encoding, and arbitrary real group weights. The edge cases \(\tau=1\), zero scores, and coincident candidate values are covered by the argument. No unjustified step, false assertion, missing lemma, or necessary clarification was found.
⟨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.